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

def Con.mkMulHom {M : Type u_1} [Mul M] (c : Con M) : M →ₙ* c.Quotient

The natural homomorphism from a magma to its quotient by a congruence relation.

Equations

• c.mkMulHom = { toFun := Con.toQuotient, map_mul' := ⋯ }

def AddCon.mkAddHom {M : Type u_1} [Add M] (c : AddCon M) : M →ₙ+ c.Quotient

The natural homomorphism from an additive magma to its quotient by an additive congruence relation.

Equations

• c.mkAddHom = { toFun := AddCon.toQuotient, map_add' := ⋯ }

@[simp]

theorem Con.mkMulHom_apply {M : Type u_1} [Mul M] (c : Con M) (a✝ : M) : c.mkMulHom a✝ = ↑a✝

@[simp]

theorem AddCon.mkAddHom_apply {M : Type u_1} [Add M] (c : AddCon M) (a✝ : M) : c.mkAddHom a✝ = ↑a✝

def Con.ker {M : Type u_1} {N : Type u_2} {F : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) : Con M

The kernel of a multiplicative homomorphism as a congruence relation.

Equations

• Con.ker f = { toSetoid := Setoid.ker ⇑f, mul' := ⋯ }

def AddCon.ker {M : Type u_1} {N : Type u_2} {F : Type u_4} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) : AddCon M

The kernel of an additive homomorphism as an additive congruence relation.

Equations

• AddCon.ker f = { toSetoid := Setoid.ker ⇑f, add' := ⋯ }

theorem Con.ker_coeMulHom {M : Type u_1} {N : Type u_2} {F : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) : ker ↑f = ker f

theorem AddCon.ker_coeAddHom {M : Type u_1} {N : Type u_2} {F : Type u_4} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) : ker ↑f = ker f

@[simp]

theorem Con.ker_rel {M : Type u_1} {N : Type u_2} {F : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) {x y : M} : (ker f) x y ↔ f x = f y

The definition of the congruence relation defined by a monoid homomorphism's kernel.

@[simp]

theorem AddCon.ker_rel {M : Type u_1} {N : Type u_2} {F : Type u_4} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) {x y : M} : (ker f) x y ↔ f x = f y

The definition of the additive congruence relation defined by an AddMonoid homomorphism's kernel.

@[simp]

theorem Con.ker_mkMulHom_eq {M : Type u_1} [Mul M] (c : Con M) : ker c.mkMulHom = c

@[simp]

theorem AddCon.ker_mkAddHom_eq {M : Type u_1} [Add M] (c : AddCon M) : ker c.mkAddHom = c

The kernel of the quotient map induced by an additive congruence relation c equals c.

@[reducible, inline, deprecated Con.ker (since := "2025-03-23")]

abbrev Con.mulKer {M : Type u_1} {P : Type u_3} [Mul M] [Mul P] (f : M → P) (h : ∀ (x y : M), f (x * y) = f x * f y) : Con M

The kernel of a multiplication-preserving function as a congruence relation.

Equations

• Con.mulKer f h = Con.ker { toFun := f, map_mul' := h }

@[reducible, inline, deprecated AddCon.ker (since := "2025-03-23")]

abbrev AddCon.addKer {M : Type u_1} {P : Type u_3} [Add M] [Add P] (f : M → P) (h : ∀ (x y : M), f (x + y) = f x + f y) : AddCon M

The kernel of an addition-preserving function as an additive congruence relation.

Equations

• AddCon.addKer f h = AddCon.ker { toFun := f, map_add' := h }

@[simp, deprecated Con.ker_mkMulHom_eq (since := "2025-03-23")]

theorem Con.mul_ker_mk_eq {M : Type u_1} [Mul M] {c : Con M} : mulKer toQuotient ⋯ = c

The kernel of the quotient map induced by a congruence relation c equals c.

@[simp, deprecated AddCon.ker_mkAddHom_eq (since := "2025-03-23")]

theorem AddCon.add_ker_mk_eq {M : Type u_1} [Add M] {c : AddCon M} : addKer toQuotient ⋯ = c

The kernel of the quotient map induced by an additive congruence relation c equals c.

def Con.mapGen {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {c : Con M} (f : M → N) : Con N

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

Equations

• Con.mapGen f = conGen (Relation.Map (⇑c) f f)

def AddCon.mapGen {M : Type u_1} {N : Type u_2} [Add M] [Add N] {c : AddCon M} (f : M → N) : AddCon N

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

Equations

• AddCon.mapGen f = addConGen (Relation.Map (⇑c) f f)

def Con.mapOfSurjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {c : Con M} (f : F) (h : ker f ≤ c) (hf : Function.Surjective ⇑f) : Con N

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

Equations

• Con.mapOfSurjective f h hf = { toSetoid := c.mapOfSurjective (⇑f) h hf, mul' := ⋯ }

def AddCon.mapOfSurjective {M : Type u_1} {N : Type u_2} {F : Type u_4} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] {c : AddCon M} (f : F) (h : ker f ≤ c) (hf : Function.Surjective ⇑f) : AddCon N

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

Equations

• AddCon.mapOfSurjective f h hf = { toSetoid := c.mapOfSurjective (⇑f) h hf, add' := ⋯ }

theorem Con.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} {F : Type u_4} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {c : Con M} {f : F} (h : ker f ≤ c) (hf : Function.Surjective ⇑f) : mapGen ⇑f = mapOfSurjective f h hf

A specialization of 'the smallest congruence relation containing a congruence relation c equals c'.

theorem AddCon.mapOfSurjective_eq_mapGen {M : Type u_1} {N : Type u_2} {F : Type u_4} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] {c : AddCon M} {f : F} (h : ker f ≤ c) (hf : Function.Surjective ⇑f) : mapGen ⇑f = mapOfSurjective f h hf

A specialization of 'the smallest additive congruence relation containing an additive congruence relation c equals c'.

def Con.correspondence {M : Type u_1} [Mul M] {c : Con M} : { d : Con M // c ≤ d } ≃o Con c.Quotient

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.

Equations

• One or more equations did not get rendered due to their size.

def AddCon.correspondence {M : Type u_1} [Add M] {c : AddCon M} : { d : AddCon M // c ≤ d } ≃o AddCon c.Quotient

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.

Equations

• One or more equations did not get rendered due to their size.

def Con.mk' {M : Type u_1} [MulOneClass M] (c : Con M) : M →* c.Quotient

The natural homomorphism from a monoid to its quotient by a congruence relation.

Equations

• c.mk' = { toFun := c.mkMulHom.toFun, map_one' := ⋯, map_mul' := ⋯ }

def AddCon.mk' {M : Type u_1} [AddZeroClass M] (c : AddCon M) : M →+ c.Quotient

The natural homomorphism from an AddMonoid to its quotient by an additive congruence relation.

Equations

• c.mk' = { toFun := c.mkAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Con.mk'_ker {M : Type u_1} [MulOneClass M] (c : Con M) : ker c.mk' = c

The kernel of the natural homomorphism from a monoid to its quotient by a congruence relation c equals c.

@[simp]

theorem AddCon.mk'_ker {M : Type u_1} [AddZeroClass M] (c : AddCon M) : ker c.mk' = c

The kernel of the natural homomorphism from an AddMonoid to its quotient by an additive congruence relation c equals c.

theorem Con.mk'_surjective {M : Type u_1} [MulOneClass M] {c : Con M} : Function.Surjective ⇑c.mk'

The natural homomorphism from a monoid to its quotient by a congruence relation is surjective.

theorem AddCon.mk'_surjective {M : Type u_1} [AddZeroClass M] {c : AddCon M} : Function.Surjective ⇑c.mk'

The natural homomorphism from an AddMonoid to its quotient by a congruence relation is surjective.

@[simp]

theorem Con.coe_mk' {M : Type u_1} [MulOneClass M] {c : Con M} : ⇑c.mk' = toQuotient

@[simp]

theorem AddCon.coe_mk' {M : Type u_1} [AddZeroClass M] {c : AddCon M} : ⇑c.mk' = toQuotient

theorem Con.ker_apply {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} {x y : M} : (ker f) x y ↔ f x = f y

theorem AddCon.ker_apply {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} {x y : M} : (ker f) x y ↔ f x = f y

theorem Con.comap_eq {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {c : Con M} {f : N →* M} : comap ⇑f ⋯ c = ker (c.mk'.comp f)

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.

theorem AddCon.comap_eq {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {c : AddCon M} {f : N →+ M} : comap ⇑f ⋯ c = ker (c.mk'.comp f)

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.

def Con.lift {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (c : Con M) (f : M →* P) (H : c ≤ ker f) : c.Quotient →* P

The homomorphism on the quotient of a monoid by a congruence relation c induced by a homomorphism constant on c's equivalence classes.

Equations

• c.lift f H = { toFun := fun (x : c.Quotient) => Con.liftOn x ⇑f ⋯, map_one' := ⋯, map_mul' := ⋯ }

def AddCon.lift {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ ker f) : c.Quotient →+ P

The homomorphism on the quotient of an AddMonoid by an additive congruence relation c induced by a homomorphism constant on c's equivalence classes.

Equations

• c.lift f H = { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Con.lift_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ ker f) (x : M) : (c.lift f H) (c.mk' x) = f x

The diagram describing the universal property for quotients of monoids commutes.

theorem AddCon.lift_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ ker f) (x : M) : (c.lift f H) (c.mk' x) = f x

The diagram describing the universal property for quotients of AddMonoids commutes.

@[simp]

theorem Con.lift_coe {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ ker f) (x : M) : (c.lift f H) ↑x = f x

The diagram describing the universal property for quotients of monoids commutes.

@[simp]

theorem AddCon.lift_coe {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ ker f) (x : M) : (c.lift f H) ↑x = f x

The diagram describing the universal property for quotients of AddMonoids commutes.

@[simp]

theorem Con.lift_comp_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f

The diagram describing the universal property for quotients of monoids commutes.

@[simp]

theorem AddCon.lift_comp_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f

The diagram describing the universal property for quotients of AddMonoids commutes.

@[simp]

theorem Con.lift_apply_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} (f : c.Quotient →* P) : c.lift (f.comp c.mk') ⋯ = f

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.

@[simp]

theorem AddCon.lift_apply_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} (f : c.Quotient →+ P) : c.lift (f.comp c.mk') ⋯ = f

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 Con.lift_funext {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} (f g : c.Quotient →* P) (h : ∀ (a : M), f ↑a = g ↑a) : f = g

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.

theorem AddCon.lift_funext {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} (f g : c.Quotient →+ P) (h : ∀ (a : M), f ↑a = g ↑a) : f = g

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 Con.lift_unique {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ ker f) (g : c.Quotient →* P) (Hg : g.comp c.mk' = f) : g = c.lift f H

The uniqueness part of the universal property for quotients of monoids.

theorem AddCon.lift_unique {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ ker f) (g : c.Quotient →+ P) (Hg : g.comp c.mk' = f) : g = c.lift f H

The uniqueness part of the universal property for quotients of AddMonoids.

theorem Con.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (h : c ≤ ker f) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(c.lift f h)

Surjective monoid homomorphisms constant on a congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

theorem AddCon.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (h : c ≤ ker f) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(c.lift f h)

Surjective AddMonoid homomorphisms constant on an additive congruence relation c's equivalence classes induce a surjective homomorphism on c's quotient.

theorem Con.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (c : Con M) (f : M →* P) (H : c ≤ ker f) (h : Function.Injective ⇑(c.lift f H)) : ker f = c

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.

theorem AddCon.ker_eq_lift_of_injective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ ker f) (h : Function.Injective ⇑(c.lift f H)) : ker f = c

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.

def Con.kerLift {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) : (ker f).Quotient →* P

The homomorphism induced on the quotient of a monoid by the kernel of a monoid homomorphism.

Equations

• Con.kerLift f = (Con.ker f).lift f ⋯

def AddCon.kerLift {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) : (ker f).Quotient →+ P

The homomorphism induced on the quotient of an AddMonoid by the kernel of an AddMonoid homomorphism.

Equations

• AddCon.kerLift f = (AddCon.ker f).lift f ⋯

@[simp]

theorem Con.kerLift_mk {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {f : M →* P} (x : M) : (kerLift f) ↑x = f x

The diagram described by the universal property for quotients of monoids, when the congruence relation is the kernel of the homomorphism, commutes.

@[simp]

theorem AddCon.kerLift_mk {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {f : M →+ P} (x : M) : (kerLift f) ↑x = f x

The diagram described by the universal property for quotients of AddMonoids, when the additive congruence relation is the kernel of the homomorphism, commutes.

theorem Con.kerLift_injective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) : Function.Injective ⇑(kerLift f)

A monoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

theorem AddCon.kerLift_injective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) : Function.Injective ⇑(kerLift f)

An AddMonoid homomorphism f induces an injective homomorphism on the quotient by f's kernel.

def Con.map {M : Type u_1} [MulOneClass M] (c d : Con M) (h : c ≤ d) : c.Quotient →* d.Quotient

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.

Equations

• c.map d h = c.lift d.mk' ⋯

def AddCon.map {M : Type u_1} [AddZeroClass M] (c d : AddCon M) (h : c ≤ d) : c.Quotient →+ d.Quotient

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.

Equations

• c.map d h = c.lift d.mk' ⋯

theorem Con.map_apply {M : Type u_1} [MulOneClass M] {c d : Con M} (h : c ≤ d) (x : c.Quotient) : (c.map d h) x = (c.lift d.mk' ⋯) x

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.

theorem AddCon.map_apply {M : Type u_1} [AddZeroClass M] {c d : AddCon M} (h : c ≤ d) (x : c.Quotient) : (c.map d h) x = (c.lift d.mk' ⋯) x

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.