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

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

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

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

Equations

• AddCon.ker f = AddCon.addKer ⇑f ⋯

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

The kernel of a monoid homomorphism as a congruence relation.

Equations

• Con.ker f = Con.mulKer ⇑f ⋯

@[simp]

theorem AddCon.ker_rel {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) {x : M} {y : M} : (AddCon.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_rel {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (f : M →* P) {x : M} {y : M} : (Con.ker f) x y ↔ f x = f y

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

theorem AddCon.mk'.proof_1 {M : Type u_1} [AddZeroClass M] (c : AddCon M) : ↑0 = ↑0

theorem AddCon.mk'.proof_2 {M : Type u_1} [AddZeroClass M] (c : AddCon M) : ∀ (x x_1 : M), { toFun := AddCon.toQuotient, map_zero' := ⋯ }.toFun (x + x_1) = { toFun := AddCon.toQuotient, map_zero' := ⋯ }.toFun (x + x_1)

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 := AddCon.toQuotient, map_zero' := ⋯, map_add' := ⋯ }

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 := Con.toQuotient, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

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

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

@[simp]

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

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

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.

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.

@[simp]

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

@[simp]

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

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

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

theorem AddCon.comap_eq {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {c : AddCon M} {f : N →+ M} : AddCon.comap ⇑f ⋯ c = AddCon.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.

theorem Con.comap_eq {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {c : Con M} {f : N →* M} : Con.comap ⇑f ⋯ c = Con.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.lift.proof_1 {M : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) : (fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯) 0 = 0

def AddCon.lift {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.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 AddCon.lift.proof_2 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (c : AddCon M) (f : M →+ P) (H : c ≤ AddCon.ker f) (x : c.Quotient) (y : c.Quotient) : { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯ }.toFun (x + y) = { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯ }.toFun x + { toFun := fun (x : c.Quotient) => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯ }.toFun y

def Con.lift {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] (c : Con M) (f : M →* P) (H : c ≤ Con.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' := ⋯ }

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

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

theorem Con.lift_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.ker f) (x : M) : (c.lift f H) (c.mk' 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 ≤ AddCon.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_coe {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.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_comp_mk' {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.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_comp_mk' {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.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_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.

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

theorem AddCon.lift_funext {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} (f : c.Quotient →+ P) (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_funext {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} (f : c.Quotient →* P) (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_unique {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (H : c ≤ AddCon.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_unique {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (H : c ≤ Con.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_surjective_of_surjective {M : Type u_1} {P : Type u_3} [AddZeroClass M] [AddZeroClass P] {c : AddCon M} {f : M →+ P} (h : c ≤ AddCon.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.lift_surjective_of_surjective {M : Type u_1} {P : Type u_3} [MulOneClass M] [MulOneClass P] {c : Con M} {f : M →* P} (h : c ≤ Con.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.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 ≤ AddCon.ker f) (h : Function.Injective ⇑(c.lift f H)) : AddCon.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.

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 ≤ Con.ker f) (h : Function.Injective ⇑(c.lift f H)) : Con.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.kerLift.proof_1 {M : Type u_1} {P : Type u_2} [AddZeroClass M] [AddZeroClass P] (f : M →+ P) : ∀ (x x_1 : M), (AddCon.ker f) x x_1 → (AddCon.ker f) x x_1

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

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

@[simp]

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

@[simp]

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

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

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

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

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

def AddCon.map {M : Type u_1} [AddZeroClass M] (c : AddCon M) (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 AddCon.map.proof_1 {M : Type u_1} [AddZeroClass M] (c : AddCon M) (d : AddCon M) (h : c ≤ d) (x : M) (y : M) (hc : c x y) : (AddCon.ker d.mk') x y

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

theorem AddCon.map_apply {M : Type u_1} [AddZeroClass M] {c : AddCon M} {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.

theorem Con.map_apply {M : Type u_1} [MulOneClass M] {c : Con M} {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.