Equivalence relations

This file defines the complete lattice of equivalence relations on a type, results about the inductively defined equivalence closure of a binary relation, and the analogues of some isomorphism theorems for quotients of arbitrary types.

Implementation notes

The complete lattice instance for equivalence relations could have been defined by lifting the Galois insertion of equivalence relations on α into binary relations on α, and then using CompleteLattice.copy to define a complete lattice instance with more appropriate definitional equalities (a similar example is Filter.CompleteLattice in Mathlib/Order/Filter/Basic.lean). This does not save space, however, and is less clear.

Partitions are not defined as a separate structure here; users are encouraged to reason about them using the existing Setoid and its infrastructure.

Tags

setoid, equivalence, iseqv, relation, equivalence relation

theorem Setoid.ext_iff {α : Sort u_3} {s t : Setoid α} : s = t ↔ ∀ (a b : α), s a b ↔ t a b

theorem Setoid.eq_iff_rel_eq {α : Type u_1} {r₁ r₂ : Setoid α} : r₁ = r₂ ↔ ⇑r₁ = ⇑r₂

Two equivalence relations are equal iff their underlying binary operations are equal.

instance Setoid.instLE_mathlib {α : Type u_1} : LE (Setoid α)

Defining ≤ for equivalence relations.

Equations

• Setoid.instLE_mathlib = { le := fun (r s : Setoid α) => ∀ ⦃x y : α⦄, r x y → s x y }

theorem Setoid.le_def {α : Type u_1} {r s : Setoid α} : r ≤ s ↔ ∀ {x y : α}, r x y → s x y

theorem Setoid.refl' {α : Type u_1} (r : Setoid α) (x : α) : r x x

theorem Setoid.symm' {α : Type u_1} (r : Setoid α) {x y : α} : r x y → r y x

theorem Setoid.trans' {α : Type u_1} (r : Setoid α) {x y z : α} : r x y → r y z → r x z

theorem Setoid.comm' {α : Type u_1} (s : Setoid α) {x y : α} : s x y ↔ s y x

def Setoid.ker {α : Type u_1} {β : Type u_2} (f : α → β) : Setoid α

The kernel of a function is an equivalence relation.

Equations

• Setoid.ker f = { r := Function.onFun (fun (x1 x2 : β) => x1 = x2) f, iseqv := ⋯ }

@[simp]

theorem Setoid.ker_mk_eq {α : Type u_1} (r : Setoid α) : ker Quotient.mk'' = r

The kernel of the quotient map induced by an equivalence relation r equals r.

theorem Setoid.ker_apply_mk_out {α : Type u_1} {β : Type u_2} {f : α → β} (a : α) : f ⟦a⟧.out = f a

theorem Setoid.ker_def {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α} : (ker f) x y ↔ f x = f y

def Setoid.prod {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) : Setoid (α × β)

Given types α, β, the product of two equivalence relations r on α and s on β: (x₁, x₂), (y₁, y₂) ∈ α × β are related by r.prod s iff x₁ is related to y₁ by r and x₂ is related to y₂ by s.

Equations

• r.prod s = { r := fun (x y : α × β) => r x.1 y.1 ∧ s x.2 y.2, iseqv := ⋯ }

theorem Setoid.prod_apply {α : Type u_1} {β : Type u_2} {r : Setoid α} {s : Setoid β} {x₁ x₂ : α} {y₁ y₂ : β} : (r.prod s) (x₁, y₁) (x₂, y₂) ↔ r x₁ x₂ ∧ s y₁ y₂

theorem Setoid.piSetoid_apply {ι : Sort u_3} {α : ι → Sort u_4} {r : (i : ι) → Setoid (α i)} {x y : (i : ι) → α i} : piSetoid x y ↔ ∀ (i : ι), (r i) (x i) (y i)

def Setoid.prodQuotientEquiv {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) : Quotient r × Quotient s ≃ Quotient (r.prod s)

A bijection between the product of two quotients and the quotient by the product of the equivalence relations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Setoid.prodQuotientEquiv_apply {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) (x✝ : Quotient r × Quotient s) : (r.prodQuotientEquiv s) x✝ = match x✝ with | (x, y) => Quotient.map₂ Prod.mk ⋯ x y

@[simp]

theorem Setoid.prodQuotientEquiv_symm_apply {α : Type u_1} {β : Type u_2} (r : Setoid α) (s : Setoid β) (q : Quotient (r.prod s)) : (r.prodQuotientEquiv s).symm q = q.liftOn' (fun (xy : α × β) => (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯

noncomputable def Setoid.piQuotientEquiv {ι : Sort u_3} {α : ι → Sort u_4} (r : (i : ι) → Setoid (α i)) : ((i : ι) → Quotient (r i)) ≃ Quotient piSetoid

