Homomorphisms on a congruence quotient of a magma

Mathlib's Con API for quotient homomorphisms — Con.lift, Con.kerLift, Con.map and the isomorphism theorems — lives in section MulOneClass and is MonoidHom-valued. Its section Mul provides only Con.mkMulHom, Con.ker, Con.mapGen, Con.mapOfSurjective and Con.correspondence. This file adds the MulHom-valued lift, together with its universal property, the kernel lift, and the map induced by a coarsening.

Homomorphisms are consumed through MulHomClass and produced as concrete →ₙ*, following Con.ker and Con.mapOfSurjective. The cost of consuming through MulHomClass is that the universal-property statements coerce the argument, as in liftMulHom_comp_mkMulHom.

Main definitions

• Con.liftMulHom: the homomorphism induced on the quotient by one constant on the classes.
• Con.kerLiftMulHom: the homomorphism induced by f on the quotient by its kernel.
• Con.mapMulHom: the homomorphism c.Quotient →ₙ* d.Quotient induced by c ≤ d.

Main results

• Con.mulHom_ext, Con.liftMulHom_unique: the universal property of the quotient.
• Con.liftMulHom_injective, Con.kerLiftMulHom_injective: injectivity of the lifts.
• Con.ker_prod, Con.ker_prodMulHom: the kernel of a paired homomorphism is the meet of the kernels.

def Con.liftMulHom {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (c : Con M) (f : F) (H : c ≤ ker f) : c.Quotient →ₙ* N

The homomorphism on c.Quotient induced by a homomorphism constant on c's classes.

Equations

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

@[simp]

theorem Con.liftMulHom_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (c : Con M) (f : F) (H : c ≤ ker f) (x : M) : (c.liftMulHom f H) ↑x = f x

@[simp]

theorem Con.liftMulHom_comp_mkMulHom {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (c : Con M) (f : F) (H : c ≤ ker f) : (c.liftMulHom f H).comp c.mkMulHom = ↑f

theorem Con.mkMulHom_surjective {M : Type u_1} [Mul M] (c : Con M) : Function.Surjective ⇑c.mkMulHom

The quotient map is surjective.

theorem Con.liftMulHom_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] {c : Con M} {f : F} (H : c ≤ ker f) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(c.liftMulHom f H)

theorem Con.liftMulHom_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] {c : Con M} {f : F} {H : c ≤ ker f} (H' : ker f ≤ c) : Function.Injective ⇑(c.liftMulHom f H)

The lift is injective when the kernel of f refines the congruence.

theorem Con.liftMulHom_apply_mkMulHom {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (f : c.Quotient →ₙ* N) : c.liftMulHom (f.comp c.mkMulHom) ⋯ = f

Every homomorphism out of the quotient is the lift of its restriction.

theorem Con.mulHom_ext {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) {f g : c.Quotient →ₙ* N} (h : f.comp c.mkMulHom = g.comp c.mkMulHom) : f = g

Extensionality for homomorphisms out of a congruence quotient: they agree as soon as they agree on the quotient map.

theorem Con.mulHom_ext_iff {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {c : Con M} {f g : c.Quotient →ₙ* N} : f = g ↔ f.comp c.mkMulHom = g.comp c.mkMulHom

theorem Con.liftMulHom_funext {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (c : Con M) (f g : c.Quotient →ₙ* N) (h : ∀ (a : M), f ↑a = g ↑a) : f = g

theorem Con.liftMulHom_unique {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (c : Con M) {f : F} (H : c ≤ ker f) (g : c.Quotient →ₙ* N) (Hg : g.comp c.mkMulHom = ↑f) : g = c.liftMulHom f H

The universal property: the lift is the unique homomorphism restricting to f.

def Con.kerLiftMulHom {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (f : F) : (ker f).Quotient →ₙ* N

The homomorphism induced by f on the quotient by its kernel.

Equations

• Con.kerLiftMulHom f = (Con.ker f).liftMulHom f ⋯

@[simp]

theorem Con.kerLiftMulHom_coe {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (f : F) (x : M) : (kerLiftMulHom f) ↑x = f x

theorem Con.kerLiftMulHom_injective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] (f : F) : Function.Injective ⇑(kerLiftMulHom f)

The kernel lift is injective: it exhibits (ker f).Quotient as a sub-object of N, which is what closure-under-quotient arguments consume.

theorem Con.kerLiftMulHom_surjective_of_surjective {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {F : Type u_3} [FunLike F M N] [MulHomClass F M N] {f : F} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(kerLiftMulHom f)

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

The homomorphism of quotients induced by a coarsening c ≤ d.

Equations

• c.mapMulHom d h = c.liftMulHom d.mkMulHom ⋯

@[simp]

theorem Con.mapMulHom_coe {M : Type u_1} [Mul M] (c d : Con M) (h : c ≤ d) (x : M) : (c.mapMulHom d h) ↑x = ↑x

theorem Con.mapMulHom_surjective {M : Type u_1} [Mul M] (c d : Con M) (h : c ≤ d) : Function.Surjective ⇑(c.mapMulHom d h)

Kernels of paired homomorphisms

theorem Con.ker_prodMulHom {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] {N' : Type u_4} [Mul N'] (f : M →ₙ* N) (g : M →ₙ* N') : ker (f.prod g) = ker f ⊓ ker g

The kernel of a paired homomorphism is the meet of the kernels.

theorem Con.ker_prod {M : Type u_4} {N : Type u_5} {N' : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass N'] (f : M →* N) (g : M →* N') : ker (f.prod g) = ker f ⊓ ker g

The kernel of a paired monoid homomorphism is the meet of the kernels.