doc-next-gen

Mathlib.GroupTheory.Congruence.Basic

Module docstring

{"# Congruence relations

This file proves basic properties of the quotient of a type by a congruence relation.

The second half of the file concerns congruence relations on monoids, in which case the quotient by the congruence relation is also a monoid. There are results about the universal property of quotients of monoids, and the isomorphism theorems for monoids.

Implementation notes

A congruence relation on a monoid M can be thought of as a submonoid of M × M for which membership is an equivalence relation, but whilst this fact is established in the file, it is not used, since this perspective adds more layers of definitional unfolding.

Tags

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

Con.prod definition
(c : Con M) (d : Con N) : Con (M × N)
Full source 
/-- Given types with multiplications `M, N`, the product of two congruence relations `c` on `M` and
    `d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁` is related to `y₁`
    by `c` and `x₂` is related to `y₂` by `d`. -/
@[to_additive prod "Given types with additions `M, N`, the product of two congruence relations
`c` on `M` and `d` on `N`: `(x₁, x₂), (y₁, y₂) ∈ M × N` are related by `c.prod d` iff `x₁`
is related to `y₁` by `c` and `x₂` is related to `y₂` by `d`."]
protected def prod (c : Con M) (d : Con N) : Con (M × N) :=
  { c.toSetoid.prod d.toSetoid with
    mul' := fun h1 h2 => ⟨c.mul h1.1 h2.1, d.mul h1.2 h2.2⟩ }
Product of congruence relations
Informal description
Given types $M$ and $N$ with multiplication operations, and congruence relations $c$ on $M$ and $d$ on $N$, the product congruence relation $c \times d$ on $M \times N$ 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$ by $c$ and $x_2$ is related to $y_2$ by $d$. This relation preserves multiplication component-wise.
Con.pi definition
{ι : Type*} {f : ι → Type*} [∀ i, Mul (f i)] (C : ∀ i, Con (f i)) : Con (∀ i, f i)
Full source 
/-- The product of an indexed collection of congruence relations. -/
@[to_additive "The product of an indexed collection of additive congruence relations."]
def pi {ι : Type*} {f : ι → Type*} [∀ i, Mul (f i)] (C : ∀ i, Con (f i)) : Con (∀ i, f i) :=
  { @piSetoid _ _ fun i => (C i).toSetoid with
    mul' := fun h1 h2 i => (C i).mul (h1 i) (h2 i) }
Product of indexed congruence relations
Informal description
Given an indexed family of types $\{f_i\}_{i \in \iota}$ each equipped with a multiplication operation, and a family of congruence relations $\{C_i\}_{i \in \iota}$ where each $C_i$ is a congruence relation on $f_i$, the product congruence relation $\prod_{i \in \iota} C_i$ on the product type $\prod_{i \in \iota} f_i$ is defined such that two functions $h_1, h_2 \in \prod_{i \in \iota} f_i$ are related if and only if $h_1(i)$ is related to $h_2(i)$ by $C_i$ for each $i \in \iota$. This relation preserves multiplication pointwise.
Con.congr definition
{c d : Con M} (h : c = d) : c.Quotient ≃* d.Quotient
Full source 
/-- Makes an isomorphism of quotients by two congruence relations, given that the relations are
    equal. -/
@[to_additive "Makes an additive isomorphism of quotients by two additive congruence relations,
given that the relations are equal."]
protected def congr {c d : Con M} (h : c = d) : c.Quotient ≃* d.Quotient :=
  { Quotient.congr (Equiv.refl M) <| by apply Con.ext_iff.mp h with
    map_mul' := fun x y => by rcases x with ⟨⟩; rcases y with ⟨⟩; rfl }
Isomorphism of quotients by equal congruence relations
Informal description
Given two congruence relations $c$ and $d$ on a multiplicative structure $M$ such that $c = d$, the function constructs a multiplicative isomorphism between the quotients $M/c$ and $M/d$. This isomorphism maps each equivalence class $[x]_c$ in $M/c$ to the corresponding equivalence class $[x]_d$ in $M/d$.
Con.congr_mk theorem
{c d : Con M} (h : c = d) (a : M) : Con.congr h (a : c.Quotient) = (a : d.Quotient)
Full source 
@[to_additive (attr := simp)]
theorem congr_mk {c d : Con M} (h : c = d) (a : M) :
    Con.congr h (a : c.Quotient) = (a : d.Quotient) := rfl
Equality of equivalence classes under congruence relation isomorphism
Informal description
For any two congruence relations $c$ and $d$ on a multiplicative structure $M$ such that $c = d$, and for any element $a \in M$, the equivalence class of $a$ in the quotient $M/c$ under the isomorphism $\text{Con.congr}\, h$ is equal to the equivalence class of $a$ in the quotient $M/d$.
Con.le_comap_conGen theorem
{M N : Type*} [Mul M] [Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) : conGen (fun x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel)
Full source 
@[to_additive]
theorem le_comap_conGen {M N : Type*} [Mul M] [Mul N] (f : M → N)
    (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
    conGen (fun x y ↦ rel (f x) (f y)) ≤ Con.comap f H (conGen rel) := by
  intro x y h
  simp only [Con.comap_rel]
  exact .rec (fun x y h ↦ .of (f x) (f y) h) (fun x ↦ .refl (f x))
    (fun _ h ↦ .symm h) (fun _ _ h1 h2 ↦ h1.trans h2) (fun {w x y z} _ _ h1 h2 ↦
    (congrArg (fun a ↦ conGen rel a (f (x * z))) (H w y)).mpr
    (((congrArg (fun a ↦ conGen rel (f w * f y) a) (H x z))).mpr
    (.mul h1 h2))) h
Inclusion of Generated Congruence Relations under Pullback
Informal description
Let $M$ and $N$ be types with multiplication operations, and let $f : M \to N$ be a multiplicative map (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$). For any binary relation $\text{rel}$ on $N$, the congruence relation generated by $\text{rel} \circ f$ (i.e., the relation $(x, y) \mapsto \text{rel}(f(x), f(y))$) is contained in the pullback along $f$ of the congruence relation generated by $\text{rel}$. In other words, $\text{conGen}(\text{rel} \circ f) \leq \text{Con.comap}\, f\, H\, (\text{conGen}\, \text{rel})$.
Con.comap_conGen_equiv theorem
{M N : Type*} [Mul M] [Mul N] (f : MulEquiv M N) (rel : N → N → Prop) : Con.comap f (map_mul f) (conGen rel) = conGen (fun x y ↦ rel (f x) (f y))
Full source 
@[to_additive]
theorem comap_conGen_equiv {M N : Type*} [Mul M] [Mul N] (f : MulEquiv M N) (rel : N → N → Prop) :
    Con.comap f (map_mul f) (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) := by
  apply le_antisymm _ (le_comap_conGen f (map_mul f) rel)
  intro a b h
  simp only [Con.comap_rel] at h
  have H : ∀ n1 n2, (conGen rel) n1 n2 → ∀ a b, f a = n1 → f b = n2 →
      (conGen fun x y ↦ rel (f x) (f y)) a b := by
    intro n1 n2 h
    induction h with
    | of x y h =>
      intro _ _ fa fb
      apply ConGen.Rel.of
      rwa [fa, fb]
    | refl x =>
      intro _ _ fc fd
      rw [f.injective (fc.trans fd.symm)]
      exact ConGen.Rel.refl _
    | symm _ h => exact fun a b fs fb ↦ ConGen.Rel.symm (h b a fb fs)
    | trans _ _ ih ih1 =>
      exact fun a b fa fb ↦ Exists.casesOn (f.surjective _) fun c' hc' ↦
      ConGen.Rel.trans (ih a c' fa hc') (ih1 c' b hc' fb)
    | mul _ _ ih ih1 =>
      rename_i w x y z _ _
      intro a b fa fb
      rw [← f.eq_symm_apply, map_mul] at fa fb
      rw [fa, fb]
      exact ConGen.Rel.mul (ih (f.symm w) (f.symm x) (by simp) (by simp))
        (ih1 (f.symm y) (f.symm z) (by simp) (by simp))
  exact H (f a) (f b) h a b (refl _) (refl _)
Equality of Pullback and Generated Congruence Relations under Multiplicative Equivalence
Informal description
Let $M$ and $N$ be types equipped with multiplication operations, and let $f : M \to N$ be a multiplicative equivalence (i.e., a bijective multiplicative map). For any binary relation $\text{rel}$ on $N$, the pullback along $f$ of the congruence relation generated by $\text{rel}$ is equal to the congruence relation generated by the relation $(x, y) \mapsto \text{rel}(f(x), f(y))$ on $M$. In other words, $\text{Con.comap}\, f\, (\text{map\_mul}\, f)\, (\text{conGen}\, \text{rel}) = \text{conGen}\, (\lambda x y, \text{rel}(f(x), f(y)))$.
Con.comap_conGen_of_bijective theorem
{M N : Type*} [Mul M] [Mul N] (f : M → N) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) : Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y))
Full source 
@[to_additive]
theorem comap_conGen_of_bijective {M N : Type*} [Mul M] [Mul N] (f : M → N)
    (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) :
    Con.comap f H (conGen rel) = conGen (fun x y ↦ rel (f x) (f y)) :=
  comap_conGen_equiv (MulEquiv.ofBijective (MulHom.mk f H) hf) rel
Equality of Pullback and Generated Congruence Relations under Bijective Multiplicative Maps
Informal description
Let $M$ and $N$ be types equipped with multiplication operations, and let $f : M \to N$ be a bijective multiplicative map (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$). For any binary relation $\text{rel}$ on $N$, the pullback along $f$ of the congruence relation generated by $\text{rel}$ is equal to the congruence relation generated by the relation $(x, y) \mapsto \text{rel}(f(x), f(y))$ on $M$. In other words, $\text{Con.comap}\, f\, H\, (\text{conGen}\, \text{rel}) = \text{conGen}\, (\lambda x y, \text{rel}(f(x), f(y)))$.
Con.submonoid definition
: Submonoid (M × M)
Full source 
/-- The submonoid of `M × M` defined by a congruence relation on a monoid `M`. -/
@[to_additive (attr := coe) "The `AddSubmonoid` of `M × M` defined by an additive congruence
relation on an `AddMonoid` `M`."]
protected def submonoid : Submonoid (M × M) where
  carrier := { x | c x.1 x.2 }
  one_mem' := c.iseqv.1 1
  mul_mem' := c.mul
Submonoid of pairs related by a congruence relation
Informal description
For a congruence relation $c$ on a monoid $M$, the submonoid of $M \times M$ consists of all pairs $(x, y)$ such that $x \sim y$ under $c$. This submonoid contains the pair $(1, 1)$ (since $1 \sim 1$ by reflexivity) and is closed under multiplication (since if $x_1 \sim y_1$ and $x_2 \sim y_2$, then $x_1x_2 \sim y_1y_2$ by the congruence property).
Con.ofSubmonoid definition
(N : Submonoid (M × M)) (H : Equivalence fun x y => (x, y) ∈ N) : Con M
Full source 
/-- The congruence relation on a monoid `M` from a submonoid of `M × M` for which membership
    is an equivalence relation. -/
@[to_additive "The additive congruence relation on an `AddMonoid` `M` from
an `AddSubmonoid` of `M × M` for which membership is an equivalence relation."]
def ofSubmonoid (N : Submonoid (M × M)) (H : Equivalence fun x y => (x, y)(x, y) ∈ N) : Con M where
  r x y := (x, y)(x, y) ∈ N
  iseqv := H
  mul' := N.mul_mem
Congruence relation from a submonoid of $M \times M$
Informal description
Given a submonoid $N$ of $M \times M$ such that the relation $\sim$ defined by $(x, y) \in N$ is an equivalence relation, the function `Con.ofSubmonoid` constructs a congruence relation on $M$ where $x \sim y$ if and only if $(x, y) \in N$. This congruence relation preserves the multiplication operation of $M$.
Con.toSubmonoid instance
: Coe (Con M) (Submonoid (M × M))
Full source 
/-- Coercion from a congruence relation `c` on a monoid `M` to the submonoid of `M × M` whose
    elements are `(x, y)` such that `x` is related to `y` by `c`. -/
@[to_additive "Coercion from a congruence relation `c` on an `AddMonoid` `M`
to the `AddSubmonoid` of `M × M` whose elements are `(x, y)` such that `x`
is related to `y` by `c`."]
instance toSubmonoid : Coe (Con M) (Submonoid (M × M)) :=
  ⟨fun c => c.submonoid⟩
Submonoid of Congruence-Related Pairs
Informal description
For any congruence relation $c$ on a monoid $M$, there is a canonical submonoid of $M \times M$ consisting of all pairs $(x, y)$ such that $x \sim y$ under $c$.
Con.mem_coe theorem
{c : Con M} {x y} : (x, y) ∈ (↑c : Submonoid (M × M)) ↔ (x, y) ∈ c
Full source 
@[to_additive]
theorem mem_coe {c : Con M} {x y} : (x, y)(x, y) ∈ (↑c : Submonoid (M × M))(x, y) ∈ (↑c : Submonoid (M × M)) ↔ (x, y) ∈ c :=
  Iff.rfl
Membership in Congruence Submonoid iff Congruent
Informal description
For a congruence relation $c$ on a monoid $M$ and elements $x, y \in M$, the pair $(x, y)$ belongs to the submonoid of $M \times M$ associated with $c$ if and only if $x$ is related to $y$ under the congruence relation $c$.
Con.to_submonoid_inj theorem
(c d : Con M) (H : (c : Submonoid (M × M)) = d) : c = d
Full source 
@[to_additive]
theorem to_submonoid_inj (c d : Con M) (H : (c : Submonoid (M × M)) = d) : c = d :=
  ext fun x y => show (x, y)(x, y) ∈ c.submonoid(x, y) ∈ c.submonoid ↔ (x, y) ∈ d from H ▸ Iff.rfl
Injectivity of Congruence Relation to Submonoid Map
Informal description
For any two congruence relations $c$ and $d$ on a monoid $M$, if the submonoids of $M \times M$ associated with $c$ and $d$ are equal, then $c = d$.
Con.le_iff theorem
{c d : Con M} : c ≤ d ↔ (c : Submonoid (M × M)) ≤ d
Full source 
@[to_additive]
theorem le_iff {c d : Con M} : c ≤ d ↔ (c : Submonoid (M × M)) ≤ d :=
  ⟨fun h _ H => h H, fun h x y hc => h <| show (x, y) ∈ c from hc⟩
Order Relation on Congruences via Submonoid Containment
Informal description
For any two congruence relations $c$ and $d$ on a monoid $M$, the relation $c \leq d$ holds if and only if the submonoid of $M \times M$ associated with $c$ is contained in the submonoid associated with $d$.
Con.mrange_mk' theorem
: MonoidHom.mrange c.mk' = ⊤
Full source 
@[to_additive (attr := simp)]
-- Porting note: removed dot notation
theorem mrange_mk' : MonoidHom.mrange c.mk' = ⊤ :=
  MonoidHom.mrange_eq_top.2 mk'_surjective
Surjectivity of the Canonical Quotient Map for Congruence Relations
Informal description
The range of the canonical monoid homomorphism from a monoid $M$ to its quotient $M/c$ by a congruence relation $c$ is the entire quotient monoid, i.e., $\text{range}([\, \cdot \,]) = M/c$.
Con.lift_range theorem
(H : c ≤ ker f) : MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f
Full source 
/-- Given a congruence relation `c` on a monoid and a homomorphism `f` constant on `c`'s
    equivalence classes, `f` has the same image as the homomorphism that `f` induces on the
    quotient. -/
@[to_additive "Given an additive congruence relation `c` on an `AddMonoid` and a homomorphism `f`
constant on `c`'s equivalence classes, `f` has the same image as the homomorphism that `f` induces
on the quotient."]
theorem lift_range (H : c ≤ ker f) : MonoidHom.mrange (c.lift f H) = MonoidHom.mrange f :=
  Submonoid.ext fun x => ⟨by rintro ⟨⟨y⟩, hy⟩; exact ⟨y, hy⟩, fun ⟨y, hy⟩ => ⟨↑y, hy⟩⟩
Image Equality for Induced Homomorphism on Quotient Monoid
Informal description
Let $M$ be a monoid with a congruence relation $c$, and let $f : M \to P$ be a monoid homomorphism that is constant on each equivalence class of $c$ (i.e., $c \leq \ker f$). Then the image of the induced homomorphism $\overline{f} : M/c \to P$ is equal to the image of $f$.
Con.kerLift_range_eq theorem
: MonoidHom.mrange (kerLift f) = MonoidHom.mrange f
Full source 
/-- Given a monoid homomorphism `f`, the induced homomorphism on the quotient by `f`'s kernel has
    the same image as `f`. -/
@[to_additive (attr := simp) "Given an `AddMonoid` homomorphism `f`, the induced homomorphism
on the quotient by `f`'s kernel has the same image as `f`."]
theorem kerLift_range_eq : MonoidHom.mrange (kerLift f) = MonoidHom.mrange f :=
  lift_range fun _ _ => id
Image Equality for Kernel Lift Homomorphism
Informal description
Let $f: M \to P$ be a monoid homomorphism. Then the image of the induced homomorphism $\overline{f}: M/\ker f \to P$ (where $\ker f$ is the kernel congruence relation of $f$) is equal to the image of $f$.
Con.quotientKerEquivRange definition
(f : M →* P) : (ker f).Quotient ≃* MonoidHom.mrange f
Full source 
/-- The **first isomorphism theorem for monoids**. -/
@[to_additive "The first isomorphism theorem for `AddMonoid`s."]
noncomputable def quotientKerEquivRange (f : M →* P) : (ker f).Quotient ≃* MonoidHom.mrange f :=
  { Equiv.ofBijective
        ((@MulEquiv.toMonoidHom (MonoidHom.mrange (kerLift f)) _ _ _ <|
              MulEquiv.submonoidCongr kerLift_range_eq).comp
          (kerLift f).mrangeRestrict) <|
      ((Equiv.bijective (@MulEquiv.toEquiv (MonoidHom.mrange (kerLift f)) _ _ _ <|
          MulEquiv.submonoidCongr kerLift_range_eq)).comp
        ⟨fun x y h =>
          kerLift_injective f <| by rcases x with ⟨⟩; rcases y with ⟨⟩; injections,
          fun ⟨w, z, hz⟩ => ⟨z, by rcases hz with ⟨⟩; rfl⟩⟩) with
    map_mul' := MonoidHom.map_mul _ }
First Isomorphism Theorem for Monoids (Image Version)
Informal description
Given a monoid homomorphism $f: M \to P$, the quotient monoid $M/\ker f$ is isomorphic to the image of $f$ in $P$ via the map $[x] \mapsto f(x)$, where $\ker f$ is the kernel congruence relation of $f$ and $[x]$ denotes the equivalence class of $x \in M$ under $\ker f$.
Con.quotientKerEquivOfRightInverse definition
(f : M →* P) (g : P → M) (hf : Function.RightInverse g f) : (ker f).Quotient ≃* P
Full source 
/-- The first isomorphism theorem for monoids in the case of a homomorphism with right inverse. -/
@[to_additive (attr := simps)
  "The first isomorphism theorem for `AddMonoid`s in the case of a homomorphism
  with right inverse."]
def quotientKerEquivOfRightInverse (f : M →* P) (g : P → M) (hf : Function.RightInverse g f) :
    (ker f).Quotient ≃* P :=
  { kerLift f with
    toFun := kerLift f
    invFun := (↑) ∘ g
    left_inv := fun x => kerLift_injective _ (by rw [Function.comp_apply, kerLift_mk, hf])
    right_inv := fun x => by (conv_rhs => rw [← hf x]); rfl }
First Isomorphism Theorem for Monoids with Right Inverse
Informal description
Given a monoid homomorphism $f: M \to P$ with a right inverse $g: P \to M$ (i.e., $f \circ g = \text{id}_P$), the quotient of $M$ by the kernel congruence relation of $f$ is isomorphic as a monoid to $P$ via the map $[x] \mapsto f(x)$.
Con.quotientKerEquivOfSurjective definition
(f : M →* P) (hf : Surjective f) : (ker f).Quotient ≃* P
Full source 
/-- The first isomorphism theorem for Monoids in the case of a surjective homomorphism.

For a `computable` version, see `Con.quotientKerEquivOfRightInverse`.
-/
@[to_additive "The first isomorphism theorem for `AddMonoid`s in the case of a surjective
homomorphism.

For a `computable` version, see `AddCon.quotientKerEquivOfRightInverse`.
"]
noncomputable def quotientKerEquivOfSurjective (f : M →* P) (hf : Surjective f) :
    (ker f).Quotient ≃* P :=
  quotientKerEquivOfRightInverse _ _ hf.hasRightInverse.choose_spec
First Isomorphism Theorem for Monoids (Surjective Case)
Informal description
Given a surjective monoid homomorphism $f: M \to P$, the quotient of $M$ by the kernel congruence relation of $f$ is isomorphic as a monoid to $P$ via the map $[x] \mapsto f(x)$.
Con.comapQuotientEquivOfSurj definition
(c : Con M) (f : N →* M) (hf : Function.Surjective f) : (Con.comap f f.map_mul c).Quotient ≃* c.Quotient
Full source 
/-- If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N -/
@[to_additive "If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c :
AddCon N"]
noncomputable def comapQuotientEquivOfSurj (c : Con M) (f : N →* M) (hf : Function.Surjective f) :
    (Con.comap f f.map_mul c).Quotient ≃* c.Quotient :=
  (Con.congr Con.comap_eq).trans <| Con.quotientKerEquivOfSurjective (c.mk'.comp f) <|
    Con.mk'_surjective.comp hf
Isomorphism between quotients by pullback congruence relations under a surjective homomorphism
Informal description
Given a congruence relation $c$ on a monoid $M$, a surjective monoid homomorphism $f : N \to M$, and the pullback congruence relation $\text{comap}\, f\, \text{map\_mul}\, c$ on $N$, there is a multiplicative isomorphism between the quotient monoid $N/(\text{comap}\, f\, \text{map\_mul}\, c)$ and the quotient monoid $M/c$. This isomorphism maps each equivalence class $[x]$ in $N/(\text{comap}\, f\, \text{map\_mul}\, c)$ to the equivalence class $[f(x)]$ in $M/c$.
Con.comapQuotientEquivOfSurj_mk theorem
(c : Con M) {f : N →* M} (hf : Function.Surjective f) (x : N) : comapQuotientEquivOfSurj c f hf x = f x
Full source 
@[to_additive (attr := simp)]
lemma comapQuotientEquivOfSurj_mk (c : Con M) {f : N →* M} (hf : Function.Surjective f) (x : N) :
    comapQuotientEquivOfSurj c f hf x = f x := rfl
Image of Equivalence Class under Quotient Isomorphism for Surjective Homomorphism
Informal description
Let $c$ be a congruence relation on a monoid $M$, and let $f : N \to M$ be a surjective monoid homomorphism. For any element $x \in N$, the image of the equivalence class $[x]$ under the isomorphism $\text{comapQuotientEquivOfSurj}\, c\, f\, hf$ from $N/(\text{comap}\, f\, \text{map\_mul}\, c)$ to $M/c$ is equal to the equivalence class $[f(x)]$ in $M/c$. In other words, the isomorphism maps $[x]$ to $[f(x)]$.
Con.comapQuotientEquivOfSurj_symm_mk theorem
(c : Con M) {f : N →* M} (hf) (x : N) : (comapQuotientEquivOfSurj c f hf).symm (f x) = x
Full source 
@[to_additive (attr := simp)]
lemma comapQuotientEquivOfSurj_symm_mk (c : Con M) {f : N →* M} (hf) (x : N) :
    (comapQuotientEquivOfSurj c f hf).symm (f x) = x :=
  (MulEquiv.symm_apply_eq (c.comapQuotientEquivOfSurj f hf)).mpr rfl
Inverse of Quotient Isomorphism Maps Equivalence Classes Back
Informal description
Let $c$ be a congruence relation on a monoid $M$, and let $f : N \to M$ be a surjective monoid homomorphism. For any element $x \in N$, the inverse of the isomorphism $\text{comapQuotientEquivOfSurj}\, c\, f\, hf$ maps the equivalence class $[f(x)]$ in $M/c$ back to the equivalence class $[x]$ in $N/(\text{comap}\, f\, \text{map\_mul}\, c)$.
Con.comapQuotientEquivOfSurj_symm_mk' theorem
(c : Con M) (f : N ≃* M) (x : N) : ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ _ _ (comapQuotientEquivOfSurj c (f : N →* M) f.surjective)) ⟦f x⟧) = ↑x
Full source 
/-- This version infers the surjectivity of the function from a MulEquiv function -/
@[to_additive (attr := simp) "This version infers the surjectivity of the function from a
MulEquiv function"]
lemma comapQuotientEquivOfSurj_symm_mk' (c : Con M) (f : N ≃* M) (x : N) :
    ((@MulEquiv.symm (Con.Quotient (comap ⇑f _ c)) _ _ _
      (comapQuotientEquivOfSurj c (f : N →* M) f.surjective)) ⟦f x⟧) = ↑x :=
  (MulEquiv.symm_apply_eq (@comapQuotientEquivOfSurj M N _ _ c f _)).mpr rfl
Inverse Isomorphism Property for Quotients by Pullback Congruence Relations
Informal description
Let $c$ be a congruence relation on a monoid $M$, and let $f : N \to M$ be a multiplicative equivalence (i.e., a bijective monoid homomorphism). For any $x \in N$, the inverse of the isomorphism $(N/\text{comap}\,f\,c) \cong M/c$ maps the equivalence class $[f(x)]$ in $M/c$ back to the equivalence class $[x]$ in $N/\text{comap}\,f\,c$.
Con.comapQuotientEquiv definition
(f : N →* M) : (comap f f.map_mul c).Quotient ≃* MonoidHom.mrange (c.mk'.comp f)
Full source 
/-- The **second isomorphism theorem for monoids**. -/
@[to_additive "The second isomorphism theorem for `AddMonoid`s."]
noncomputable def comapQuotientEquiv (f : N →* M) :
    (comap f f.map_mul c).Quotient ≃* MonoidHom.mrange (c.mk'.comp f) :=
  (Con.congr comap_eq).trans <| quotientKerEquivRange <| c.mk'.comp f
Second Isomorphism Theorem for Monoids (Pullback Version)
Informal description
Given a monoid homomorphism $f : N \to M$ and a congruence relation $c$ on $M$, there is a multiplicative isomorphism between: 1. The quotient monoid $N/\text{comap}\,f\,c$ (where $\text{comap}\,f\,c$ is the pullback congruence relation on $N$) 2. The image of the composition of $f$ with the natural projection $M \to M/c$ This isomorphism is given by mapping the equivalence class $[n]_{\text{comap}\,f\,c}$ to $[f(n)]_c$ in the image.
Con.quotientQuotientEquivQuotient definition
(c d : Con M) (h : c ≤ d) : (ker (c.map d h)).Quotient ≃* d.Quotient
Full source 
/-- The **third isomorphism theorem for monoids**. -/
@[to_additive "The third isomorphism theorem for `AddMonoid`s."]
def quotientQuotientEquivQuotient (c d : Con M) (h : c ≤ d) :
    (ker (c.map d h)).Quotient ≃* d.Quotient :=
  { Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h with
    map_mul' := fun x y =>
      Con.induction_on₂ x y fun w z =>
        Con.induction_on₂ w z fun a b =>
          show _ = d.mk' a * d.mk' b by rw [← d.mk'.map_mul]; rfl }
Third Isomorphism Theorem for Monoids
Informal description
Given two congruence relations $c$ and $d$ on a monoid $M$ with $c \leq d$, there is a monoid isomorphism between: 1. The quotient of $M/c$ by the kernel of the natural map $M/c \to M/d$ 2. The quotient monoid $M/d$ This isomorphism is given by the equivalence classes: $[[x]_c]_{\ker} \mapsto [x]_d$ for $x \in M$, where $[x]_c$ denotes the equivalence class of $x$ under $c$ and $[x]_d$ under $d$.
Con.smul theorem
{α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) {w x : M} (h : c w x) : c (a • w) (a • x)
Full source 
@[to_additive]
theorem smul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α)
    {w x : M} (h : c w x) : c (a • w) (a • x) := by
  simpa only [smul_one_mul] using c.mul (c.refl' (a • (1 : M) : M)) h
Scalar Multiplication Preserves Congruence Relations
Informal description
Let $M$ be a multiplicative monoid with a scalar multiplication operation by elements of type $\alpha$, such that $\alpha$ acts compatibly with the multiplication in $M$ (i.e., $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for all $a, b \in \alpha$ and $m \in M$). For any congruence relation $c$ on $M$, scalar $a \in \alpha$, and elements $w, x \in M$ such that $w \sim x$ under $c$, we have $a \cdot w \sim a \cdot x$ under $c$.
Con.instSMul instance
{α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) : SMul α c.Quotient
Full source 
@[to_additive]
instance instSMul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) :
    SMul α c.Quotient where
  smul a := (Quotient.map' (a • ·)) fun _ _ => c.smul a
Scalar Multiplication on Quotient Monoid by Congruence Relation
Informal description
For a multiplicative monoid $M$ with a scalar multiplication operation by elements of type $\alpha$ that is compatible with the multiplication in $M$ (i.e., $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for all $a, b \in \alpha$ and $m \in M$), and a congruence relation $c$ on $M$, the quotient monoid $M/c$ inherits a scalar multiplication operation from $M$.
Con.coe_smul theorem
{α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) (x : M) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient)
Full source 
@[to_additive]
theorem coe_smul {α M : Type*} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M)
    (a : α) (x : M) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient) :=
  rfl
Scalar Multiplication Commutes with Quotient Projection in Monoids
Informal description
Let $M$ be a multiplicative monoid with a scalar multiplication operation by elements of type $\alpha$ that is compatible with the multiplication in $M$ (i.e., $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for all $a, b \in \alpha$ and $m \in M$). For any congruence relation $c$ on $M$, scalar $a \in \alpha$, and element $x \in M$, the equivalence class of $a \cdot x$ in the quotient monoid $M/c$ is equal to the scalar multiplication of $a$ with the equivalence class of $x$ in $M/c$. In symbols: $$ [a \cdot x] = a \cdot [x] $$ where $[x]$ denotes the equivalence class of $x$ in $M/c$.
Con.instSMulCommClass instance
{α β M : Type*} [MulOneClass M] [SMul α M] [SMul β M] [IsScalarTower α M M] [IsScalarTower β M M] [SMulCommClass α β M] (c : Con M) : SMulCommClass α β c.Quotient
Full source 
instance instSMulCommClass {α β M : Type*} [MulOneClass M] [SMul α M] [SMul β M]
    [IsScalarTower α M M] [IsScalarTower β M M] [SMulCommClass α β M] (c : Con M) :
    SMulCommClass α β c.Quotient where
  smul_comm a b := Quotient.ind' fun m => congr_arg Quotient.mk'' <| smul_comm a b m
Commutativity of Scalar Multiplications on Quotient Monoid by Congruence Relation
Informal description
For a multiplicative monoid $M$ with scalar multiplication operations by elements of types $\alpha$ and $\beta$ that are compatible with the multiplication in $M$ (i.e., $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for all $a, b \in \alpha$ or $\beta$ and $m \in M$), and a congruence relation $c$ on $M$, if the scalar multiplications by $\alpha$ and $\beta$ commute on $M$, then they also commute on the quotient monoid $M/c$.
Con.instIsScalarTower instance
{α β M : Type*} [MulOneClass M] [SMul α β] [SMul α M] [SMul β M] [IsScalarTower α M M] [IsScalarTower β M M] [IsScalarTower α β M] (c : Con M) : IsScalarTower α β c.Quotient
Full source 
instance instIsScalarTower {α β M : Type*} [MulOneClass M] [SMul α β] [SMul α M] [SMul β M]
    [IsScalarTower α M M] [IsScalarTower β M M] [IsScalarTower α β M] (c : Con M) :
    IsScalarTower α β c.Quotient where
  smul_assoc a b := Quotient.ind' fun m => congr_arg Quotient.mk'' <| smul_assoc a b m
Scalar Tower Property on Quotient Monoid by Congruence Relation
Informal description
For a multiplicative monoid $M$ with scalar multiplication operations by elements of types $\alpha$ and $\beta$ that are compatible with the multiplication in $M$, and a congruence relation $c$ on $M$, the quotient monoid $M/c$ inherits the scalar tower property from $M$. This means that for any $a \in \alpha$, $b \in \beta$, and $m \in M$, the scalar multiplications satisfy $(a \cdot b) \cdot [m] = a \cdot (b \cdot [m])$ in the quotient $M/c$, where $[m]$ denotes the equivalence class of $m$ under $c$.
Con.instIsCentralScalar instance
{α M : Type*} [MulOneClass M] [SMul α M] [SMul αᵐᵒᵖ M] [IsScalarTower α M M] [IsScalarTower αᵐᵒᵖ M M] [IsCentralScalar α M] (c : Con M) : IsCentralScalar α c.Quotient
Full source 
instance instIsCentralScalar {α M : Type*} [MulOneClass M] [SMul α M] [SMul αᵐᵒᵖ M]
    [IsScalarTower α M M] [IsScalarTower αᵐᵒᵖ M M] [IsCentralScalar α M] (c : Con M) :
    IsCentralScalar α c.Quotient where
  op_smul_eq_smul a := Quotient.ind' fun m => congr_arg Quotient.mk'' <| op_smul_eq_smul a m
Central Scalar Multiplication on Quotient Monoid by Congruence Relation
Informal description
For a multiplicative monoid $M$ with scalar multiplication operations by elements of type $\alpha$ and its opposite $\alpha^\text{op}$, both compatible with the multiplication in $M$ (i.e., $a \cdot (b \cdot m) = (a \cdot b) \cdot m$ for all $a, b \in \alpha$ or $\alpha^\text{op}$ and $m \in M$), and a congruence relation $c$ on $M$, if the scalar multiplication by $\alpha$ is central (i.e., $a \cdot m = m \cdot a$ for all $a \in \alpha$ and $m \in M$), then the quotient monoid $M/c$ inherits the property that scalar multiplication by $\alpha$ is central.
Con.mulAction instance
{α M : Type*} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M] (c : Con M) : MulAction α c.Quotient
Full source 
@[to_additive]
instance mulAction {α M : Type*} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M]
    (c : Con M) : MulAction α c.Quotient where
  one_smul := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| one_smul _ _
  mul_smul _ _ := Quotient.ind' fun _ => congr_arg Quotient.mk'' <| mul_smul _ _ _
Multiplicative Action on Quotient Monoid by Congruence Relation
Informal description
For a monoid $\alpha$ and a multiplicative monoid $M$ with a multiplicative action by $\alpha$ that is compatible with the multiplication in $M$ (i.e., $a \cdot (m_1 \cdot m_2) = (a \cdot m_1) \cdot m_2$ for all $a \in \alpha$ and $m_1, m_2 \in M$), and a congruence relation $c$ on $M$, the quotient monoid $M/c$ inherits a multiplicative action by $\alpha$.
Con.mulDistribMulAction instance
{α M : Type*} [Monoid α] [Monoid M] [MulDistribMulAction α M] [IsScalarTower α M M] (c : Con M) : MulDistribMulAction α c.Quotient
Full source 
instance mulDistribMulAction {α M : Type*} [Monoid α] [Monoid M] [MulDistribMulAction α M]
    [IsScalarTower α M M] (c : Con M) : MulDistribMulAction α c.Quotient :=
  { smul_one := fun _ => congr_arg Quotient.mk'' <| smul_one _
    smul_mul := fun _ => Quotient.ind₂' fun _ _ => congr_arg Quotient.mk'' <| smul_mul' _ _ _ }
Multiplicative Distributive Action on Quotient Monoid by Congruence Relation
Informal description
For any monoid $\alpha$, monoid $M$ with a multiplicative distributive action by $\alpha$ that is compatible with the multiplication in $M$ (i.e., $a \cdot (m_1 \cdot m_2) = (a \cdot m_1) \cdot m_2$ for all $a \in \alpha$ and $m_1, m_2 \in M$), and a congruence relation $c$ on $M$, the quotient monoid $M/c$ inherits a multiplicative distributive action by $\alpha$.