# Monomorphisms and epimorphisms in Group#

In this file, we prove monomorphisms in the category of groups are injective homomorphisms and epimorphisms are surjective homomorphisms.

theorem AddMonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [] [] {f : A →+ B} (h : ∀ (u v : f.ker →+ A), f.comp u = f.comp vu = v) :
f.ker =
theorem MonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [] [] {f : A →* B} (h : ∀ (u v : f.ker →* A), f.comp u = f.comp vu = v) :
f.ker =
theorem AddMonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [] [] {f : A →+ B} (h : ∀ (u v : B →+ B f.range), u.comp f = v.comp fu = v) :
f.range =
theorem MonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [] [] {f : A →* B} (h : ∀ (u v : B →* B f.range), u.comp f = v.comp fu = v) :
f.range =
Equations
• G.instGroupα_1 = G.str
Equations
• G.instGroupα_1 = G.str
theorem GroupCat.ker_eq_bot_of_mono {A : GroupCat} {B : GroupCat} (f : A B) :
theorem GroupCat.mono_iff_injective {A : GroupCat} {B : GroupCat} (f : A B) :

Define X' to be the set of all left cosets with an extra point at "infinity".

Instances For
Equations
• One or more equations did not get rendered due to their size.
theorem GroupCat.SurjectiveOfEpiAuxs.mul_smul {A : GroupCat} {B : GroupCat} (f : A B) (b : B) (b' : B) :
(b * b') x = b b' x
theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range {A : GroupCat} {B : GroupCat} (f : A B) {b : B} (hb : ) :
theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A : GroupCat} {B : GroupCat} (f : A B) {b : B} (hb : b) :
noncomputable def GroupCat.SurjectiveOfEpiAuxs.tau {A : GroupCat} {B : GroupCat} (f : A B) :

Let τ be the permutation on X' exchanging f.range and the point at infinity.

Equations
• = Equiv.swap GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
Instances For
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) :
GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
= GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : ) :
= GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
= GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) :
GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =

Let g : B ⟶ S(X') be defined as such that, for any β : B, g(β) is the function sending point at infinity to point at infinity and sending coset y to β • y.

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

Define h : B ⟶ S(X') to be τ g τ⁻¹

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

The strategy is the following: assuming epi f

• prove that f.range = {x | h x = g x};
• thus f ≫ h = f ≫ g so that h = g;
• but if f is not surjective, then some x ∉ f.range, then h x ≠ g x at the coset f.range.
theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (y : (Set.range fun (x : B) => x ())) :
theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) (x : B) :
() GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : ) :
() GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (b : B) (hb : ) :
=
theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : ) (b : B) (hb : b) :
theorem GroupCat.SurjectiveOfEpiAuxs.agree {A : GroupCat} {B : GroupCat} (f : A B) :
() = {x : B | }
theorem GroupCat.SurjectiveOfEpiAuxs.comp_eq {A : GroupCat} {B : GroupCat} (f : A B) :
CategoryTheory.CategoryStruct.comp f (let_fun this := ; this) = CategoryTheory.CategoryStruct.comp f (let_fun this := ; this)
theorem GroupCat.SurjectiveOfEpiAuxs.g_ne_h {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : x) :
theorem GroupCat.surjective_of_epi {A : GroupCat} {B : GroupCat} (f : A B) :
theorem GroupCat.epi_iff_surjective {A : GroupCat} {B : GroupCat} (f : A B) :
.PreservesMonomorphisms
Equations
instance GroupCat.forget_groupCat_preserves_mono :
.PreservesMonomorphisms
Equations
.PreservesEpimorphisms
Equations
instance GroupCat.forget_groupCat_preserves_epi :
.PreservesEpimorphisms
Equations
Equations
Equations
• G.instCommGroupObjForget = G.str