Documentation

Mathlib.GroupTheory.Congruence.Basic

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

def Con.prod {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (d : Con N) :
Con (M × N)

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.

Equations
  • c.prod d = { toSetoid := c.prod d.toSetoid, mul' := }
def AddCon.prod {M : Type u_1} {N : Type u_2} [Add M] [Add N] (c : AddCon M) (d : AddCon N) :
AddCon (M × N)

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.

Equations
  • c.prod d = { toSetoid := c.prod d.toSetoid, add' := }
def Con.pi {ι : Type u_4} {f : ιType u_5} [(i : ι) → Mul (f i)] (C : (i : ι) → Con (f i)) :
Con ((i : ι) → f i)

The product of an indexed collection of congruence relations.

Equations
  • Con.pi C = { toSetoid := piSetoid, mul' := }
def AddCon.pi {ι : Type u_4} {f : ιType u_5} [(i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) :
AddCon ((i : ι) → f i)

The product of an indexed collection of additive congruence relations.

Equations
  • AddCon.pi C = { toSetoid := piSetoid, add' := }
def Con.congr {M : Type u_1} [Mul M] {c d : Con M} (h : c = d) :
c.Quotient ≃* d.Quotient

Makes an isomorphism of quotients by two congruence relations, given that the relations are equal.

Equations
def AddCon.congr {M : Type u_1} [Add M] {c d : AddCon M} (h : c = d) :
c.Quotient ≃+ d.Quotient

Makes an additive isomorphism of quotients by two additive congruence relations, given that the relations are equal.

Equations
@[simp]
theorem Con.congr_mk {M : Type u_1} [Mul M] {c d : Con M} (h : c = d) (a : M) :
(Con.congr h) a = a
@[simp]
theorem AddCon.congr_mk {M : Type u_1} [Add M] {c d : AddCon M} (h : c = d) (a : M) :
(AddCon.congr h) a = a
theorem Con.le_comap_conGen {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : MN) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : NNProp) :
(conGen fun (x y : M) => rel (f x) (f y)) Con.comap f H (conGen rel)
theorem AddCon.le_comap_conGen {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : MN) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : NNProp) :
(addConGen fun (x y : M) => rel (f x) (f y)) AddCon.comap f H (addConGen rel)
theorem Con.comap_conGen_equiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) (rel : NNProp) :
Con.comap f (conGen rel) = conGen fun (x y : M) => rel (f x) (f y)
theorem AddCon.comap_conGen_equiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (rel : NNProp) :
AddCon.comap f (addConGen rel) = addConGen fun (x y : M) => rel (f x) (f y)
theorem Con.comap_conGen_of_bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : MN) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : NNProp) :
Con.comap f H (conGen rel) = conGen fun (x y : M) => rel (f x) (f y)
theorem AddCon.comap_conGen_of_bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : MN) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : NNProp) :
AddCon.comap f H (addConGen rel) = addConGen fun (x y : M) => rel (f x) (f y)
def Con.submonoid {M : Type u_1} [MulOneClass M] (c : Con M) :

The submonoid of M × M defined by a congruence relation on a monoid M.

Equations
  • c = { carrier := {x : M × M | c x.1 x.2}, mul_mem' := , one_mem' := }
def AddCon.addSubmonoid {M : Type u_1} [AddZeroClass M] (c : AddCon M) :

The AddSubmonoid of M × M defined by an additive congruence relation on an AddMonoid M.

Equations
  • c = { carrier := {x : M × M | c x.1 x.2}, add_mem' := , zero_mem' := }
def Con.ofSubmonoid {M : Type u_1} [MulOneClass M] (N : Submonoid (M × M)) (H : Equivalence fun (x y : M) => (x, y) N) :
Con M

The congruence relation on a monoid M from a submonoid of M × M for which membership is an equivalence relation.

Equations
def AddCon.ofAddSubmonoid {M : Type u_1} [AddZeroClass M] (N : AddSubmonoid (M × M)) (H : Equivalence fun (x y : M) => (x, y) N) :

The additive congruence relation on an AddMonoid M from an AddSubmonoid of M × M for which membership is an equivalence relation.