A bijection between an indexed product of quotients and the quotient by the product of the equivalence relations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Setoid.piQuotientEquiv_symm_apply {ι : Sort u_3} {α : ι → Sort u_4} (r : (i : ι) → Setoid (α i)) (q : Quotient piSetoid) (i : ι) : (piQuotientEquiv r).symm q i = q.liftOn' (fun (x : (i : ι) → α i) (i : ι) => Quotient.mk'' (x i)) ⋯ i

@[simp]

theorem Setoid.piQuotientEquiv_apply {ι : Sort u_3} {α : ι → Sort u_4} (r : (i : ι) → Setoid (α i)) (x : (i : ι) → Quotient (r i)) : (piQuotientEquiv r) x = Quotient.mk'' fun (i : ι) => (x i).out

instance Setoid.instMin_mathlib {α : Type u_1} : Min (Setoid α)

The infimum of two equivalence relations.

Equations

• Setoid.instMin_mathlib = { min := fun (r s : Setoid α) => { r := fun (x y : α) => r x y ∧ s x y, iseqv := ⋯ } }

theorem Setoid.inf_def {α : Type u_1} {r s : Setoid α} : ⇑(r ⊓ s) = ⇑r ⊓ ⇑s

The infimum of 2 equivalence relations r and s is the same relation as the infimum of the underlying binary operations.

theorem Setoid.inf_iff_and {α : Type u_1} {r s : Setoid α} {x y : α} : (r ⊓ s) x y ↔ r x y ∧ s x y

instance Setoid.instInfSet {α : Type u_1} : InfSet (Setoid α)

The infimum of a set of equivalence relations.

Equations

• Setoid.instInfSet = { sInf := fun (S : Set (Setoid α)) => { r := fun (x y : α) => ∀ r ∈ S, r x y, iseqv := ⋯ } }

theorem Setoid.sInf_def {α : Type u_1} {s : Set (Setoid α)} : ⇑(sInf s) = sInf (@r α '' s)

The underlying binary operation of the infimum of a set of equivalence relations is the infimum of the set's image under the map to the underlying binary operation.

instance Setoid.instPartialOrder {α : Type u_1} : PartialOrder (Setoid α)

Equations

• Setoid.instPartialOrder = { le := fun (x1 x2 : Setoid α) => x1 ≤ x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯, le_antisymm := ⋯ }

instance Setoid.completeLattice {α : Type u_1} : CompleteLattice (Setoid α)

The complete lattice of equivalence relations on a type, with bottom element = and top element the trivial equivalence relation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Setoid.top_def {α : Type u_1} : ⇑⊤ = ⊤

@[simp]

theorem Setoid.bot_def {α : Type u_1} : ⇑⊥ = fun (x1 x2 : α) => x1 = x2

theorem Setoid.eq_top_iff {α : Type u_1} {s : Setoid α} : s = ⊤ ↔ ∀ (x y : α), s x y

theorem Setoid.sInf_equiv {α : Type u_1} {S : Set (Setoid α)} {x y : α} : x ≈ y ↔ ∀ s ∈ S, s x y

theorem Setoid.sInf_iff {α : Type u_1} {S : Set (Setoid α)} {x y : α} : (sInf S) x y ↔ ∀ s ∈ S, s x y

theorem Setoid.quotient_mk_sInf_eq {α : Type u_1} {S : Set (Setoid α)} {x y : α} : ⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s x y

def Setoid.map_of_le {α : Type u_1} {s t : Setoid α} (h : s ≤ t) : Quotient s → Quotient t

The map induced between quotients by a setoid inequality.

Equations

• Setoid.map_of_le h = Quotient.map' id h

