doc-next-gen

Mathlib.Data.Setoid.Basic

Module docstring

{"# 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 "}

Setoid.instLE_mathlib instance
: LE (Setoid α)
Full source 
/-- Defining `≤` for equivalence relations. -/
instance : LE (Setoid α) :=
  ⟨fun r s => ∀ ⦃x y⦄, r x y → s x y⟩
Partial Order on Equivalence Relations
Informal description
For any type $\alpha$, the set of equivalence relations on $\alpha$ is equipped with a partial order $\leq$ where for two equivalence relations $r$ and $s$, $r \leq s$ if and only if $r(x,y)$ implies $s(x,y)$ for all $x, y \in \alpha$.
Setoid.le_def theorem
{r s : Setoid α} : r ≤ s ↔ ∀ {x y}, r x y → s x y
Full source 
theorem le_def {r s : Setoid α} : r ≤ s ↔ ∀ {x y}, r x y → s x y :=
  Iff.rfl
Characterization of Partial Order on Equivalence Relations
Informal description
For any two equivalence relations $r$ and $s$ on a type $\alpha$, the relation $r \leq s$ holds if and only if for all $x, y \in \alpha$, $r(x, y)$ implies $s(x, y)$.
Setoid.refl' theorem
(r : Setoid α) (x) : r x x
Full source 
@[refl]
theorem refl' (r : Setoid α) (x) : r x x := r.iseqv.refl x
Reflexivity of Equivalence Relations
Informal description
For any equivalence relation $r$ on a type $\alpha$ and any element $x \in \alpha$, the relation $r$ is reflexive at $x$, i.e., $r(x, x)$ holds.
Setoid.symm' theorem
(r : Setoid α) : ∀ {x y}, r x y → r y x
Full source 
@[symm]
theorem symm' (r : Setoid α) : ∀ {x y}, r x y → r y x := r.iseqv.symm
Symmetry of Equivalence Relations
Informal description
For any equivalence relation $r$ on a type $\alpha$ and any elements $x, y \in \alpha$, if $x$ is related to $y$ under $r$ (i.e., $r(x, y)$ holds), then $y$ is related to $x$ under $r$ (i.e., $r(y, x)$ holds).
Setoid.trans' theorem
(r : Setoid α) : ∀ {x y z}, r x y → r y z → r x z
Full source 
@[trans]
theorem trans' (r : Setoid α) : ∀ {x y z}, r x y → r y z → r x z := r.iseqv.trans
Transitivity of Equivalence Relations
Informal description
For any equivalence relation $r$ on a type $\alpha$ and any elements $x, y, z \in \alpha$, if $x$ is related to $y$ under $r$ and $y$ is related to $z$ under $r$, then $x$ is related to $z$ under $r$.
Setoid.comm' theorem
(s : Setoid α) {x y} : s x y ↔ s y x
Full source 
theorem comm' (s : Setoid α) {x y} : s x y ↔ s y x :=
  ⟨s.symm', s.symm'⟩
Symmetry of Equivalence Relations (Bidirectional Form)
Informal description
For any equivalence relation $s$ on a type $\alpha$ and any elements $x, y \in \alpha$, the relation $s(x, y)$ holds if and only if $s(y, x)$ holds.
Setoid.ker definition
(f : α → β) : Setoid α
Full source 
/-- The kernel of a function is an equivalence relation. -/
def ker (f : α → β) : Setoid α :=
  ⟨(· = ·) on f, eq_equivalence.comap f⟩
Kernel of a function as an equivalence relation
Informal description
Given a function $f : \alpha \to \beta$, the kernel of $f$ is the equivalence relation on $\alpha$ defined by $x \sim y$ if and only if $f(x) = f(y)$.
Setoid.ker_mk_eq theorem
(r : Setoid α) : ker (@Quotient.mk'' _ r) = r
Full source 
/-- The kernel of the quotient map induced by an equivalence relation r equals r. -/
@[simp]
theorem ker_mk_eq (r : Setoid α) : ker (@Quotient.mk'' _ r) = r :=
  ext fun _ _ => Quotient.eq
Kernel of Quotient Map Equals Original Equivalence Relation
Informal description
For any equivalence relation $r$ on a type $\alpha$, the kernel of the quotient map $\text{Quotient.mk} : \alpha \to \alpha / r$ is equal to $r$ itself. In other words, two elements $x, y \in \alpha$ are related by $r$ if and only if their images under the quotient map are equal.
Setoid.ker_apply_mk_out theorem
{f : α → β} (a : α) : f (⟦a⟧ : Quotient (Setoid.ker f)).out = f a
Full source 
theorem ker_apply_mk_out {f : α → β} (a : α) : f (⟦a⟧ : Quotient (Setoid.ker f)).out = f a :=
  @Quotient.mk_out _ (Setoid.ker f) a
Function Value Preservation under Quotient Kernel Representative Selection
Informal description
For any function $f : \alpha \to \beta$ and any element $a \in \alpha$, the value of $f$ at the representative of the equivalence class $[a]$ in the quotient by the kernel of $f$ is equal to $f(a)$. In other words, $f([a].\text{out}) = f(a)$, where $[a].\text{out}$ is a chosen representative of the equivalence class $[a]$.
Setoid.ker_def theorem
{f : α → β} {x y : α} : ker f x y ↔ f x = f y
Full source 
theorem ker_def {f : α → β} {x y : α} : kerker f x y ↔ f x = f y :=
  Iff.rfl
