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 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' := ⋯ }

theorem AddCon.prod.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (c : AddCon M) (d : AddCon N) : ∀ {w x y z : M × N}, (c.prod d.toSetoid) w x → (c.prod d.toSetoid) y z → c.Rel (w + y).1 (x + z).1 ∧ d.Rel (w + y).2 (x + z).2

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.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' := ⋯ }

theorem AddCon.pi.proof_1 {ι : Type u_1} {f : ι → Type u_2} [(i : ι) → Add (f i)] (C : (i : ι) → AddCon (f i)) : ∀ {w x y z : (i : ι) → f i}, piSetoid w x → piSetoid y z → ∀ (i : ι), (C i) (w i + y i) (x i + z i)

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.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' := ⋯ }

theorem AddCon.congr.proof_2 {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} (h : c = d) (x : c.Quotient) (y : c.Quotient) : (Quotient.congr (Equiv.refl M) ⋯).toFun (x + y) = (Quotient.congr (Equiv.refl M) ⋯).toFun x + (Quotient.congr (Equiv.refl M) ⋯).toFun y

theorem AddCon.congr.proof_1 {M : Type u_1} [Add M] {c : AddCon M} {d : AddCon M} (h : c = d) (x : M) (y : M) : c x y ↔ d x y

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' := ⋯ }

theorem AddCon.addSubmonoid.proof_1 {M : Type u_1} [AddZeroClass M] (c : AddCon M) : ∀ {a b : M × M}, c a.1 a.2 → c b.1 b.2 → c (a.1 + b.1) (a.2 + b.2)

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' := ⋯ }

theorem AddCon.addSubmonoid.proof_2 {M : Type u_1} [AddZeroClass M] (c : AddCon M) : c.toSetoid 0 0

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.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' := ⋯ }

theorem AddCon.ofAddSubmonoid.proof_1 {M : Type u_1} [AddZeroClass M] (N : AddSubmonoid (M × M)) : ∀ {w x y z : M}, (w, x) ∈ N → (y, z) ∈ N → (w, x) + (y, z) ∈ N

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' := ⋯ }

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 }

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 }

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.mem_coe {M : Type u_1} [MulOneClass M] {c : Con M} {x : M} {y : M} : (x, y) ∈ ↑c ↔ (x, y) ∈ c

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

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

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

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

@[simp]

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

@[simp]

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

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.

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.

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

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

theorem AddCon.quotientKerEquivRange.proof_2 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) : Function.Bijective (⇑(AddEquiv.addSubmonoidCongr ⋯).toEquiv ∘ ⇑(AddCon.kerLift f).mrangeRestrict)

theorem AddCon.quotientKerEquivRange.proof_3 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (a : (AddCon.ker f).Quotient) (b : (AddCon.ker f).Quotient) : ((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) (a + b) = ((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) a + ((AddEquiv.addSubmonoidCongr ⋯).toAddMonoidHom.comp (AddCon.kerLift f).mrangeRestrict) b

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' := ⋯ }

theorem AddCon.quotientKerEquivRange.proof_1 {M : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) : AddMonoidHomClass ((AddCon.ker f).Quotient →+ P) (AddCon.ker f).Quotient P

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' := ⋯ }

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' := ⋯ }

theorem AddCon.quotientKerEquivOfRightInverse.proof_1 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ⇑f) (x : (AddCon.ker f).Quotient) : (AddCon.toQuotient ∘ g) ((AddCon.kerLift f) x) = x

theorem AddCon.quotientKerEquivOfRightInverse.proof_2 {M : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (g : P → M) (hf : Function.RightInverse g ⇑f) (x : P) : (AddCon.kerLift f) ((AddCon.toQuotient ∘ g) x) = x

theorem AddCon.quotientKerEquivOfRightInverse.proof_3 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (x : (AddCon.ker f).Quotient) (y : (AddCon.ker f).Quotient) : (↑(AddCon.kerLift f)).toFun (x + y) = (↑(AddCon.kerLift f)).toFun x + (↑(AddCon.kerLift f)).toFun y

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

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

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' := ⋯ }

theorem AddCon.quotientKerEquivOfSurjective.proof_1 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ⇑f) : Function.HasRightInverse ⇑f

theorem AddCon.quotientKerEquivOfSurjective.proof_2 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) (hf : Function.Surjective ⇑f) : Function.RightInverse (Exists.choose ⋯) ⇑f

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.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 ⋯) ⋯

theorem AddCon.comapQuotientEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) : AddMonoidHomClass (N →+ c.Quotient) N c.Quotient

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))

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))

theorem AddCon.quotientQuotientEquivQuotient.proof_1 {M : Type u_1} [AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) (x : (AddCon.ker (c.map d h)).Quotient) (y : (AddCon.ker (c.map d h)).Quotient) : (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (x + y) = (c.quotientQuotientEquivQuotient d.toSetoid h).toFun x + (c.quotientQuotientEquivQuotient d.toSetoid h).toFun y

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' := ⋯ }

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' := ⋯ }

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)

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)

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) ⋯ }

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) ⋯ }

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

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.addAction.proof_1 {α : Type u_2} {M : Type u_1} [AddMonoid α] [AddZeroClass M] [AddAction α M] [VAddAssocClass α M M] (c : AddCon M) (q : Quotient c.toSetoid) : 0 +ᵥ q = q

theorem AddCon.addAction.proof_2 {α : Type u_2} {M : Type u_1} [AddMonoid α] [AddZeroClass M] [AddAction α M] [VAddAssocClass α M M] (c : AddCon M) : ∀ (x x_1 : α) (q : Quotient c.toSetoid), x + x_1 +ᵥ q = x +ᵥ (x_1 +ᵥ q)

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.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 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 ⋯ ⋯