def Setoid.map_sInf {α : Type u_1} {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : Quotient (sInf S) → Quotient s

The map from the quotient of the infimum of a set of setoids into the quotient by an element of this set.

Equations

• Setoid.map_sInf h = Setoid.map_of_le ⋯

theorem Setoid.eqvGen_eq {α : Type u_1} (r : α → α → Prop) : Relation.EqvGen.setoid r = sInf {s : Setoid α | ∀ ⦃x y : α⦄, r x y → s x y}

The inductively defined equivalence closure of a binary relation r is the infimum of the set of all equivalence relations containing r.

theorem Setoid.sup_eq_eqvGen {α : Type u_1} (r s : Setoid α) : r ⊔ s = Relation.EqvGen.setoid fun (x y : α) => r x y ∨ s x y

The supremum of two equivalence relations r and s is the equivalence closure of the binary relation x is related to y by r or s.

theorem Setoid.sup_def {α : Type u_1} {r s : Setoid α} : r ⊔ s = Relation.EqvGen.setoid (⇑r ⊔ ⇑s)

The supremum of 2 equivalence relations r and s is the equivalence closure of the supremum of the underlying binary operations.

theorem Setoid.sSup_eq_eqvGen {α : Type u_1} (S : Set (Setoid α)) : sSup S = Relation.EqvGen.setoid fun (x y : α) => ∃ r ∈ S, r x y

The supremum of a set S of equivalence relations is the equivalence closure of the binary relation there exists r ∈ S relating x and y.

theorem Setoid.sSup_def {α : Type u_1} {s : Set (Setoid α)} : sSup s = Relation.EqvGen.setoid (sSup (@r α '' s))

The supremum of a set of equivalence relations is the equivalence closure of the supremum of the set's image under the map to the underlying binary operation.

@[simp]

theorem Setoid.eqvGen_of_setoid {α : Type u_1} (r : Setoid α) : Relation.EqvGen.setoid ⇑r = r

The equivalence closure of an equivalence relation r is r.

theorem Setoid.eqvGen_idem {α : Type u_1} (r : α → α → Prop) : Relation.EqvGen.setoid ⇑(Relation.EqvGen.setoid r) = Relation.EqvGen.setoid r

Equivalence closure is idempotent.

theorem Setoid.eqvGen_le {α : Type u_1} {r : α → α → Prop} {s : Setoid α} (h : ∀ (x y : α), r x y → s x y) : Relation.EqvGen.setoid r ≤ s

The equivalence closure of a binary relation r is contained in any equivalence relation containing r.

theorem Setoid.eqvGen_mono {α : Type u_1} {r s : α → α → Prop} (h : ∀ (x y : α), r x y → s x y) : Relation.EqvGen.setoid r ≤ Relation.EqvGen.setoid s

Equivalence closure of binary relations is monotone.

def Setoid.gi {α : Type u_1} : GaloisInsertion Relation.EqvGen.setoid (@r α)

There is a Galois insertion of equivalence relations on α into binary relations on α, with equivalence closure the lower adjoint.

Equations

• Setoid.gi = { choice := fun (r : α → α → Prop) (x : ⇑(Relation.EqvGen.setoid r) ≤ r) => Relation.EqvGen.setoid r, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

theorem Setoid.injective_iff_ker_bot {α : Type u_1} {β : Type u_2} (f : α → β) : Function.Injective f ↔ ker f = ⊥

A function from α to β is injective iff its kernel is the bottom element of the complete lattice of equivalence relations on α.

theorem Setoid.ker_iff_mem_preimage {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α} : (ker f) x y ↔ x ∈ f ⁻¹' {f y}

The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f.

def Setoid.liftEquiv {α : Type u_1} {β : Type u_2} (r : Setoid α) : { f : α → β // r ≤ ker f } ≃ (Quotient r → β)

Equivalence between functions α → β such that r x y → f x = f y and functions quotient r → β.

Equations

• r.liftEquiv = { toFun := fun (f : { f : α → β // r ≤ Setoid.ker f }) => Quotient.lift ↑f ⋯, invFun := fun (f : Quotient r → β) => ⟨f ∘ Quotient.mk'', ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Setoid.lift_unique {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quotient r → β) (Hg : f = g ∘ Quotient.mk'') : Quotient.lift f H = g

The uniqueness part of the universal property for quotients of an arbitrary type.

theorem Setoid.ker_lift_injective {α : Type u_1} {β : Type u_2} (f : α → β) : Function.Injective (Quotient.lift f ⋯)

Given a map f from α to β, the natural map from the quotient of α by the kernel of f is injective.

theorem Setoid.ker_eq_lift_of_injective {α : Type u_1} {β : Type u_2} {r : Setoid α} (f : α → β) (H : ∀ (x y : α), r x y → f x = f y) (h : Function.Injective (Quotient.lift f H)) : ker f = r

Given a map f from α to β, the kernel of f is the unique equivalence relation on α whose induced map from the quotient of α to β is injective.

noncomputable def Setoid.quotientKerEquivRange {α : Type u_1} {β : Type u_2} (f : α → β) : Quotient (ker f) ≃ ↑(Set.range f)

The first isomorphism theorem for sets: the quotient of α by the kernel of a function f bijects with f's image.

Equations

• Setoid.quotientKerEquivRange f = Equiv.ofBijective (Quotient.lift (fun (x : α) => ⟨f x, ⋯⟩) ⋯) ⋯

def Setoid.quotientKerEquivOfRightInverse {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.RightInverse g f) : Quotient (ker f) ≃ β

If f has a computable right-inverse, then the quotient by its kernel is equivalent to its domain.

Equations

• Setoid.quotientKerEquivOfRightInverse f g hf = { toFun := fun (a : Quotient (Setoid.ker f)) => a.liftOn' f ⋯, invFun := fun (b : β) => Quotient.mk'' (g b), left_inv := ⋯, right_inv := hf }

@[simp]

theorem Setoid.quotientKerEquivOfRightInverse_symm_apply {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.RightInverse g f) (b : β) : (quotientKerEquivOfRightInverse f g hf).symm b = Quotient.mk'' (g b)

@[simp]

theorem Setoid.quotientKerEquivOfRightInverse_apply {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.RightInverse g f) (a : Quotient (ker f)) : (quotientKerEquivOfRightInverse f g hf) a = a.liftOn' f ⋯

noncomputable def Setoid.quotientKerEquivOfSurjective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Surjective f) : Quotient (ker f) ≃ β

The quotient of α by the kernel of a surjective function f bijects with f's codomain.

If a specific right-inverse of f is known, Setoid.quotientKerEquivOfRightInverse can be definitionally more useful.

Equations

• Setoid.quotientKerEquivOfSurjective f hf = Setoid.quotientKerEquivOfRightInverse f (Function.surjInv hf) ⋯

def Setoid.map {α : Type u_1} {β : Type u_2} (r : Setoid α) (f : α → β) : Setoid β

Given a function f : α → β and equivalence relation r on α, the equivalence closure of the relation on f's image defined by 'x ≈ y iff the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.'

Equations

• r.map f = Relation.EqvGen.setoid (Relation.Map (⇑r) f f)

def Setoid.mapOfSurjective {α : Type u_1} {β : Type u_2} (r : Setoid α) (f : α → β) (h : ker f ≤ r) (hf : Function.Surjective f) : Setoid β

Given a surjective function f whose kernel is contained in an equivalence relation r, the equivalence relation on f's codomain defined by x ≈ y ↔ the elements of f⁻¹(x) are related to the elements of f⁻¹(y) by r.

Equations

• r.mapOfSurjective f h hf = { r := Relation.Map (⇑r) f f, iseqv := ⋯ }

theorem Setoid.mapOfSurjective_eq_map {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (h : ker f ≤ r) (hf : Function.Surjective f) : r.map f = r.mapOfSurjective f h hf

A special case of the equivalence closure of an equivalence relation r equalling r.

@[reducible, inline]

abbrev Setoid.comap {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) : Setoid α

Given a function f : α → β, an equivalence relation r on β induces an equivalence relation on α defined by 'x ≈ y iff f(x) is related to f(y) by r'.

See note [reducible non-instances].

Equations

• Setoid.comap f r = { r := Function.onFun (⇑r) f, iseqv := ⋯ }

theorem Setoid.comap_rel {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) (x y : α) : (comap f r) x y ↔ r (f x) (f y)

theorem Setoid.comap_eq {α : Type u_1} {β : Type u_2} {f : α → β} {r : Setoid β} : comap f r = ker (Quotient.mk'' ∘ f)

Given a map f : N → M and an equivalence relation r on β, the equivalence relation induced on α by f equals the kernel of r's quotient map composed with f.

noncomputable def Setoid.comapQuotientEquiv {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) : Quotient (comap f r) ≃ ↑(Set.range (Quotient.mk'' ∘ f))

The second isomorphism theorem for sets.

Equations

• Setoid.comapQuotientEquiv f r = (Quotient.congrRight ⋯).trans (Setoid.quotientKerEquivRange (Quotient.mk'' ∘ f))

def Setoid.quotientQuotientEquivQuotient {α : Type u_1} (r s : Setoid α) (h : r ≤ s) : Quotient (ker (Quot.mapRight h)) ≃ Quotient s

The third isomorphism theorem for sets.

Equations

• One or more equations did not get rendered due to their size.

def Setoid.correspondence {α : Type u_1} (r : Setoid α) : { s : Setoid α // r ≤ s } ≃o Setoid (Quotient r)

Given an equivalence relation r on α, the order-preserving bijection between the set of equivalence relations containing r and the equivalence relations on the quotient of α by r.

Equations

• One or more equations did not get rendered due to their size.

def Setoid.sigmaQuotientEquivOfLe {α : Type u_1} {r s : Setoid α} (hle : r ≤ s) : (q : Quotient s) × Quotient (comap Subtype.val r) ≃ Quotient r

Given two equivalence relations with r ≤ s, a bijection between the sum of the quotients by r on each equivalence class by s and the quotient by r.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quotient.subsingleton_iff {α : Type u_1} {s : Setoid α} : Subsingleton (Quotient s) ↔ s = ⊤

theorem Quot.subsingleton_iff {α : Type u_1} (r : α → α → Prop) : Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