Characterization of Kernel Relation: $\ker f(x,y) \leftrightarrow f(x) = f(y)$
Informal description
For any function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the kernel relation $\ker f$ relates $x$ and $y$ if and only if $f(x) = f(y)$.
Setoid.prod definition
(r : Setoid α) (s : Setoid β) : Setoid (α × β)
Full source 
/-- 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`. -/
protected def prod (r : Setoid α) (s : Setoid β) :
    Setoid (α × β) where
  r x y := r x.1 y.1 ∧ s x.2 y.2
  iseqv :=
    ⟨fun x => ⟨r.refl' x.1, s.refl' x.2⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩,
      fun h₁ h₂ => ⟨r.trans' h₁.1 h₂.1, s.trans' h₁.2 h₂.2⟩⟩
Product of Equivalence Relations
Informal description
Given equivalence relations $r$ on a type $\alpha$ and $s$ on a type $\beta$, the product equivalence relation $r \times s$ on $\alpha \times \beta$ is defined such that two pairs $(x_1, x_2)$ and $(y_1, y_2)$ are related if and only if $x_1$ is related to $y_1$ under $r$ and $x_2$ is related to $y_2$ under $s$. The relation $r \times s$ satisfies the properties of an equivalence relation: 1. Reflexivity: $(x_1, x_2) \sim (x_1, x_2)$ for all $(x_1, x_2) \in \alpha \times \beta$. 2. Symmetry: If $(x_1, x_2) \sim (y_1, y_2)$, then $(y_1, y_2) \sim (x_1, x_2)$. 3. Transitivity: If $(x_1, x_2) \sim (y_1, y_2)$ and $(y_1, y_2) \sim (z_1, z_2)$, then $(x_1, x_2) \sim (z_1, z_2)$.
Setoid.prod_apply theorem
{r : Setoid α} {s : Setoid β} {x₁ x₂ : α} {y₁ y₂ : β} : @Setoid.r _ (r.prod s) (x₁, y₁) (x₂, y₂) ↔ (@Setoid.r _ r x₁ x₂ ∧ @Setoid.r _ s y₁ y₂)
Full source 
lemma prod_apply {r : Setoid α} {s : Setoid β} {x₁ x₂ : α} {y₁ y₂ : β} :
    @Setoid.r _ (r.prod s) (x₁, y₁) (x₂, y₂) ↔ (@Setoid.r _ r x₁ x₂ ∧ @Setoid.r _ s y₁ y₂) :=
  Iff.rfl
Characterization of Product Equivalence Relation
Informal description
For any equivalence relations $r$ on a type $\alpha$ and $s$ on a type $\beta$, and for any pairs $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, the relation $(x_1, y_1) \sim (x_2, y_2)$ holds in the product equivalence relation $r \times s$ if and only if $x_1 \sim x_2$ in $r$ and $y_1 \sim y_2$ in $s$.
Setoid.piSetoid_apply theorem
{ι : Sort*} {α : ι → Sort*} {r : ∀ i, Setoid (α i)} {x y : ∀ i, α i} : @Setoid.r _ (@piSetoid _ _ r) x y ↔ ∀ i, @Setoid.r _ (r i) (x i) (y i)
Full source 
lemma piSetoid_apply {ι : Sort*} {α : ι → Sort*} {r : ∀ i, Setoid (α i)} {x y : ∀ i, α i} :
    @Setoid.r _ (@piSetoid _ _ r) x y ↔ ∀ i, @Setoid.r _ (r i) (x i) (y i) :=
  Iff.rfl
Characterization of Product Equivalence Relation for Dependent Functions
Informal description
For any family of types $\{α_i\}_{i \in ι}$ equipped with equivalence relations $\{r_i\}_{i \in ι}$, and for any two elements $x, y \in \prod_{i \in ι} α_i$, the relation $x \sim y$ in the product equivalence relation holds if and only if $x_i \sim y_i$ holds in each component $i \in ι$ under the respective equivalence relation $r_i$.
Setoid.prodQuotientEquiv definition
(r : Setoid α) (s : Setoid β) : Quotient r × Quotient s ≃ Quotient (r.prod s)
Full source 
/-- A bijection between the product of two quotients and the quotient by the product of the
equivalence relations. -/
@[simps]
def prodQuotientEquiv (r : Setoid α) (s : Setoid β) :
    QuotientQuotient r × Quotient sQuotient r × Quotient s ≃ Quotient (r.prod s) where
  toFun | (x, y) => Quotient.map₂ Prod.mk (fun _ _ hx _ _ hy ↦ ⟨hx, hy⟩) x y
  invFun q := Quotient.liftOn' q (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2))
    fun x y hxy ↦ Prod.ext (by simpa using hxy.1) (by simpa using hxy.2)
  left_inv q := by
    rcases q with ⟨qa, qb⟩
    exact Quotient.inductionOn₂' qa qb fun _ _ ↦ rfl
  right_inv q := by
    simp only
    refine Quotient.inductionOn' q fun _ ↦ rfl
Bijection between product of quotients and quotient by product relation
Informal description
Given equivalence relations $r$ on a type $\alpha$ and $s$ on a type $\beta$, there is a natural bijection between the product of the quotient sets $\alpha / r \times \beta / s$ and the quotient of the product type $\alpha \times \beta$ by the product equivalence relation $r \times s$. The bijection is constructed as follows: - The forward map takes a pair of equivalence classes $([x]_r, [y]_s)$ and maps it to the equivalence class $[(x, y)]_{r \times s}$. - The inverse map takes an equivalence class $[(a, b)]_{r \times s}$ and returns the pair of equivalence classes $([a]_r, [b]_s)$.
Setoid.piQuotientEquiv definition
{ι : Sort*} {α : ι → Sort*} (r : ∀ i, Setoid (α i)) : (∀ i, Quotient (r i)) ≃ Quotient (@piSetoid _ _ r)
Full source 
/-- A bijection between an indexed product of quotients and the quotient by the product of the
equivalence relations. -/
@[simps]
noncomputable def piQuotientEquiv {ι : Sort*} {α : ι → Sort*} (r : ∀ i, Setoid (α i)) :
    (∀ i, Quotient (r i)) ≃ Quotient (@piSetoid _ _ r) where
  toFun x := Quotient.mk'' fun i ↦ (x i).out
  invFun q := Quotient.liftOn' q (fun x i ↦ Quotient.mk'' (x i)) fun x y hxy ↦ by
    ext i
    simpa using hxy i
  left_inv q := by
    ext i
    simp
  right_inv q := by
    refine Quotient.inductionOn' q fun _ ↦ ?_
    simp only [Quotient.liftOn'_mk'', Quotient.eq'']
    intro i
    change Setoid.r _ _
    rw [← Quotient.eq'']
    simp
Product of Quotients as Quotient of Products
Informal description
Given an indexed family of types $\alpha_i$ and equivalence relations $r_i$ on each $\alpha_i$, there is a natural bijection between the product of the quotients $\prod_i \alpha_i / r_i$ and the quotient of the product type $\prod_i \alpha_i$ by the product equivalence relation $\text{piSetoid}\ r$. The bijection is constructed as follows: - The forward map takes a family of equivalence classes $[x_i]_{r_i}$ and maps it to the equivalence class $[(\lambda i, x_i)]_{\text{piSetoid}\ r}$. - The inverse map takes an equivalence class $[f]_{\text{piSetoid}\ r}$ and returns the family of equivalence classes $[f(i)]_{r_i}$ for each index $i$. This bijection preserves the equivalence structure in both directions.
Setoid.instMin_mathlib instance
: Min (Setoid α)
Full source 
/-- The infimum of two equivalence relations. -/
instance : Min (Setoid α) :=
  ⟨fun r s =>
    ⟨fun x y => r x y ∧ s x y,
      ⟨fun x => ⟨r.refl' x, s.refl' x⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩, fun h1 h2 =>
        ⟨r.trans' h1.1 h2.1, s.trans' h1.2 h2.2⟩⟩⟩⟩
Existence of Minimal Equivalence Relation on a Type
Informal description
For any type $\alpha$, the set of equivalence relations on $\alpha$ has a minimal element with respect to the partial order of refinement. This minimal equivalence relation is the finest one, where each element is only related to itself.
Setoid.inf_def theorem
{r s : Setoid α} : ⇑(r ⊓ s) = ⇑r ⊓ ⇑s
Full source 
/-- The infimum of 2 equivalence relations r and s is the same relation as the infimum
    of the underlying binary operations. -/
theorem inf_def {r s : Setoid α} : ⇑(r ⊓ s) = ⇑r ⊓ ⇑s :=
  rfl
Infimum of Equivalence Relations as Infimum of Binary Relations
Informal description
For any two equivalence relations $r$ and $s$ on a type $\alpha$, the underlying binary relation of their infimum $r \sqcap s$ is equal to the infimum of the underlying binary relations of $r$ and $s$. In other words, $(r \sqcap s)(x, y) = r(x, y) \sqcap s(x, y)$ for all $x, y \in \alpha$.
Setoid.inf_iff_and theorem
{r s : Setoid α} {x y} : (r ⊓ s) x y ↔ r x y ∧ s x y
Full source 
theorem inf_iff_and {r s : Setoid α} {x y} : (r ⊓ s) x y ↔ r x y ∧ s x y :=
  Iff.rfl
Infimum of Equivalence Relations is Componentwise Conjunction
Informal description
For any two equivalence relations $r$ and $s$ on a type $\alpha$, and for any elements $x, y \in \alpha$, the infimum relation $r \sqcap s$ relates $x$ and $y$ if and only if both $r$ relates $x$ and $y$ and $s$ relates $x$ and $y$. In other words, $(r \sqcap s)(x, y) \leftrightarrow r(x, y) \land s(x, y)$.
Setoid.instInfSet instance
: InfSet (Setoid α)
Full source 
/-- The infimum of a set of equivalence relations. -/
instance : InfSet (Setoid α) :=
  ⟨fun S =>
    { r := fun x y => ∀ r ∈ S, r x y
      iseqv := ⟨fun x r _ => r.refl' x, fun h r hr => r.symm' <| h r hr, fun h1 h2 r hr =>
        r.trans' (h1 r hr) <| h2 r hr⟩ }⟩
Infimum of Equivalence Relations
Informal description
For any type $\alpha$, the set of equivalence relations on $\alpha$ has an infimum operation. Given a set $S$ of equivalence relations, their infimum is the equivalence relation where two elements are related if and only if they are related by every equivalence relation in $S$.
Setoid.sInf_def theorem
{s : Set (Setoid α)} : ⇑(sInf s) = sInf ((⇑) '' s)
Full source 
/-- 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. -/
theorem sInf_def {s : Set (Setoid α)} : ⇑(sInf s) = sInf ((⇑) '' s) := by
  ext
  simp only [sInf_image, iInf_apply, iInf_Prop_eq]
  rfl
Infimum of Equivalence Relations as Infimum of Binary Relations
Informal description
For any set $S$ of equivalence relations on a type $\alpha$, the underlying binary relation of the infimum of $S$ is equal to the infimum of the image of $S$ under the map that sends each equivalence relation to its underlying binary relation. In other words, for any $x, y \in \alpha$, we have $(\inf S)(x, y) \leftrightarrow \inf \{r(x, y) \mid r \in S\}$.
Setoid.instPartialOrder instance
: PartialOrder (Setoid α)
Full source 
instance : PartialOrder (Setoid α) where
  le := (· ≤ ·)
  lt r s := r ≤ s ∧ ¬s ≤ r
  le_refl _ _ _ := id
  le_trans _ _ _ hr hs _ _ h := hs <| hr h
  lt_iff_le_not_le _ _ := Iff.rfl
  le_antisymm _ _ h1 h2 := Setoid.ext fun _ _ => ⟨fun h => h1 h, fun h => h2 h⟩
Partial Order on Equivalence Relations
Informal description
For any type $\alpha$, the set of equivalence relations on $\alpha$ forms a partial order under the relation $\leq$, where $r \leq s$ if and only if $r(x,y)$ implies $s(x,y)$ for all $x, y \in \alpha$.
Setoid.completeLattice instance
: CompleteLattice (Setoid α)
Full source 
/-- The complete lattice of equivalence relations on a type, with bottom element `=`
    and top element the trivial equivalence relation. -/
instance completeLattice : CompleteLattice (Setoid α) :=
  { (completeLatticeOfInf (Setoid α)) fun _ =>
      ⟨fun _ hr _ _ h => h _ hr, fun _ hr _ _ h _ hr' => hr hr' h⟩ with
    inf := Min.min
    inf_le_left := fun _ _ _ _ h => h.1
    inf_le_right := fun _ _ _ _ h => h.2
    le_inf := fun _ _ _ h1 h2 _ _ h => ⟨h1 h, h2 h⟩
    top := ⟨fun _ _ => True, ⟨fun _ => trivial, fun h => h, fun h1 _ => h1⟩⟩
    le_top := fun _ _ _ _ => trivial
    bot := ⟨(· = ·), ⟨fun _ => rfl, fun h => h.symm, fun h1 h2 => h1.trans h2⟩⟩
    bot_le := fun r x _ h => h ▸ r.2.1 x }
Complete Lattice Structure on Equivalence Relations
Informal description
For any type $\alpha$, the set of equivalence relations on $\alpha$ forms a complete lattice. The bottom element is the equality relation $=$, and the top element is the trivial equivalence relation where all elements are related. The infimum of a set of equivalence relations is the finest equivalence relation coarser than all of them, and the supremum is the coarsest equivalence relation finer than all of them.
Setoid.top_def theorem
: ⇑(⊤ : Setoid α) = ⊤
Full source 
@[simp]
theorem top_def : ⇑(⊤ : Setoid α) = ⊤ :=
  rfl
Top Equivalence Relation is Universal Relation
Informal description
The top element in the complete lattice of equivalence relations on a type $\alpha$ is the relation that relates every pair of elements in $\alpha$, i.e., $\top(x,y)$ holds for all $x, y \in \alpha$.
Setoid.bot_def theorem
: ⇑(⊥ : Setoid α) = (· = ·)
Full source 
@[simp]
theorem bot_def : ⇑(⊥ : Setoid α) = (· = ·) :=
  rfl
Bottom Equivalence Relation is Equality
Informal description
The bottom element in the complete lattice of equivalence relations on a type $\alpha$ is the equality relation, i.e., $\bot(x,y)$ holds if and only if $x = y$ for all $x, y \in \alpha$.
Setoid.sInf_equiv theorem
{S : Set (Setoid α)} {x y : α} : letI := sInf S x ≈ y ↔ ∀ s ∈ S, s x y
Full source 
lemma sInf_equiv {S : Set (Setoid α)} {x y : α} :
    letI := sInf S
    x ≈ yx ≈ y ↔ ∀ s ∈ S, s x y := Iff.rfl
Characterization of Infimum of Equivalence Relations
Informal description
Let $S$ be a set of equivalence relations on a type $\alpha$, and let $x, y$ be elements of $\alpha$. Then, under the infimum equivalence relation $\bigsqcap S$, $x$ is equivalent to $y$ if and only if for every equivalence relation $s \in S$, $x$ is related to $y$ under $s$.
Setoid.sInf_iff theorem
{S : Set (Setoid α)} {x y : α} : sInf S x y ↔ ∀ s ∈ S, s x y
Full source 
lemma sInf_iff {S : Set (Setoid α)} {x y : α} :
    sInfsInf S x y ↔ ∀ s ∈ S, s x y := Iff.rfl
Characterization of Infimum of Equivalence Relations
Informal description
For any set $S$ of equivalence relations on a type $\alpha$ and any elements $x, y \in \alpha$, the infimum of $S$ relates $x$ and $y$ if and only if every equivalence relation in $S$ relates $x$ and $y$. In symbols: \[ \bigwedge S\, x\, y \leftrightarrow \forall s \in S,\, s\, x\, y \]
Setoid.quotient_mk_sInf_eq theorem
{S : Set (Setoid α)} {x y : α} : Quotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s x y
Full source 
lemma quotient_mk_sInf_eq {S : Set (Setoid α)} {x y : α} :
    Quotient.mkQuotient.mk (sInf S) x = Quotient.mk (sInf S) y ↔ ∀ s ∈ S, s x y := by
  simp [sInf_iff]
Equivalence Classes under Infimum of Equivalence Relations
Informal description
For any type $\alpha$, a set $S$ of equivalence relations on $\alpha$, and elements $x, y \in \alpha$, the equivalence classes of $x$ and $y$ under the infimum of $S$ are equal if and only if $x$ and $y$ are related by every equivalence relation in $S$. In other words, \[ [x]_{\bigwedge S} = [y]_{\bigwedge S} \leftrightarrow \forall s \in S, s(x, y). \]
Setoid.map_of_le definition
{s t : Setoid α} (h : s ≤ t) : Quotient s → Quotient t
Full source 
/-- The map induced between quotients by a setoid inequality. -/
def map_of_le {s t : Setoid α} (h : s ≤ t) : Quotient s → Quotient t :=
  Quotient.map' id h
Induced map between quotients by a setoid inequality
Informal description
Given two equivalence relations $s$ and $t$ on a type $\alpha$ such that $s \leq t$ (i.e., $s(x,y)$ implies $t(x,y)$ for all $x, y \in \alpha$), the function maps a quotient element of $s$ to the corresponding quotient element of $t$ by the identity function.
Setoid.map_sInf definition
{S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) : Quotient (sInf S) → Quotient s
Full source 
/-- The map from the quotient of the infimum of a set of setoids into the quotient
by an element of this set. -/
def map_sInf {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S) :
    Quotient (sInf S) → Quotient s :=
  Setoid.map_of_le fun _ _ a ↦ a s h
Quotient map from infimum of equivalence relations to a member equivalence relation
Informal description
Given a set $S$ of equivalence relations on a type $\alpha$ and an equivalence relation $s \in S$, the function maps an equivalence class of the infimum of $S$ to the corresponding equivalence class of $s$. More precisely, for any $x \in \alpha$, the function sends the equivalence class $[x]_{\bigwedge S}$ to $[x]_s$, where $\bigwedge S$ denotes the infimum of the set $S$ of equivalence relations.
Setoid.eqvGen_eq theorem
(r : α → α → Prop) : EqvGen.setoid r = sInf {s : Setoid α | ∀ ⦃x y⦄, r x y → s x y}
Full source 
/-- The inductively defined equivalence closure of a binary relation r is the infimum
    of the set of all equivalence relations containing r. -/
theorem eqvGen_eq (r : α → α → Prop) :
    EqvGen.setoid r = sInf { s : Setoid α | ∀ ⦃x y⦄, r x y → s x y } :=
  le_antisymm
    (fun _ _ H =>
      EqvGen.rec (fun _ _ h _ hs => hs h) (refl' _) (fun _ _ _ => symm' _)
        (fun _ _ _ _ _ => trans' _) H)
    (sInf_le fun _ _ h => EqvGen.rel _ _ h)
Equivalence Closure as Infimum of Containing Equivalence Relations
Informal description
For any binary relation $r$ on a type $\alpha$, the equivalence closure of $r$ (denoted by $\text{EqvGen.setoid}\, r$) is equal to the infimum of all equivalence relations on $\alpha$ that contain $r$. In other words, $\text{EqvGen.setoid}\, r = \bigwedge \{s \text{ equivalence relation on } \alpha \mid \forall x y, r(x,y) \to s(x,y)\}$.
Setoid.sup_eq_eqvGen theorem
(r s : Setoid α) : r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y
Full source 
/-- 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 sup_eq_eqvGen (r s : Setoid α) :
    r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y := by
  rw [eqvGen_eq]
  apply congr_arg sInf
  simp only [le_def, or_imp, ← forall_and]
Supremum of Equivalence Relations as Equivalence Closure of Union
Informal description
For any two equivalence relations $r$ and $s$ on a type $\alpha$, their supremum $r \sqcup s$ in the lattice of equivalence relations is equal to the equivalence closure of the binary relation defined by $x \sim y$ if and only if $r(x,y)$ or $s(x,y)$ holds. In other words, $r \sqcup s = \text{EqvGen}(\lambda x y, r(x,y) \lor s(x,y))$.
Setoid.sup_def theorem
{r s : Setoid α} : r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s)
Full source 
/-- The supremum of 2 equivalence relations r and s is the equivalence closure of the
    supremum of the underlying binary operations. -/
theorem sup_def {r s : Setoid α} : r ⊔ s = EqvGen.setoid (⇑r ⊔ ⇑s) := by
  rw [sup_eq_eqvGen]; rfl
Supremum of Equivalence Relations as Equivalence Closure of Pointwise Supremum
Informal description
For any two equivalence relations $r$ and $s$ on a type $\alpha$, their supremum $r \sqcup s$ in the lattice of equivalence relations is equal to the equivalence closure of the pointwise supremum of the underlying binary relations of $r$ and $s$. In other words, $r \sqcup s = \text{EqvGen}(r \sqcup s)$ where the second $\sqcup$ denotes the pointwise supremum of relations.
Setoid.sSup_eq_eqvGen theorem
(S : Set (Setoid α)) : sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r x y
Full source 
/-- 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 sSup_eq_eqvGen (S : Set (Setoid α)) :
    sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r x y := by
  rw [eqvGen_eq]
  apply congr_arg sInf
  simp only [upperBounds, le_def, and_imp, exists_imp]
  ext
  exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩
Supremum of Equivalence Relations as Equivalence Closure of Their Union
Informal description
For any set $S$ of equivalence relations on a type $\alpha$, the supremum of $S$ in the lattice of equivalence relations is equal to the equivalence closure of the binary relation defined by $x \sim y$ if and only if there exists an equivalence relation $r \in S$ such that $r(x,y)$ holds. In other words, $\bigvee S = \text{EqvGen}(\lambda x y, \exists r \in S, r(x,y))$.
Setoid.sSup_def theorem
{s : Set (Setoid α)} : sSup s = EqvGen.setoid (sSup ((⇑) '' s))
Full source 
/-- 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. -/
theorem sSup_def {s : Set (Setoid α)} : sSup s = EqvGen.setoid (sSup ((⇑) '' s)) := by
  rw [sSup_eq_eqvGen, sSup_image]
  congr with (x y)
  simp only [iSup_apply, iSup_Prop_eq, exists_prop]
Supremum of Equivalence Relations as Equivalence Closure of Union of Relations
Informal description
For any set $S$ of equivalence relations on a type $\alpha$, the supremum of $S$ in the lattice of equivalence relations is equal to the equivalence closure of the supremum of the image of $S$ under the map to their underlying binary relations. In other words, $\bigvee S = \text{EqvGen}(\bigvee \{r.r \mid r \in S\})$, where $r.r$ denotes the binary relation underlying the equivalence relation $r$.
Setoid.eqvGen_of_setoid theorem
(r : Setoid α) : EqvGen.setoid r.r = r
Full source 
/-- The equivalence closure of an equivalence relation r is r. -/
@[simp]
theorem eqvGen_of_setoid (r : Setoid α) : EqvGen.setoid r.r = r :=
  le_antisymm (by rw [eqvGen_eq]; exact sInf_le fun _ _ => id) EqvGen.rel
Equivalence Closure of an Equivalence Relation is Itself
Informal description
For any equivalence relation $r$ on a type $\alpha$, the equivalence closure of the underlying binary relation of $r$ is equal to $r$ itself. In other words, if $r$ is already an equivalence relation, then $\text{EqvGen.setoid}\, r.r = r$.
Setoid.eqvGen_idem theorem
(r : α → α → Prop) : EqvGen.setoid (EqvGen.setoid r) = EqvGen.setoid r
Full source 
/-- Equivalence closure is idempotent. -/
theorem eqvGen_idem (r : α → α → Prop) : EqvGen.setoid (EqvGen.setoid r) = EqvGen.setoid r :=
  eqvGen_of_setoid _
Idempotence of Equivalence Closure
Informal description
For any binary relation $r$ on a type $\alpha$, the equivalence closure of the equivalence closure of $r$ is equal to the equivalence closure of $r$. In other words, the operation of taking the equivalence closure is idempotent: $\text{EqvGen.setoid}\, (\text{EqvGen.setoid}\, r) = \text{EqvGen.setoid}\, r$.
Setoid.eqvGen_le theorem
{r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s x y) : EqvGen.setoid r ≤ s
Full source 
/-- The equivalence closure of a binary relation r is contained in any equivalence
    relation containing r. -/
theorem eqvGen_le {r : α → α → Prop} {s : Setoid α} (h : ∀ x y, r x y → s x y) :
    EqvGen.setoid r ≤ s := by rw [eqvGen_eq]; exact sInf_le h
Equivalence Closure is the Smallest Containing Equivalence Relation
Informal description
For any binary relation $r$ on a type $\alpha$ and any equivalence relation $s$ on $\alpha$, if $r(x,y)$ implies $s(x,y)$ for all $x, y \in \alpha$, then the equivalence closure of $r$ is contained in $s$. In other words, if $r \subseteq s$ as binary relations, then $\text{EqvGen.setoid}\, r \leq s$ in the lattice of equivalence relations.
Setoid.eqvGen_mono theorem
{r s : α → α → Prop} (h : ∀ x y, r x y → s x y) : EqvGen.setoid r ≤ EqvGen.setoid s
Full source 
/-- Equivalence closure of binary relations is monotone. -/
theorem eqvGen_mono {r s : α → α → Prop} (h : ∀ x y, r x y → s x y) :
    EqvGen.setoid r ≤ EqvGen.setoid s :=
  eqvGen_le fun _ _ hr => EqvGen.rel _ _ <| h _ _ hr
Monotonicity of Equivalence Closure
Informal description
For any two binary relations $r$ and $s$ on a type $\alpha$, if $r(x,y)$ implies $s(x,y)$ for all $x, y \in \alpha$, then the equivalence closure of $r$ is contained in the equivalence closure of $s$. In other words, if $r \subseteq s$ as binary relations, then $\text{EqvGen.setoid}\, r \leq \text{EqvGen.setoid}\, s$ in the lattice of equivalence relations.
Setoid.gi definition
: @GaloisInsertion (α → α → Prop) (Setoid α) _ _ EqvGen.setoid (⇑)
Full source 
/-- There is a Galois insertion of equivalence relations on α into binary relations
    on α, with equivalence closure the lower adjoint. -/
def gi : @GaloisInsertion (α → α → Prop) (Setoid α) _ _ EqvGen.setoid (⇑) where
  choice r _ := EqvGen.setoid r
  gc _ s := ⟨fun H _ _ h => H <| EqvGen.rel _ _ h, fun H => eqvGen_of_setoid s ▸ eqvGen_mono H⟩
  le_l_u x := (eqvGen_of_setoid x).symm ▸ le_refl x
  choice_eq _ _ := rfl
Galois insertion between binary relations and equivalence relations
Informal description
There is a Galois insertion between the set of binary relations on a type $\alpha$ and the set of equivalence relations on $\alpha$, where the equivalence closure operation $\text{EqvGen.setoid}$ is the lower adjoint and the identity map is the upper adjoint. This means that for any binary relation $r$ and any equivalence relation $s$ on $\alpha$, the equivalence closure of $r$ is contained in $s$ if and only if $r$ is contained in $s$ when viewed as a binary relation.
Setoid.injective_iff_ker_bot theorem
(f : α → β) : Injective f ↔ ker f = ⊥
Full source 
/-- A function from α to β is injective iff its kernel is the bottom element of the complete lattice
    of equivalence relations on α. -/
theorem injective_iff_ker_bot (f : α → β) : InjectiveInjective f ↔ ker f = ⊥ :=
  (@eq_bot_iff (Setoid α) _ _ (ker f)).symm
Injectivity Criterion via Kernel Equivalence Relation: $f$ injective $\iff$ $\ker f = {=}$
Informal description
A function $f \colon \alpha \to \beta$ is injective if and only if its kernel equivalence relation $\ker f$ is equal to the bottom element of the complete lattice of equivalence relations on $\alpha$, which is the equality relation $=$.
Setoid.ker_iff_mem_preimage theorem
{f : α → β} {x y} : ker f x y ↔ x ∈ f ⁻¹' {f y}
Full source 
/-- The elements related to x ∈ α by the kernel of f are those in the preimage of f(x) under f. -/
theorem ker_iff_mem_preimage {f : α → β} {x y} : kerker f x y ↔ x ∈ f ⁻¹' {f y} :=
  Iff.rfl
Characterization of Kernel Relation via Preimage: $\ker f(x,y) \leftrightarrow x \in f^{-1}(\{f(y)\})$
Informal description
For any function $f : \alpha \to \beta$ and elements $x, y \in \alpha$, the relation $\ker f(x, y)$ holds (i.e., $x$ is equivalent to $y$ under the kernel equivalence relation of $f$) if and only if $x$ belongs to the preimage of $\{f(y)\}$ under $f$, i.e., $f(x) = f(y)$.
Setoid.liftEquiv definition
(r : Setoid α) : { f : α → β // r ≤ ker f } ≃ (Quotient r → β)
Full source 
/-- Equivalence between functions `α → β` such that `r x y → f x = f y` and functions
`quotient r → β`. -/
def liftEquiv (r : Setoid α) : { f : α → β // r ≤ ker f }{ f : α → β // r ≤ ker f } ≃ (Quotient r → β) where
  toFun f := Quotient.lift (f : α → β) f.2
  invFun f := ⟨f ∘ Quotient.mk'', fun x y h => by simp [ker_def, Quotient.sound' h]⟩
  left_inv := fun ⟨_, _⟩ => Subtype.eq <| funext fun _ => rfl
  right_inv _ := funext fun x => Quotient.inductionOn' x fun _ => rfl
Equivalence between relation-respecting functions and quotient functions
Informal description
Given an equivalence relation $r$ on a type $\alpha$, there is a natural equivalence between: 1. The set of functions $f : \alpha \to \beta$ that respect $r$ (i.e., $r(x,y) \Rightarrow f(x) = f(y)$) 2. The set of functions from the quotient space $\alpha / r$ to $\beta$ The equivalence is given by lifting a function $f$ respecting $r$ to a function on the quotient, and conversely, any function on the quotient can be composed with the canonical projection $\alpha \to \alpha / r$ to obtain a function respecting $r$.
Setoid.lift_unique theorem
{r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quotient r → β) (Hg : f = g ∘ Quotient.mk'') : Quotient.lift f H = g
Full source 
/-- The uniqueness part of the universal property for quotients of an arbitrary type. -/
theorem lift_unique {r : Setoid α} {f : α → β} (H : r ≤ ker f) (g : Quotient r → β)
    (Hg : f = g ∘ Quotient.mk'') : Quotient.lift f H = g := by
  ext ⟨x⟩
  rw [← Quotient.mk, Quotient.lift_mk f H, Hg, Function.comp_apply, Quotient.mk''_eq_mk]
Uniqueness of Lift to Quotient via Kernel Condition
Informal description
Let $r$ be an equivalence relation on a type $\alpha$, and let $f : \alpha \to \beta$ be a function such that $r$ is finer than the kernel of $f$ (i.e., $r(x,y)$ implies $f(x) = f(y)$ for all $x, y \in \alpha$). If $g : \text{Quotient}(r) \to \beta$ is a function satisfying $f = g \circ \text{Quotient.mk}$, then the lift of $f$ to the quotient $\text{Quotient}(r)$ is equal to $g$.
Setoid.ker_lift_injective theorem
(f : α → β) : Injective (@Quotient.lift _ _ (ker f) f fun _ _ h => h)
Full source 
/-- Given a map f from α to β, the natural map from the quotient of α by the kernel of f is
    injective. -/
theorem ker_lift_injective (f : α → β) : Injective (@Quotient.lift _ _ (ker f) f fun _ _ h => h) :=
  fun x y => Quotient.inductionOn₂' x y fun _ _ h => Quotient.sound' h
Injectivity of the quotient map induced by the kernel of a function
Informal description
Given a function $f \colon \alpha \to \beta$, the induced map from the quotient of $\alpha$ by the kernel equivalence relation of $f$ to $\beta$ is injective.
Setoid.ker_eq_lift_of_injective theorem
{r : Setoid α} (f : α → β) (H : ∀ x y, r x y → f x = f y) (h : Injective (Quotient.lift f H)) : ker f = r
Full source 
/-- 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. -/
theorem ker_eq_lift_of_injective {r : Setoid α} (f : α → β) (H : ∀ x y, r x y → f x = f y)
    (h : Injective (Quotient.lift f H)) : ker f = r :=
  le_antisymm
    (fun x y hk =>
      Quotient.exact <| h <| show Quotient.lift f H ⟦x⟧ = Quotient.lift f H ⟦y⟧ from hk)
    H
Kernel Equivalence Relation Characterization via Injectivity of Quotient Lift
Informal description
Let $r$ be an equivalence relation on a type $\alpha$, and let $f \colon \alpha \to \beta$ be a function such that $r(x,y)$ implies $f(x) = f(y)$ for all $x, y \in \alpha$. If the induced map $\text{Quotient}(r) \to \beta$ is injective, then the kernel equivalence relation of $f$ is equal to $r$.
Setoid.quotientKerEquivRange definition
: Quotient (ker f) ≃ Set.range f
Full source 
/-- The first isomorphism theorem for sets: the quotient of α by the kernel of a function f
    bijects with f's image. -/
noncomputable def quotientKerEquivRange : QuotientQuotient (ker f) ≃ Set.range f :=
  Equiv.ofBijective
    ((@Quotient.lift _ (Set.range f) (ker f) fun x => ⟨f x, Set.mem_range_self x⟩) fun _ _ h =>
      Subtype.ext_val h)
    ⟨fun x y h => ker_lift_injective f <| by rcases x with ⟨⟩; rcases y with ⟨⟩; injections,
      fun ⟨_, z, hz⟩ =>
      ⟨@Quotient.mk'' _ (ker f) z, Subtype.ext_iff_val.2 hz⟩⟩
First isomorphism theorem for sets (quotient by kernel bijects with image)
Informal description
The first isomorphism theorem for sets: The quotient of $\alpha$ by the kernel of a function $f$ is in bijection with the image of $f$. More precisely, there exists a bijection between the quotient set $\alpha / \ker f$ and the range $\text{range } f \subseteq \beta$.
Setoid.quotientKerEquivOfRightInverse definition
(g : β → α) (hf : Function.RightInverse g f) : Quotient (ker f) ≃ β
Full source 
/-- If `f` has a computable right-inverse, then the quotient by its kernel is equivalent to its
domain. -/
@[simps]
def quotientKerEquivOfRightInverse (g : β → α) (hf : Function.RightInverse g f) :
    QuotientQuotient (ker f) ≃ β where
  toFun a := (Quotient.liftOn' a f) fun _ _ => id
  invFun b := Quotient.mk'' (g b)
  left_inv a := Quotient.inductionOn' a fun a => Quotient.sound' <| hf (f a)
  right_inv := hf
Quotient by kernel equivalence relation is equivalent to codomain when a right inverse exists
Informal description
Given a function $f : \alpha \to \beta$ with a computable right inverse $g : \beta \to \alpha$ (i.e., $f \circ g = \text{id}_\beta$), the quotient of $\alpha$ by the kernel equivalence relation of $f$ is in bijection with $\beta$. The bijection maps each equivalence class $[a]$ to $f(a)$ and its inverse maps each $b \in \beta$ to the equivalence class of $g(b)$.
Setoid.quotientKerEquivOfSurjective definition
(hf : Surjective f) : Quotient (ker f) ≃ β
Full source 
/-- 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. -/
noncomputable def quotientKerEquivOfSurjective (hf : Surjective f) : QuotientQuotient (ker f) ≃ β :=
  quotientKerEquivOfRightInverse _ (Function.surjInv hf) (rightInverse_surjInv hf)
First isomorphism theorem for sets (surjective case)
Informal description
Given a surjective function $f : \alpha \to \beta$, the quotient of $\alpha$ by the kernel equivalence relation of $f$ is in bijection with $\beta$. The bijection maps each equivalence class $[a]$ to $f(a)$ and its inverse maps each $b \in \beta$ to the equivalence class of the surjective inverse of $f$ evaluated at $b$.
Setoid.map definition
(r : Setoid α) (f : α → β) : Setoid β
Full source 
/-- 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`.' -/
def map (r : Setoid α) (f : α → β) : Setoid β :=
  Relation.EqvGen.setoid (Relation.Map r f f)