Equations
instance Con.toSubmonoid {M : Type u_1} [MulOneClass M] :
Coe (Con M) (Submonoid (M × M))

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.

Equations
  • Con.toSubmonoid = { coe := fun (c : Con M) => c }
instance AddCon.toAddSubmonoid {M : Type u_1} [AddZeroClass M] :

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.

Equations
  • AddCon.toAddSubmonoid = { coe := fun (c : AddCon M) => c }
theorem Con.mem_coe {M : Type u_1} [MulOneClass M] {c : Con M} {x y : M} :
(x, y) c (x, y) c
theorem AddCon.mem_coe {M : Type u_1} [AddZeroClass M] {c : AddCon M} {x y : M} :
(x, y) c (x, y) c
theorem Con.to_submonoid_inj {M : Type u_1} [MulOneClass M] (c d : Con M) (H : c = d) :
c = d
theorem AddCon.to_addSubmonoid_inj {M : Type u_1} [AddZeroClass M] (c d : AddCon M) (H : c = d) :
c = d
theorem Con.le_iff {M : Type u_1} [MulOneClass M] {c d : Con M} :
c d c d
theorem AddCon.le_iff {M : Type u_1} [AddZeroClass M] {c d : AddCon M} :
c d c d
@[simp]
theorem Con.mrange_mk' {M : Type u_1} [MulOneClass M] {c : Con M} :
@[simp]
theorem AddCon.mrange_mk' {M : Type u_1} [AddZeroClass M] {c : AddCon M} :
theorem Con.lift_range {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c Con.ker f) :

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.

theorem AddCon.lift_range {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c AddCon.ker f) :

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.

@[simp]

Given a monoid homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

@[simp]

Given an AddMonoid homomorphism f, the induced homomorphism on the quotient by f's kernel has the same image as f.

noncomputable def Con.quotientKerEquivRange {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) :
(Con.ker f).Quotient ≃* (MonoidHom.mrange f)

The first isomorphism theorem for monoids.

Equations
noncomputable def AddCon.quotientKerEquivRange {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) :
(AddCon.ker f).Quotient ≃+ (AddMonoidHom.mrange f)

The first isomorphism theorem for AddMonoids.

Equations
def Con.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : PM) (hf : Function.RightInverse g f) :
(Con.ker f).Quotient ≃* P

The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.

Equations
def AddCon.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : PM) (hf : Function.RightInverse g f) :
(AddCon.ker f).Quotient ≃+ P

The first isomorphism theorem for AddMonoids in the case of a homomorphism with right inverse.

Equations
@[simp]
theorem Con.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : PM) (hf : Function.RightInverse g f) (a : (Con.ker f).Quotient) :
@[simp]
theorem Con.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : PM) (hf : Function.RightInverse g f) (a✝ : P) :
(Con.quotientKerEquivOfRightInverse f g hf).symm a✝ = (Con.toQuotient g) a✝
@[simp]
theorem AddCon.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : PM) (hf : Function.RightInverse g f) (a : (AddCon.ker f).Quotient) :
@[simp]
theorem AddCon.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : PM) (hf : Function.RightInverse g f) (a✝ : P) :
(AddCon.quotientKerEquivOfRightInverse f g hf).symm a✝ = (AddCon.toQuotient g) a✝
noncomputable def Con.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (hf : Function.Surjective f) :
(Con.ker f).Quotient ≃* P

The first isomorphism theorem for Monoids in the case of a surjective homomorphism.

For a computable version, see Con.quotientKerEquivOfRightInverse.

Equations
noncomputable def AddCon.quotientKerEquivOfSurjective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (hf : Function.Surjective f) :
(AddCon.ker f).Quotient ≃+ P

The first isomorphism theorem for AddMonoids in the case of a surjective homomorphism.

For a computable version, see AddCon.quotientKerEquivOfRightInverse.

Equations
noncomputable def Con.comapQuotientEquivOfSurj {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) (hf : Function.Surjective f) :
(Con.comap f c).Quotient ≃* c.Quotient

If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N

