# 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

source
theorem Setoid.ext_iff {α : Sort u_3} {s t : Setoid α} :
s = t ↔ ∀ (a b : α), s a b ↔ t a b
source
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.

source
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 }

source
theorem Setoid.le_def {α : Type u_1} {r s : Setoid α} :
r ≤ s ↔ ∀ {x y : α}, r x y → s x y
source
theorem Setoid.refl' {α : Type u_1} (r : Setoid α) (x : α) :
r x x
source
theorem Setoid.symm' {α : Type u_1} (r : Setoid α) {x y : α} :
r x y → r y x
source
theorem Setoid.trans' {α : Type u_1} (r : Setoid α) {x y z : α} :
r x y → r y z → r x z
source
theorem Setoid.comm' {α : Type u_1} (s : Setoid α) {x y : α} :
s x y ↔ s y x
source
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 := ⋯ }

Instances For

source
@[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.

source
theorem Setoid.ker_apply_mk_out {α : Type u_1} {β : Type u_2} {f : α → β} (a : α) :
f ⟦a⟧.out = f a
source
@[simp]
theorem Setoid.ker_def {α : Type u_1} {β : Type u_2} {f : α → β} {x y : α} :
(ker f) x y ↔ f x = f y
source
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 := ⋯ }

Instances For

source
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₂
source
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)
source
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.

Instances For

source
@[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
source
@[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)) ⋯
source
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.

Instances For

source
@[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
source
@[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
source
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 := ⋯ } }

source
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.

source
theorem Setoid.inf_iff_and {α : Type u_1} {r s : Setoid α} {x y : α} :
(r ⊓ s) x y ↔ r x y ∧ s x y
source
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 := ⋯ } }

source
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.

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

- Setoid.instPartialOrder = { toLE := Setoid.instLE_mathlib, lt := fun (r s : Setoid α) => r ≤ s ∧ ¬s ≤ r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

source
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.

source
@[simp]
theorem Setoid.top_def {α : Type u_1} :
⇑⊤ = ⊤
source
@[simp]
theorem Setoid.bot_def {α : Type u_1} :
⇑⊥ = fun (x1 x2 : α) => x1 = x2
source
theorem Setoid.eq_top_iff {α : Type u_1} {s : Setoid α} :
s = ⊤ ↔ ∀ (x y : α), s x y
source
theorem Setoid.sInf_equiv {α : Type u_1} {S : Set (Setoid α)} {x y : α} :
x ≈ y ↔ ∀ s ∈ S, s x y
source
theorem Setoid.sInf_iff {α : Type u_1} {S : Set (Setoid α)} {x y : α} :
(sInf S) x y ↔ ∀ s ∈ S, s x y
source
theorem Setoid.quotient_mk_sInf_eq {α : Type u_1} {S : Set (Setoid α)} {x y : α} :
⟦x⟧ = ⟦y⟧ ↔ ∀ s ∈ S, s x y
source
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

Instances For

source
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 ⋯

Instances For

source
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.

source
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`.

source
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.

source
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`.

source
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.

source
@[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.

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

Equivalence closure is idempotent.

source
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.

source
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.

source
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 := ⋯ }

Instances For

source
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 α.

source
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.

source
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 := ⋯ }

Instances For

source
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.

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

Given a function `f`, lift it to the quotient by its kernel.

Equations

- Setoid.kerLift f = Quotient.lift f ⋯

Instances For

source
@[simp]
theorem Setoid.kerLift_mk {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
kerLift f ⟦x⟧ = f x
source
theorem Setoid.kerLift_injective {α : Type u_1} {β : Type u_2} (f : α → β) :
Function.Injective (kerLift f)

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

source
@[deprecated Setoid.kerLift_injective (since := "2025-10-11")]
theorem Setoid.ker_lift_injective {α : Type u_1} {β : Type u_2} (f : α → β) :
Function.Injective (kerLift f)

Alias of `Setoid.kerLift_injective`.

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

source
theorem Setoid.ker_eq_lift_of_injective {α : Type u_1} {β : Type u_2} {r : Setoid α} (f : α → β) (H : r ≤ ker f) (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.

source
theorem Setoid.lift_injective_iff_ker_eq_of_le {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (hle : r ≤ ker f) :
Function.Injective (Quotient.lift f hle) ↔ ker f = r
source
@[simp]
theorem Setoid.range_kerLift_eq_range {α : Type u_1} {β : Type u_2} (f : α → β) :
Set.range (kerLift f) = Set.range f

The image of `f` lifted to the quotient by its kernel is equal to the image of `f` itself.

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

The quotient of `α` by the kernel of a function `f` bijects with the image of `f` lifted to the quotient.

Equations

- Setoid.quotientKerEquivRangeKerLift f = Equiv.ofInjective (Setoid.kerLift f) ⋯

Instances For

source
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 = (Setoid.quotientKerEquivRangeKerLift f).trans (Equiv.setCongr ⋯)

Instances For

source
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 := Setoid.kerLift f, invFun := fun (b : β) => Quotient.mk'' (g b), left_inv := ⋯, right_inv := hf }

Instances For

source
@[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✝ = kerLift f a✝
source
@[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)
source
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) ⋯

Instances For

source
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)

Instances For

source
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 := ⋯ }

Instances For

source
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 equaling r.

source
@[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 := ⋯ }

Instances For

source
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)
source
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`.

source
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))

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[simp]
theorem Quotient.subsingleton_iff {α : Type u_1} {s : Setoid α} :
Subsingleton (Quotient s) ↔ s = ⊤
source
theorem Quot.subsingleton_iff {α : Type u_1} (r : α → α → Prop) :
Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