Induced equivalence relation on the codomain of a function
Informal description
Given an equivalence relation \( r \) on a type \( \alpha \) and a function \( f : \alpha \to \beta \), the equivalence relation `Setoid.map r f` on \( \beta \) is the smallest equivalence relation such that \( f(x) \) is related to \( f(y) \) whenever \( x \) is related to \( y \) under \( r \). In other words, it is the equivalence closure of the relation on \( f \)'s image defined by \( x \approx y \) if and only if the elements of \( f^{-1}(x) \) are related to the elements of \( f^{-1}(y) \) by \( r \).
Setoid.mapOfSurjective definition
(r : Setoid α) (f : α → β) (h : ker f ≤ r) (hf : Surjective f) : Setoid β
Full source 
/-- 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. -/
def mapOfSurjective (r : Setoid α) (f : α → β) (h : ker f ≤ r) (hf : Surjective f) : Setoid β :=
  ⟨Relation.Map r f f, Relation.map_equivalence r.iseqv f hf h⟩
Equivalence relation induced by a surjective function with kernel condition
Informal description
Given an equivalence relation $r$ on a type $\alpha$, a surjective function $f : \alpha \to \beta$, and a proof that the kernel of $f$ is contained in $r$, the equivalence relation on $\beta$ induced by $f$ is defined by $x \approx y$ if and only if for any $a \in f^{-1}(x)$ and $b \in f^{-1}(y)$, $a$ is related to $b$ under $r$.
Setoid.mapOfSurjective_eq_map theorem
(h : ker f ≤ r) (hf : Surjective f) : map r f = mapOfSurjective r f h hf
Full source 
/-- A special case of the equivalence closure of an equivalence relation r equalling r. -/
theorem mapOfSurjective_eq_map (h : ker f ≤ r) (hf : Surjective f) :
    map r f = mapOfSurjective r f h hf := by
  rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]; rfl