Equations
noncomputable def AddCon.comapQuotientEquivOfSurj {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) (hf : Function.Surjective f) :
(AddCon.comap f c).Quotient ≃+ c.Quotient

If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : AddCon N

Equations
@[simp]
theorem Con.comapQuotientEquivOfSurj_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) {f : N →* M} (hf : Function.Surjective f) (x : N) :
(c.comapQuotientEquivOfSurj f hf) x = (f x)
@[simp]
theorem AddCon.comapQuotientEquivOfSurj_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) {f : N →+ M} (hf : Function.Surjective f) (x : N) :
(c.comapQuotientEquivOfSurj f hf) x = (f x)
@[simp]
theorem Con.comapQuotientEquivOfSurj_symm_mk {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) {f : N →* M} (hf : Function.Surjective f) (x : N) :
(c.comapQuotientEquivOfSurj f hf).symm (f x) = x
@[simp]
theorem AddCon.comapQuotientEquivOfSurj_symm_mk {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) {f : N →+ M} (hf : Function.Surjective f) (x : N) :
(c.comapQuotientEquivOfSurj f hf).symm (f x) = x
@[simp]
theorem Con.comapQuotientEquivOfSurj_symm_mk' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N ≃* M) (x : N) :
(c.comapQuotientEquivOfSurj f ).symm f x = x

This version infers the surjectivity of the function from a MulEquiv function

@[simp]
theorem AddCon.comapQuotientEquivOfSurj_symm_mk' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N ≃+ M) (x : N) :
(c.comapQuotientEquivOfSurj f ).symm f x = x

This version infers the surjectivity of the function from a MulEquiv function

noncomputable def Con.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) :
(Con.comap f c).Quotient ≃* (MonoidHom.mrange (c.mk'.comp f))

The second isomorphism theorem for monoids.

Equations
noncomputable def AddCon.comapQuotientEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) :
(AddCon.comap f c).Quotient ≃+ (AddMonoidHom.mrange (c.mk'.comp f))

The second isomorphism theorem for AddMonoids.

Equations
def Con.quotientQuotientEquivQuotient {M : Type u_1} [MulOneClass M] (c d : Con M) (h : c d) :
(Con.ker (c.map d h)).Quotient ≃* d.Quotient

The third isomorphism theorem for monoids.

Equations
  • c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_mul' := }
def AddCon.quotientQuotientEquivQuotient {M : Type u_1} [AddZeroClass M] (c d : AddCon M) (h : c d) :
(AddCon.ker (c.map d h)).Quotient ≃+ d.Quotient

The third isomorphism theorem for AddMonoids.

Equations
  • c.quotientQuotientEquivQuotient d h = { toEquiv := c.quotientQuotientEquivQuotient d.toSetoid h, map_add' := }
theorem Con.smul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) {w x : M} (h : c w x) :
c (a w) (a x)
theorem AddCon.vadd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) (a : α) {w x : M} (h : c w x) :
c (a +ᵥ w) (a +ᵥ x)
instance Con.instSMul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) :
SMul α c.Quotient
Equations
instance AddCon.instVAdd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) :
VAdd α c.Quotient
Equations
theorem Con.coe_smul {α : Type u_4} {M : Type u_5} [MulOneClass M] [SMul α M] [IsScalarTower α M M] (c : Con M) (a : α) (x : M) :
(a x) = a x
theorem AddCon.coe_vadd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) (a : α) (x : M) :
(a +ᵥ x) = a +ᵥ x
instance Con.mulAction {α : Type u_4} {M : Type u_5} [Monoid α] [MulOneClass M] [MulAction α M] [IsScalarTower α M M] (c : Con M) :
MulAction α c.Quotient
Equations
instance AddCon.addAction {α : Type u_4} {M : Type u_5} [AddMonoid α] [AddZeroClass M] [AddAction α M] [VAddAssocClass α M M] (c : AddCon M) :
AddAction α c.Quotient
Equations
instance Con.mulDistribMulAction {α : Type u_4} {M : Type u_5} [Monoid α] [Monoid M] [MulDistribMulAction α M] [IsScalarTower α M M] (c : Con M) :
MulDistribMulAction α c.Quotient
Equations