doc-next-gen

Mathlib.GroupTheory.Congruence.Hom

Module docstring

{"# Congruence relations and homomorphisms

This file contains elementary definitions involving congruence relations and morphisms.

Main definitions

  • Con.ker: the kernel of a monoid homomorphism as a congruence relation
  • Con.mk': the map from a monoid to its quotient by a congruence relation
  • Con.lift: the homomorphism on the quotient given that the congruence is in the kernel
  • Con.map: homomorphism from a smaller to a larger quotient

Tags

congruence, congruence relation, quotient, quotient by congruence relation, monoid, quotient monoid "}

Con.mkMulHom definition
(c : Con M) : MulHom M c.Quotient
Full source 
/-- The natural homomorphism from a magma to its quotient by a congruence relation. -/
@[to_additive (attr := simps)"The natural homomorphism from an additive magma to its quotient by an
additive congruence relation."]
def mkMulHom (c : Con M) : MulHom M c.Quotient where
  toFun := (↑)
  map_mul' _ _ := rfl
Canonical multiplicative homomorphism to the quotient by a congruence relation
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$, the function maps an element $x \in M$ to its equivalence class $[x] \in M/c$ and preserves multiplication, i.e., $[x \cdot y] = [x] \cdot [y]$ for all $x, y \in M$.
Con.ker definition
(f : F) : Con M
Full source 
/-- The kernel of a multiplicative homomorphism as a congruence relation. -/
@[to_additive "The kernel of an additive homomorphism as an additive congruence relation."]
def ker (f : F) : Con M where
  toSetoid := Setoid.ker f
  mul' h1 h2 := by
    dsimp [Setoid.ker, onFun] at *
    rw [map_mul, h1, h2, map_mul]
Kernel congruence relation of a multiplicative homomorphism
Informal description
The kernel of a multiplicative homomorphism $f : M \to N$ is the congruence relation on $M$ defined by $x \sim y$ if and only if $f(x) = f(y)$. This relation preserves multiplication, meaning that if $x_1 \sim y_1$ and $x_2 \sim y_2$, then $x_1 \cdot x_2 \sim y_1 \cdot y_2$.
Con.ker_coeMulHom theorem
(f : F) : ker (f : MulHom M N) = ker f
Full source 
@[to_additive (attr := norm_cast)]
theorem ker_coeMulHom (f : F) : ker (f : MulHom M N) = ker f := rfl
Equality of Kernel Congruence Relations for Multiplicative Homomorphism Representations
Informal description
For any multiplicative homomorphism $f \colon M \to N$, the kernel congruence relation of $f$ (viewed as a non-unital multiplicative homomorphism) is equal to the kernel congruence relation of $f$ (viewed as an element of the homomorphism class $F$).
Con.ker_rel theorem
(f : F) {x y} : ker f x y ↔ f x = f y
Full source 
/-- The definition of the congruence relation defined by a monoid homomorphism's kernel. -/
@[to_additive (attr := simp) "The definition of the additive congruence relation defined by an
`AddMonoid` homomorphism's kernel."]
theorem ker_rel (f : F) {x y} : kerker f x y ↔ f x = f y :=
  Iff.rfl
Characterization of Kernel Congruence Relation via Homomorphism Equality
Informal description
For any multiplicative homomorphism $f \colon M \to N$ and any elements $x, y \in M$, the kernel congruence relation $\ker f$ relates $x$ and $y$ if and only if $f(x) = f(y)$. In other words, $x \sim y$ under $\ker f$ if and only if $f$ maps $x$ and $y$ to the same element in $N$.
Con.ker_mkMulHom_eq theorem
(c : Con M) : ker (mkMulHom c) = c
Full source 
@[to_additive (attr := simp) "The kernel of the quotient map induced by an additive congruence
relation `c` equals `c`."]
theorem ker_mkMulHom_eq (c : Con M) : ker (mkMulHom c) = c :=
  ext fun _ _ => Quotient.eq''
Kernel of Canonical Quotient Homomorphism Equals Original Congruence Relation
Informal description
For any congruence relation $c$ on a multiplicative structure $M$, the kernel of the canonical multiplicative homomorphism from $M$ to its quotient $M/c$ is equal to $c$ itself. In other words, the congruence relation defined by $x \sim y$ if and only if $[x] = [y]$ in $M/c$ is exactly $c$.
Con.mulKer abbrev
(f : M → P) (h : ∀ x y, f (x * y) = f x * f y) : Con M
Full source 
/-- The kernel of a multiplication-preserving function as a congruence relation. -/
@[to_additive "The kernel of an addition-preserving function as an additive congruence relation."]
abbrev mulKer (f : M → P) (h : ∀ x y, f (x * y) = f x * f y) : Con M :=
  ker <| MulHom.mk f h
Kernel Congruence Relation of a Multiplicative Homomorphism
Informal description
Given a multiplicative structure $M$ and a function $f \colon M \to P$ that preserves multiplication (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the kernel congruence relation $\ker f$ is defined as the set of pairs $(x, y) \in M \times M$ such that $f(x) = f(y)$. This relation is a congruence, meaning it is an equivalence relation that respects the multiplication operation.
Con.mul_ker_mk_eq theorem
{c : Con M} : (mulKer ((↑) : M → c.Quotient) fun _ _ => rfl) = c
Full source 
/-- The kernel of the quotient map induced by a congruence relation `c` equals `c`. -/
@[to_additive (attr := simp) "The kernel of the quotient map induced by an additive congruence
relation `c` equals `c`."]
theorem mul_ker_mk_eq {c : Con M} :
    (mulKer ((↑) : M → c.Quotient) fun _ _ => rfl) = c :=
  ext fun _ _ => Quotient.eq''
Kernel of Quotient Projection Equals Original Congruence Relation
Informal description
For any congruence relation $c$ on a multiplicative structure $M$, the kernel congruence relation of the canonical projection $\pi \colon M \to M/c$ (where $\pi(x) = [x]$) is equal to $c$ itself. In other words, $\ker \pi = c$.
Con.mapGen definition
{c : Con M} (f : M → N) : Con N
Full source 
/-- Given a function `f`, the smallest congruence relation containing the binary relation on `f`'s
image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)`
by a congruence relation `c`.' -/
@[to_additive "Given a function `f`, the smallest additive congruence relation containing the
binary relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the
elements of `f⁻¹(y)` by an additive congruence relation `c`.'"]
def mapGen {c : Con M} (f : M → N) : Con N :=
  conGen <| Relation.Map c f f
Congruence relation generated by the image of a function
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$ and a function $f : M \to N$, the function `Con.mapGen f` constructs the smallest congruence relation on $N$ such that for any $x, y \in M$, if $x \sim y$ under $c$, then $f(x) \sim f(y)$ under the new congruence relation. More precisely, this congruence relation is generated by the image of $c$ under $f$, i.e., it is the smallest congruence relation containing all pairs $(f(x), f(y))$ where $x \sim y$ under $c$.
Con.mapOfSurjective definition
{c : Con M} (f : F) (h : ker f ≤ c) (hf : Surjective f) : Con N
Full source 
/-- Given a surjective multiplicative-preserving function `f` whose kernel is contained in a
congruence relation `c`, the congruence relation on `f`'s codomain defined by '`x ≈ y` iff the
elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` by `c`.' -/
@[to_additive "Given a surjective addition-preserving function `f` whose kernel is contained in
an additive congruence relation `c`, the additive congruence relation on `f`'s codomain defined
by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)` by `c`.'"]
def mapOfSurjective {c : Con M} (f : F) (h : ker f ≤ c) (hf : Surjective f) : Con N where
  __ := c.toSetoid.mapOfSurjective f h hf
  mul' h₁ h₂ := by
    rcases h₁ with ⟨a, b, h1, rfl, rfl⟩
    rcases h₂ with ⟨p, q, h2, rfl, rfl⟩
    exact ⟨a * p, b * q, c.mul h1 h2, map_mul f _ _, map_mul f _ _⟩
Congruence relation induced by a surjective multiplicative-preserving function with kernel condition
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$, a multiplicative-preserving function $f : M \to N$ whose kernel is contained in $c$, and a proof that $f$ is surjective, the congruence relation $\text{mapOfSurjective}\ f\ h\ hf$ on $N$ 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 $c$. This relation preserves multiplication, meaning that if $x_1 \approx y_1$ and $x_2 \approx y_2$, then $x_1 \cdot x_2 \approx y_1 \cdot y_2$.
Con.mapOfSurjective_eq_mapGen theorem
{c : Con M} {f : F} (h : ker f ≤ c) (hf : Surjective f) : c.mapGen f = c.mapOfSurjective f h hf
Full source 
/-- A specialization of 'the smallest congruence relation containing a congruence relation `c`
equals `c`'. -/
@[to_additive "A specialization of 'the smallest additive congruence relation containing
an additive congruence relation `c` equals `c`'."]
theorem mapOfSurjective_eq_mapGen {c : Con M} {f : F} (h : ker f ≤ c) (hf : Surjective f) :
    c.mapGen f = c.mapOfSurjective f h hf := by
  rw [← conGen_of_con (c.mapOfSurjective f h hf)]; rfl
Equality of Generated and Induced Congruence Relations for Surjective Homomorphisms
Informal description
Let $M$ and $N$ be multiplicative structures, $c$ a congruence relation on $M$, and $f : M \to N$ a surjective homomorphism whose kernel is contained in $c$. Then the congruence relation on $N$ generated by the image of $c$ under $f$ is equal to the congruence relation induced by $f$ with kernel condition $h$.
Con.correspondence definition
{c : Con M} : { d // c ≤ d } ≃o Con c.Quotient
Full source 
/-- Given a congruence relation `c` on a type `M` with a multiplication, the order-preserving
bijection between the set of congruence relations containing `c` and the congruence relations
on the quotient of `M` by `c`. -/
@[to_additive "Given an additive congruence relation `c` on a type `M` with an addition,
the order-preserving bijection between the set of additive congruence relations containing `c` and
the additive congruence relations on the quotient of `M` by `c`."]
def correspondence {c : Con M} : { d // c ≤ d }{ d // c ≤ d } ≃o Con c.Quotient where
  toFun d :=
    d.1.mapOfSurjective (mkMulHom c) (by rw [Con.ker_mkMulHom_eq]; exact d.2) <|
      Quotient.mk_surjective
  invFun d :=
    ⟨comap ((↑) : M → c.Quotient) (fun _ _ => rfl) d, fun x y h =>
      show d x y by rw [c.eq.2 h]; exact d.refl _⟩
  left_inv d :=
    Subtype.ext_iff_val.2 <|
      ext fun x y =>
        ⟨fun ⟨a, b, H, hx, hy⟩ =>
          d.1.trans (d.1.symm <| d.2 <| c.eq.1 hx) <| d.1.trans H <| d.2 <| c.eq.1 hy,
          fun h => ⟨_, _, h, rfl, rfl⟩⟩
  right_inv d :=
    ext fun x y =>
      ⟨fun ⟨_, _, H, hx, hy⟩ =>
        hx ▸ hy ▸ H,
        Con.induction_on₂ x y fun w z h => ⟨w, z, h, rfl, rfl⟩⟩
  map_rel_iff' {s t} := by
    constructor
    · intros h x y hs
      rcases h ⟨x, y, hs, rfl, rfl⟩ with ⟨a, b, ht, hx, hy⟩
      exact t.1.trans (t.1.symm <| t.2 <| c.eq.1 hx) (t.1.trans ht (t.2 <| c.eq.1 hy))
    · exact Relation.map_mono
Correspondence between congruence relations containing $c$ and congruence relations on $M/c$
Informal description
Given a congruence relation $c$ on a multiplicative structure $M$, there is an order-preserving bijection between the set of congruence relations on $M$ containing $c$ and the set of congruence relations on the quotient $M/c$. Specifically, the bijection maps a congruence relation $d$ (with $c \leq d$) to the congruence relation on $M/c$ induced by $d$ via the canonical projection $M \to M/c$, and its inverse maps a congruence relation on $M/c$ back to its preimage under this projection.
Con.mk' definition
: M →* c.Quotient
Full source 
/-- The natural homomorphism from a monoid to its quotient by a congruence relation. -/
@[to_additive "The natural homomorphism from an `AddMonoid` to its quotient by an additive
congruence relation."]
def mk' : M →* c.Quotient where
  __ := mkMulHom c
  map_one' := rfl
Canonical homomorphism to quotient monoid by congruence relation
Informal description
The natural homomorphism from a monoid $M$ to its quotient $M/c$ by a congruence relation $c$, mapping each element $x \in M$ to its equivalence class $[x] \in M/c$. This homomorphism preserves the multiplicative identity and the multiplication operation, i.e., $[1] = 1$ and $[x \cdot y] = [x] \cdot [y]$ for all $x, y \in M$.
Con.mk'_ker theorem
: ker c.mk' = c
Full source 
/-- The kernel of the natural homomorphism from a monoid to its quotient by a congruence
    relation `c` equals `c`. -/
@[to_additive (attr := simp) "The kernel of the natural homomorphism from an `AddMonoid` to its
quotient by an additive congruence relation `c` equals `c`."]
theorem mk'_ker : ker c.mk' = c :=
  ext fun _ _ => c.eq
Kernel of Quotient Homomorphism Equals Congruence Relation
Informal description
For any congruence relation $c$ on a monoid $M$, the kernel of the canonical homomorphism $\pi \colon M \to M/c$ (which sends each element to its equivalence class) is equal to $c$ itself. In other words, two elements $x, y \in M$ are congruent under $c$ if and only if they are mapped to the same equivalence class by $\pi$.
Con.mk'_surjective theorem
: Surjective c.mk'
Full source 
/-- The natural homomorphism from a monoid to its quotient by a congruence relation is
    surjective. -/
@[to_additive "The natural homomorphism from an `AddMonoid` to its quotient by a congruence
relation is surjective."]
theorem mk'_surjective : Surjective c.mk' :=
  Quotient.mk''_surjective
Surjectivity of the Quotient Homomorphism for Monoids
Informal description
The canonical homomorphism $c.\text{mk}' \colon M \to M/c$ from a monoid $M$ to its quotient by a congruence relation $c$ is surjective. That is, for every element $[x] \in M/c$, there exists an element $y \in M$ such that $c.\text{mk}'(y) = [x]$.
Con.coe_mk' theorem
: (c.mk' : M → c.Quotient) = ((↑) : M → c.Quotient)
Full source 
@[to_additive (attr := simp)]
theorem coe_mk' : (c.mk' : M → c.Quotient) = ((↑) : M → c.Quotient) :=
  rfl
Canonical Homomorphism to Quotient Equals Natural Projection
Informal description
The canonical homomorphism $c.\text{mk}'$ from a monoid $M$ to its quotient $M/c$ by a congruence relation $c$ coincides with the natural projection map $\uparrow \colon M \to M/c$, i.e., $c.\text{mk}' = \uparrow$.
Con.ker_apply theorem
{f : M →* P} {x y} : ker f x y ↔ f x = f y
Full source 
@[to_additive]
theorem ker_apply {f : M →* P} {x y} : kerker f x y ↔ f x = f y := Iff.rfl
Characterization of Kernel Congruence Relation via Homomorphism Equality
Informal description
For any monoid homomorphism $f \colon M \to P$ and elements $x, y \in M$, the kernel congruence relation $\ker f$ relates $x$ and $y$ if and only if $f(x) = f(y)$. In other words, $x \sim y$ under $\ker f$ if and only if $f$ maps $x$ and $y$ to the same element in $P$.
Con.comap_eq theorem
{f : N →* M} : comap f f.map_mul c = ker (c.mk'.comp f)
Full source 
/-- Given a monoid homomorphism `f : N → M` and a congruence relation `c` on `M`, the congruence
    relation induced on `N` by `f` equals the kernel of `c`'s quotient homomorphism composed with
    `f`. -/
@[to_additive "Given an `AddMonoid` homomorphism `f : N → M` and an additive congruence relation
`c` on `M`, the additive congruence relation induced on `N` by `f` equals the kernel of `c`'s
quotient homomorphism composed with `f`."]
theorem comap_eq {f : N →* M} : comap f f.map_mul c = ker (c.mk'.comp f) :=
  ext fun x y => show c _ _ ↔ c.mk' _ = c.mk' _ by rw [← c.eq]; rfl
Induced Congruence Relation Equals Kernel of Quotient Composition
Informal description
Given a monoid homomorphism $f \colon N \to M$ and a congruence relation $c$ on $M$, the congruence relation on $N$ induced by $f$ (i.e., $x \sim y$ if and only if $f(x) \sim f(y)$ under $c$) is equal to the kernel of the composition of $f$ with the canonical quotient homomorphism $M \to M/c$. In other words, for all $x, y \in N$, we have $f(x) \sim f(y)$ under $c$ if and only if $[f(x)] = [f(y)]$ in $M/c$, where $[ \cdot ]$ denotes the equivalence class under $c$.
Con.lift definition
(H : c ≤ ker f) : c.Quotient →* P
Full source 
/-- The homomorphism on the quotient of a monoid by a congruence relation `c` induced by a
    homomorphism constant on `c`'s equivalence classes. -/
@[to_additive "The homomorphism on the quotient of an `AddMonoid` by an additive congruence
relation `c` induced by a homomorphism constant on `c`'s equivalence classes."]
def lift (H : c ≤ ker f) : c.Quotient →* P where
  toFun x := (Con.liftOn x f) fun _ _ h => H h
  map_one' := by rw [← f.map_one]; rfl
  map_mul' x y := Con.induction_on₂ x y fun m n => by
    dsimp only [← coe_mul, Con.liftOn_coe]
    rw [map_mul]
Lifting a monoid homomorphism to the quotient by a congruence relation
Informal description
Given a monoid homomorphism \( f \colon M \to P \) and a congruence relation \( c \) on \( M \) such that \( c \) is contained in the kernel of \( f \) (i.e., \( c(x, y) \) implies \( f(x) = f(y) \) for all \( x, y \in M \)), the function `Con.lift f H` is the unique monoid homomorphism from the quotient monoid \( M/c \) to \( P \) that satisfies \( \text{Con.lift}\ f\ H\ ([x]) = f(x) \) for all \( x \in M \), where \( [x] \) denotes the equivalence class of \( x \) in \( M/c \).
Con.lift_mk' theorem
(H : c ≤ ker f) (x) : c.lift f H (c.mk' x) = f x
Full source 
/-- The diagram describing the universal property for quotients of monoids commutes. -/
@[to_additive "The diagram describing the universal property for quotients of `AddMonoid`s
commutes."]
theorem lift_mk' (H : c ≤ ker f) (x) : c.lift f H (c.mk' x) = f x :=
  rfl
Universal Property of Quotient Monoid: $\text{Con.lift}\ f\ H\ ([x]) = f(x)$
Informal description
Let $M$ and $P$ be monoids, $c$ a congruence relation on $M$, and $f \colon M \to P$ a monoid homomorphism such that $c$ is contained in the kernel of $f$ (i.e., $c(x,y)$ implies $f(x) = f(y)$ for all $x,y \in M$). Then for any $x \in M$, the lifted homomorphism $\text{Con.lift}\ f\ H$ evaluated at the equivalence class $[x] \in M/c$ equals $f(x)$, i.e., \[ \text{Con.lift}\ f\ H\ ([x]) = f(x). \]
Con.lift_coe theorem
(H : c ≤ ker f) (x : M) : c.lift f H x = f x
Full source 
/-- The diagram describing the universal property for quotients of monoids commutes. -/
@[to_additive (attr := simp) "The diagram describing the universal property for quotients of
`AddMonoid`s commutes."]
theorem lift_coe (H : c ≤ ker f) (x : M) : c.lift f H x = f x :=
  rfl
Lifted Homomorphism Evaluates as Original on Quotient Classes
Informal description
Given a monoid homomorphism $f \colon M \to P$ and a congruence relation $c$ on $M$ such that $c$ is contained in the kernel of $f$ (i.e., $c(x,y)$ implies $f(x) = f(y)$ for all $x,y \in M$), the lifted homomorphism $\text{Con.lift}\ f\ H$ satisfies $\text{Con.lift}\ f\ H\ ([x]) = f(x)$ for all $x \in M$, where $[x]$ denotes the equivalence class of $x$ in the quotient $M/c$.
Con.lift_comp_mk' theorem
(H : c ≤ ker f) : (c.lift f H).comp c.mk' = f
Full source 
/-- The diagram describing the universal property for quotients of monoids commutes. -/
@[to_additive (attr := simp) "The diagram describing the universal property for quotients of
`AddMonoid`s commutes."]
theorem lift_comp_mk' (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f := by ext; rfl
Commutativity of Quotient Monoid Diagram: $(\text{lift}\ f\ H) \circ \text{mk'} = f$
Informal description
Let $M$ and $P$ be monoids, $c$ a congruence relation on $M$, and $f \colon M \to P$ a monoid homomorphism such that $c$ is contained in the kernel of $f$. Then the composition of the lifted homomorphism $\text{Con.lift}\ f\ H \colon M/c \to P$ with the canonical projection $\text{Con.mk'} \colon M \to M/c$ equals $f$, i.e., \[ (\text{Con.lift}\ f\ H) \circ \text{Con.mk'} = f. \]
Con.lift_apply_mk' theorem
(f : c.Quotient →* P) : (c.lift (f.comp c.mk') fun x y h => show f ↑x = f ↑y by rw [c.eq.2 h]) = f
Full source 
/-- Given a homomorphism `f` from the quotient of a monoid by a congruence relation, `f` equals the
    homomorphism on the quotient induced by `f` composed with the natural map from the monoid to
    the quotient. -/
@[to_additive (attr := simp) "Given a homomorphism `f` from the quotient of an `AddMonoid` by an
additive congruence relation, `f` equals the homomorphism on the quotient induced by `f` composed
with the natural map from the `AddMonoid` to the quotient."]
theorem lift_apply_mk' (f : c.Quotient →* P) :
    (c.lift (f.comp c.mk') fun x y h => show f ↑x = f ↑y by rw [c.eq.2 h]) = f := by
  ext x; rcases x with ⟨⟩; rfl
Lifting a Homomorphism from the Quotient Monoid Preserves the Original Homomorphism
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $P$ be another monoid. For any monoid homomorphism $f \colon M/c \to P$, the homomorphism obtained by lifting the composition $f \circ \pi$ (where $\pi \colon M \to M/c$ is the canonical projection) through the congruence relation $c$ is equal to $f$ itself. That is, $\text{Con.lift}(f \circ \pi, H) = f$, where $H$ is the proof that $c$ is contained in the kernel of $f \circ \pi$.
Con.lift_funext theorem
(f g : c.Quotient →* P) (h : ∀ a : M, f a = g a) : f = g
Full source 
/-- Homomorphisms on the quotient of a monoid by a congruence relation are equal if they
    are equal on elements that are coercions from the monoid. -/
@[to_additive "Homomorphisms on the quotient of an `AddMonoid` by an additive congruence relation
are equal if they are equal on elements that are coercions from the `AddMonoid`."]
theorem lift_funext (f g : c.Quotient →* P) (h : ∀ a : M, f a = g a) : f = g := by
  rw [← lift_apply_mk' f, ← lift_apply_mk' g]
  congr 1
  exact DFunLike.ext_iff.2 h
Uniqueness of Homomorphisms on Quotient Monoid via Equality on Representatives
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $P$ be another monoid. For any two monoid homomorphisms $f, g \colon M/c \to P$, if $f([a]) = g([a])$ for all $a \in M$, then $f = g$.
Con.lift_unique theorem
(H : c ≤ ker f) (g : c.Quotient →* P) (Hg : g.comp c.mk' = f) : g = c.lift f H
Full source 
/-- The uniqueness part of the universal property for quotients of monoids. -/
@[to_additive "The uniqueness part of the universal property for quotients of `AddMonoid`s."]
theorem lift_unique (H : c ≤ ker f) (g : c.Quotient →* P) (Hg : g.comp c.mk' = f) :
    g = c.lift f H :=
  (lift_funext g (c.lift f H)) fun x => by
    subst f
    rfl
Uniqueness of the Lift in the Universal Property of Quotient Monoids
Informal description
Let $M$ and $P$ be monoids, $c$ a congruence relation on $M$, and $f \colon M \to P$ a monoid homomorphism such that $c$ is contained in the kernel of $f$ (i.e., $x \sim y$ under $c$ implies $f(x) = f(y)$). For any monoid homomorphism $g \colon M/c \to P$ satisfying $g \circ \pi = f$, where $\pi \colon M \to M/c$ is the canonical projection, we have $g = \text{Con.lift}\ f\ H$.
Con.lift_surjective_of_surjective theorem
(h : c ≤ ker f) (hf : Surjective f) : Surjective (c.lift f h)
Full source 
/-- Surjective monoid homomorphisms constant on a congruence relation `c`'s equivalence classes
    induce a surjective homomorphism on `c`'s quotient. -/
@[to_additive "Surjective `AddMonoid` homomorphisms constant on an additive congruence
relation `c`'s equivalence classes induce a surjective homomorphism on `c`'s quotient."]
theorem lift_surjective_of_surjective (h : c ≤ ker f) (hf : Surjective f) :
    Surjective (c.lift f h) := fun y =>
  (Exists.elim (hf y)) fun w hw => ⟨w, (lift_mk' h w).symm ▸ hw⟩
Surjectivity of Quotient Lift for Surjective Homomorphisms
Informal description
Let $M$ and $P$ be monoids, $c$ a congruence relation on $M$, and $f \colon M \to P$ a surjective monoid homomorphism such that $c$ is contained in the kernel of $f$ (i.e., $x \sim y$ under $c$ implies $f(x) = f(y)$). Then the induced homomorphism $\overline{f} \colon M/c \to P$ defined by $\overline{f}([x]) = f(x)$ is also surjective.
Con.ker_eq_lift_of_injective theorem
(H : c ≤ ker f) (h : Injective (c.lift f H)) : ker f = c
Full source 
/-- Given a monoid homomorphism `f` from `M` to `P`, the kernel of `f` is the unique congruence
    relation on `M` whose induced map from the quotient of `M` to `P` is injective. -/
@[to_additive "Given an `AddMonoid` homomorphism `f` from `M` to `P`, the kernel of `f`
is the unique additive congruence relation on `M` whose induced map from the quotient of `M`
to `P` is injective."]
theorem ker_eq_lift_of_injective (H : c ≤ ker f) (h : Injective (c.lift f H)) : ker f = c :=
  toSetoid_inj <| Setoid.ker_eq_lift_of_injective f H h
Kernel Congruence Characterization via Injectivity of Quotient Lift
Informal description
Let $M$ and $P$ be monoids, $f \colon M \to P$ a monoid homomorphism, and $c$ a congruence relation on $M$ such that $c$ is contained in the kernel of $f$ (i.e., $x \sim y$ under $c$ implies $f(x) = f(y)$). If the induced homomorphism $\overline{f} \colon M/c \to P$ is injective, then the kernel congruence relation of $f$ equals $c$.
Con.kerLift definition
: (ker f).Quotient →* P
Full source 
/-- The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism. -/
@[to_additive "The homomorphism induced on the quotient of an `AddMonoid` by the kernel
of an `AddMonoid` homomorphism."]
def kerLift : (ker f).Quotient →* P :=
  ((ker f).lift f) fun _ _ => id
Kernel lift homomorphism
Informal description
The homomorphism induced on the quotient of a monoid \( M \) by the kernel congruence relation of a monoid homomorphism \( f \colon M \to P \). Specifically, it is the unique monoid homomorphism from \( M/\ker f \) to \( P \) that satisfies \( \text{Con.kerLift}\ f\ ([x]) = f(x) \) for all \( x \in M \), where \( [x] \) denotes the equivalence class of \( x \) in \( M/\ker f \).
Con.kerLift_mk theorem
(x : M) : kerLift f x = f x
Full source 
/-- The diagram described by the universal property for quotients of monoids, when the congruence
    relation is the kernel of the homomorphism, commutes. -/
@[to_additive (attr := simp) "The diagram described by the universal property for quotients
of `AddMonoid`s, when the additive congruence relation is the kernel of the homomorphism,
commutes."]
theorem kerLift_mk (x : M) : kerLift f x = f x :=
  rfl
Kernel Lift Homomorphism Evaluates to Original Function on Representatives
Informal description
For any monoid homomorphism $f \colon M \to P$ and any element $x \in M$, the kernel lift homomorphism $\text{kerLift}\, f$ evaluated at the equivalence class $[x]$ in the quotient $M/\ker f$ equals $f(x)$.
Con.kerLift_injective theorem
(f : M →* P) : Injective (kerLift f)
Full source 
/-- A monoid homomorphism `f` induces an injective homomorphism on the quotient by `f`'s kernel. -/
@[to_additive "An `AddMonoid` homomorphism `f` induces an injective homomorphism on the quotient
by `f`'s kernel."]
theorem kerLift_injective (f : M →* P) : Injective (kerLift f) := fun x y =>
  Quotient.inductionOn₂' x y fun _ _ => (ker f).eq.2
Injectivity of the Kernel Lift Homomorphism
Informal description
For any monoid homomorphism $f \colon M \to P$, the induced homomorphism $\text{kerLift}\, f \colon M/\ker f \to P$ is injective, where $\ker f$ is the kernel congruence relation of $f$ and $M/\ker f$ is the quotient monoid.
Con.map definition
(c d : Con M) (h : c ≤ d) : c.Quotient →* d.Quotient
Full source 
/-- Given congruence relations `c, d` on a monoid such that `d` contains `c`, `d`'s quotient
    map induces a homomorphism from the quotient by `c` to the quotient by `d`. -/
@[to_additive "Given additive congruence relations `c, d` on an `AddMonoid` such that `d`
contains `c`, `d`'s quotient map induces a homomorphism from the quotient by `c` to the quotient
by `d`."]
def map (c d : Con M) (h : c ≤ d) : c.Quotient →* d.Quotient :=
  (c.lift d.mk') fun x y hc => show (ker d.mk') x y from (mk'_ker d).symm ▸ h hc
Induced homomorphism between quotient monoids by finer congruence relation
Informal description
Given two congruence relations \( c \) and \( d \) on a monoid \( M \) such that \( c \leq d \) (i.e., \( c \) is finer than \( d \)), the function `Con.map c d h` is the induced monoid homomorphism from the quotient monoid \( M/c \) to the quotient monoid \( M/d \). This homomorphism sends each equivalence class \([x]_c\) to the equivalence class \([x]_d\).
Con.map_apply theorem
{c d : Con M} (h : c ≤ d) (x) : c.map d h x = c.lift d.mk' (fun _ _ hc => d.eq.2 <| h hc) x
Full source 
/-- Given congruence relations `c, d` on a monoid such that `d` contains `c`, the definition of
    the homomorphism from the quotient by `c` to the quotient by `d` induced by `d`'s quotient
    map. -/
@[to_additive "Given additive congruence relations `c, d` on an `AddMonoid` such that `d`
contains `c`, the definition of the homomorphism from the quotient by `c` to the quotient by `d`
induced by `d`'s quotient map."]
theorem map_apply {c d : Con M} (h : c ≤ d) (x) :
    c.map d h x = c.lift d.mk' (fun _ _ hc => d.eq.2 <| h hc) x :=
  rfl
Commutativity of Induced Homomorphism Between Quotient Monoids
Informal description
Let $M$ be a monoid with two congruence relations $c$ and $d$ such that $c \leq d$ (i.e., $c$ is finer than $d$). For any element $x \in M$, the image of the equivalence class $[x]_c$ under the induced homomorphism $\text{Con.map}\ c\ d\ h$ from $M/c$ to $M/d$ is equal to the equivalence class $[x]_d$ obtained by lifting the canonical projection $d.\text{mk'}$ through $c$. In other words, the following diagram commutes: $$\text{Con.map}\ c\ d\ h ([x]_c) = [x]_d$$ where $[x]_c$ denotes the equivalence class of $x$ in $M/c$ and $[x]_d$ denotes the equivalence class of $x$ in $M/d$.