Equality of Induced Equivalence Relations via Surjective Functions
Informal description
Given an equivalence relation $r$ on a type $\alpha$, a surjective function $f : \alpha \to \beta$, and a proof that the kernel of $f$ is contained in $r$, the equivalence relation on $\beta$ induced by $f$ via `map` is equal to the one induced via `mapOfSurjective`. That is, $\text{map}\,r\,f = \text{mapOfSurjective}\,r\,f\,h\,hf$.
Setoid.comap abbrev
(f : α → β) (r : Setoid β) : Setoid α
Full source 
/-- 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]. -/
abbrev comap (f : α → β) (r : Setoid β) : Setoid α :=
  ⟨r on f, r.iseqv.comap _⟩
Pullback of an Equivalence Relation via a Function
Informal description
Given a function $f : \alpha \to \beta$ and an equivalence relation $r$ on $\beta$, the *pullback* (or *preimage*) equivalence relation on $\alpha$ is defined by $x \sim y$ if and only if $f(x) \sim_r f(y)$.
Setoid.comap_rel theorem
(f : α → β) (r : Setoid β) (x y : α) : comap f r x y ↔ r (f x) (f y)
Full source 
theorem comap_rel (f : α → β) (r : Setoid β) (x y : α) : comapcomap f r x y ↔ r (f x) (f y) :=
  Iff.rfl
