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 : Con M} {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

• Con.congr h = { toEquiv := Quotient.congr (Equiv.refl M) ⋯, map_mul' := ⋯ }

def AddCon.congr {M : Type u_1} [Add M] {c : AddCon M} {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

• AddCon.congr h = { toEquiv := Quotient.congr (Equiv.refl M) ⋯, map_add' := ⋯ }

@[simp]

theorem Con.congr_mk {M : Type u_1} [Mul M] {c : Con M} {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 : AddCon M} {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 : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (rel : N → N → Prop) : (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 : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop) : (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 : N → N → Prop) : 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 : N → N → Prop) : 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 : 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 : 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 : M → N) (hf : Function.Bijective f) (H : ∀ (x y : M), f (x + y) = f x + f y) (rel : N → N → Prop) : 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) : Submonoid (M × 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) : AddSubmonoid (M × 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

• Con.ofSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, mul' := ⋯ }

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

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

Equations

• AddCon.ofAddSubmonoid N H = { r := fun (x y : M) => (x, y) ∈ N, iseqv := H, add' := ⋯ }

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] : Coe (AddCon M) (AddSubmonoid (M × 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 : M} {y : M} : (x, y) ∈ ↑c ↔ (x, y) ∈ c

theorem AddCon.mem_coe {M : Type u_1} [AddZeroClass M] {c : AddCon M} {x : M} {y : M} : (x, y) ∈ ↑c ↔ (x, y) ∈ c

theorem Con.to_submonoid_inj {M : Type u_1} [MulOneClass M] (c : Con M) (d : Con M) (H : ↑c = ↑d) : c = d

theorem AddCon.to_addSubmonoid_inj {M : Type u_1} [AddZeroClass M] (c : AddCon M) (d : AddCon M) (H : ↑c = ↑d) : c = d

theorem Con.le_iff {M : Type u_1} [MulOneClass M] {c : Con M} {d : Con M} : c ≤ d ↔ ↑c ≤ ↑d

theorem AddCon.le_iff {M : Type u_1} [AddZeroClass M] {c : AddCon M} {d : AddCon M} : c ≤ d ↔ ↑c ≤ ↑d

@[simp]

theorem Con.mrange_mk' {M : Type u_1} [MulOneClass M] {c : Con M} : MonoidHom.mrange c.mk' = ⊤

@[simp]

theorem AddCon.mrange_mk' {M : Type u_1} [AddZeroClass M] {c : AddCon M} : AddMonoidHom.mrange c.mk' = ⊤

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) : MonoidHom.mrange (c.lift f H) = MonoidHom.mrange 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) : AddMonoidHom.mrange (c.lift f H) = AddMonoidHom.mrange 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]

theorem Con.kerLift_range_eq {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} : MonoidHom.mrange (Con.kerLift f) = MonoidHom.mrange f

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

@[simp]

theorem AddCon.kerLift_range_eq {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} : AddMonoidHom.mrange (AddCon.kerLift f) = AddMonoidHom.mrange f

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

• Con.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((MulEquiv.submonoidCongr ⋯).toMonoidHom.comp (Con.kerLift f).mrangeRestrict) ⋯, map_mul' := ⋯ }

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

• AddCon.quotientKerEquivRange f = { toEquiv := Equiv.ofBijective ⇑((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) ⋯, map_add' := ⋯ }

def Con.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (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

• Con.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(Con.kerLift f), invFun := Con.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

def AddCon.quotientKerEquivOfRightInverse {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (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

• AddCon.quotientKerEquivOfRightInverse f g hf = { toFun := ⇑(AddCon.kerLift f), invFun := AddCon.toQuotient ∘ g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

theorem Con.quotientKerEquivOfRightInverse_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (hf : Function.RightInverse g ⇑f) (a : (Con.ker f).Quotient) : (Con.quotientKerEquivOfRightInverse f g hf) a = (Con.kerLift f) a

@[simp]

theorem Con.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) (g : P → M) (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 : P → M) (hf : Function.RightInverse g ⇑f) (a : (AddCon.ker f).Quotient) : (AddCon.quotientKerEquivOfRightInverse f g hf) a = (AddCon.kerLift f) a

@[simp]

theorem AddCon.quotientKerEquivOfRightInverse_symm_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (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

• Con.quotientKerEquivOfSurjective f hf = Con.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯

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

• AddCon.quotientKerEquivOfSurjective f hf = AddCon.quotientKerEquivOfRightInverse f (Exists.choose ⋯) ⋯

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

• c.comapQuotientEquivOfSurj f hf = (Con.congr ⋯).trans (Con.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)

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

• c.comapQuotientEquivOfSurj f hf = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)

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

• c.comapQuotientEquiv f = (Con.congr ⋯).trans (Con.quotientKerEquivRange (c.mk'.comp f))

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

• c.comapQuotientEquiv f = (AddCon.congr ⋯).trans (AddCon.quotientKerEquivRange (c.mk'.comp f))

def Con.quotientQuotientEquivQuotient {M : Type u_1} [MulOneClass M] (c : Con M) (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 : AddCon M) (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 : M} {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 : M} {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

• c.instSMul = { smul := fun (a : α) => Quotient.map' (fun (x : M) => a • x) ⋯ }

instance AddCon.instVAdd {α : Type u_4} {M : Type u_5} [AddZeroClass M] [VAdd α M] [VAddAssocClass α M M] (c : AddCon M) : VAdd α c.Quotient

Equations

• c.instVAdd = { vadd := fun (a : α) => Quotient.map' (fun (x : M) => a +ᵥ x) ⋯ }

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

• c.mulAction = MulAction.mk ⋯ ⋯

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

• c.addAction = AddAction.mk ⋯ ⋯

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

• c.mulDistribMulAction = MulDistribMulAction.mk ⋯ ⋯