Characterization of Pullback Equivalence Relation via Function Application
Informal description
Given a function $f : \alpha \to \beta$ and an equivalence relation $r$ on $\beta$, for any elements $x, y \in \alpha$, the pullback equivalence relation $\text{comap}\,f\,r$ relates $x$ and $y$ if and only if $r$ relates $f(x)$ and $f(y)$. In other words, $x \sim_{\text{comap}\,f\,r} y \leftrightarrow f(x) \sim_r f(y)$.
Setoid.comap_eq theorem
{f : α → β} {r : Setoid β} : comap f r = ker (@Quotient.mk'' _ r ∘ f)
Full source 
/-- 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`. -/
theorem comap_eq {f : α → β} {r : Setoid β} : comap f r = ker (@Quotient.mk'' _ r ∘ f) :=
  ext fun x y => show _ ↔ ⟦_⟧ = ⟦_⟧ by rw [Quotient.eq]; rfl
Pullback Equivalence Relation Equals Kernel of Quotient Composition
Informal description
Given a function $f : \alpha \to \beta$ and an equivalence relation $r$ on $\beta$, the pullback equivalence relation on $\alpha$ via $f$ is equal to the kernel of the composition of $f$ with the quotient map of $r$. In other words, for any $x, y \in \alpha$, we have $x \sim y$ under the pullback relation if and only if $[f(x)]_r = [f(y)]_r$ in the quotient $\beta/r$.
Setoid.comapQuotientEquiv definition
(f : α → β) (r : Setoid β) : Quotient (comap f r) ≃ Set.range (@Quotient.mk'' _ r ∘ f)
Full source 
/-- The second isomorphism theorem for sets. -/
noncomputable def comapQuotientEquiv (f : α → β) (r : Setoid β) :
    QuotientQuotient (comap f r) ≃ Set.range (@Quotient.mk'' _ r ∘ f) :=
  (Quotient.congrRight <| Setoid.ext_iff.1 comap_eq).trans <| quotientKerEquivRange <|
    Quotient.mk''Quotient.mk'' ∘ f
Second isomorphism theorem for sets (quotient by pullback equivalence bijects with image of quotient map)
Informal description
Given a function $f : \alpha \to \beta$ and an equivalence relation $r$ on $\beta$, there is a natural equivalence between the quotient of $\alpha$ by the pullback equivalence relation $\text{comap}\,f\,r$ and the range of the composition of $f$ with the quotient map $\text{Quotient.mk''}_r : \beta \to \text{Quotient}\,r$. In other words, the quotient set $\alpha / \text{comap}\,f\,r$ is in bijection with the image of the map $[f]_r : \alpha \to \text{Quotient}\,r$ defined by $[f]_r(x) = [f(x)]_r$.
Setoid.quotientQuotientEquivQuotient definition
(s : Setoid α) (h : r ≤ s) : Quotient (ker (Quot.mapRight h)) ≃ Quotient s
Full source 
/-- The third isomorphism theorem for sets. -/
def quotientQuotientEquivQuotient (s : Setoid α) (h : r ≤ s) :
    QuotientQuotient (ker (Quot.mapRight h)) ≃ Quotient s where
  toFun x :=
    (Quotient.liftOn' x fun w =>
        (Quotient.liftOn' w (@Quotient.mk'' _ s)) fun _ _ H => Quotient.sound <| h H)
      fun x y => Quotient.inductionOn₂' x y fun _ _ H => show @Quot.mk _ _ _ = @Quot.mk _ _ _ from H
  invFun x :=
    (Quotient.liftOn' x fun w => @Quotient.mk'' _ (ker <| Quot.mapRight h) <| @Quotient.mk'' _ r w)
      fun _ _ H => Quotient.sound' <| show @Quot.mk _ _ _ = @Quot.mk _ _ _ from Quotient.sound H
  left_inv x :=
    Quotient.inductionOn' x fun y => Quotient.inductionOn' y fun w => by show ⟦_⟧ = _; rfl
  right_inv x := Quotient.inductionOn' x fun y => by show ⟦_⟧ = _; rfl
Third Isomorphism Theorem for Quotients
Informal description
Given two equivalence relations $r$ and $s$ on a type $\alpha$ such that $r \leq s$ (i.e., $r$ is finer than $s$), there is a natural equivalence between the quotient of the quotient of $\alpha$ by $r$ and the quotient of $\alpha$ by $s$. More precisely, the equivalence relation $\ker(\text{Quot.mapRight } h)$ on $\text{Quotient } r$ is defined by identifying two equivalence classes $[x]_r$ and $[y]_r$ if $[x]_s = [y]_s$, and the theorem states that $\text{Quotient } (\ker(\text{Quot.mapRight } h))$ is equivalent to $\text{Quotient } s$.
Setoid.correspondence definition
(r : Setoid α) : { s // r ≤ s } ≃o Setoid (Quotient r)
Full source 
/-- 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`. -/
def correspondence (r : Setoid α) : { s // r ≤ s }{ s // r ≤ s } ≃o Setoid (Quotient r) where
  toFun s := ⟨Quotient.lift₂ s.1.1 fun _ _ _ _ h₁ h₂ ↦ Eq.propIntro
      (fun h ↦ s.1.trans' (s.1.trans' (s.1.symm' (s.2 h₁)) h) (s.2 h₂))
      (fun h ↦ s.1.trans' (s.1.trans' (s.2 h₁) h) (s.1.symm' (s.2 h₂))),
    ⟨Quotient.ind s.1.2.1, fun {x y} ↦ Quotient.inductionOn₂ x y fun _ _ ↦ s.1.2.2,
      fun {x y z} ↦ Quotient.inductionOn₃ x y z fun _ _ _ ↦ s.1.2.3⟩⟩
  invFun s := ⟨comap Quotient.mk' s, fun x y h => by rw [comap_rel, Quotient.eq'.2 h]⟩
  left_inv _ := rfl
  right_inv _ := ext fun x y ↦ Quotient.inductionOn₂ x y fun _ _ ↦ Iff.rfl
  map_rel_iff' :=
    ⟨fun h x y hs ↦ @h ⟦x⟧ ⟦y⟧ hs, fun h x y ↦ Quotient.inductionOn₂ x y fun _ _ hs ↦ h hs⟩
Correspondence Theorem for Equivalence Relations
Informal description
Given an equivalence relation $r$ on a type $\alpha$, there is an order-preserving bijection between the set of equivalence relations on $\alpha$ containing $r$ and the set of equivalence relations on the quotient $\alpha / r$. More precisely, the bijection maps an equivalence relation $s$ (with $r \leq s$) to the equivalence relation on $\alpha / r$ defined by lifting $s$ via the quotient map, and its inverse maps an equivalence relation on $\alpha / r$ to its pullback along the quotient map.
Setoid.sigmaQuotientEquivOfLe definition
{r s : Setoid α} (hle : r ≤ s) : (Σ q : Quotient s, Quotient (r.comap (Subtype.val : Quotient.mk s ⁻¹' { q } → α))) ≃ Quotient r
Full source 
/-- 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`. -/
def sigmaQuotientEquivOfLe {r s : Setoid α} (hle : r ≤ s) :
    (Σ q : Quotient s, Quotient (r.comap (Subtype.val : Quotient.mk s ⁻¹' {q} → α))) ≃
      Quotient r :=
  .trans (.symm <| .sigmaCongrRight fun _ ↦ .subtypeQuotientEquivQuotientSubtype
      (s₁ := r) (s₂ := r.comap Subtype.val) _ _ (fun _ ↦ Iff.rfl) fun _ _ ↦ Iff.rfl)
    (.sigmaFiberEquiv fun a ↦ a.lift (Quotient.mk s) fun _ _ h ↦ Quotient.sound <| hle h)
Bijection between nested equivalence quotients
Informal description
Given two equivalence relations $r$ and $s$ on a type $\alpha$ with $r \leq s$, there is a bijection between the dependent sum of quotients (where for each equivalence class $q$ of $s$, we take the quotient by $r$ restricted to the preimage of $q$) and the quotient by $r$. More precisely, the bijection is between: 1. The dependent sum type $\Sigma (q : \alpha / s), (\text{Quotient.mk } s)^{-1}\{q\} / r$, where each fiber is the quotient of the preimage of $q$ under the relation $r$. 2. The quotient $\alpha / r$.
Quotient.subsingleton_iff theorem
{s : Setoid α} : Subsingleton (Quotient s) ↔ s = ⊤
Full source 
@[simp]
theorem Quotient.subsingleton_iff {s : Setoid α} : SubsingletonSubsingleton (Quotient s) ↔ s = ⊤ := by
  simp only [_root_.subsingleton_iff, eq_top_iff, Setoid.le_def, Setoid.top_def, Pi.top_apply,
    forall_const]
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quotient.mk'_surjective.forall.trans (forall_congr' fun b => ?_)
  simp_rw [Prop.top_eq_true, true_implies, Quotient.eq']
Quotient is Subsingleton iff Equivalence Relation is Trivial
Informal description
For any equivalence relation $s$ on a type $\alpha$, the quotient $\alpha / s$ is a subsingleton (i.e., has at most one element) if and only if $s$ is the trivial equivalence relation where all elements are related (i.e., $s = \top$).
Quot.subsingleton_iff theorem
(r : α → α → Prop) : Subsingleton (Quot r) ↔ Relation.EqvGen r = ⊤
Full source 
theorem Quot.subsingleton_iff (r : α → α → Prop) :
    SubsingletonSubsingleton (Quot r) ↔ Relation.EqvGen r = ⊤ := by
  simp only [_root_.subsingleton_iff, _root_.eq_top_iff, Pi.le_def, Pi.top_apply, forall_const]
  refine Quot.mk_surjective.forall.trans (forall_congr' fun a => ?_)
  refine Quot.mk_surjective.forall.trans (forall_congr' fun b => ?_)
  rw [Quot.eq]
  simp only [forall_const, le_Prop_eq, Pi.top_apply, Prop.top_eq_true, true_implies]
Quotient is Subsingleton iff Relation Generates Trivial Equivalence
Informal description
For any binary relation $r$ on a type $\alpha$, the quotient $\alpha / r$ is a subsingleton (i.e., has at most one element) if and only if the equivalence closure of $r$ is the trivial equivalence relation where all elements are related (i.e., $\text{EqvGen}(r) = \top$).