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} [AddGroup A] [AddGroup B] {f : A →+ B} (h : ∀ (u v : ↥(AddMonoidHom.ker f) →+ A), AddMonoidHom.comp f u = AddMonoidHom.comp f v → u = v) : AddMonoidHom.ker f = ⊥

theorem MonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [Group A] [Group B] {f : A →* B} (h : ∀ (u v : ↥(MonoidHom.ker f) →* A), MonoidHom.comp f u = MonoidHom.comp f v → u = v) : MonoidHom.ker f = ⊥

theorem AddMonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [AddCommGroup A] [AddCommGroup B] {f : A →+ B} (h : ∀ (u v : B →+ B ⧸ AddMonoidHom.range f), AddMonoidHom.comp u f = AddMonoidHom.comp v f → u = v) : AddMonoidHom.range f = ⊤

theorem MonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [CommGroup A] [CommGroup B] {f : A →* B} (h : ∀ (u v : B →* B ⧸ MonoidHom.range f), MonoidHom.comp u f = MonoidHom.comp v f → u = v) : MonoidHom.range f = ⊤

instance AddGroupCat.instGroupα_1 (G : AddGroupCat) : AddGroup ↑G

Equations

• AddGroupCat.instGroupα_1 G = G.str

instance GroupCat.instGroupα_1 (G : GroupCat) : Group ↑G

Equations

• GroupCat.instGroupα_1 G = G.str

theorem AddGroupCat.ker_eq_bot_of_mono {A : AddGroupCat} {B : AddGroupCat} (f : A ⟶ B) [CategoryTheory.Mono f] : AddMonoidHom.ker f = ⊥

theorem GroupCat.ker_eq_bot_of_mono {A : GroupCat} {B : GroupCat} (f : A ⟶ B) [CategoryTheory.Mono f] : MonoidHom.ker f = ⊥

theorem AddGroupCat.mono_iff_ker_eq_bot {A : AddGroupCat} {B : AddGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ AddMonoidHom.ker f = ⊥

theorem GroupCat.mono_iff_ker_eq_bot {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ MonoidHom.ker f = ⊥

theorem AddGroupCat.mono_iff_injective {A : AddGroupCat} {B : AddGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem GroupCat.mono_iff_injective {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

inductive GroupCat.SurjectiveOfEpiAuxs.XWithInfinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : Type u

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

• fromCoset: {A B : GroupCat} → {f : A ⟶ B} → ↑(Set.range fun (x : ↑B) => x • ↑(MonoidHom.range f)) → GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f
• infinity: {A B : GroupCat} → {f : A ⟶ B} → GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f

instance GroupCat.SurjectiveOfEpiAuxs.instSMulαGroupXWithInfinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : SMul (↑B) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

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) (x : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f) : (b * b') • x = b • b' • x

theorem GroupCat.SurjectiveOfEpiAuxs.one_smul {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f) : 1 • x = x

theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range {A : GroupCat} {B : GroupCat} (f : A ⟶ B) {b : ↑B} (hb : b ∈ MonoidHom.range f) : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := b • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = b • ↑(MonoidHom.range f)) } = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A : GroupCat} {B : GroupCat} (f : A ⟶ B) {b : ↑B} (hb : b ∉ MonoidHom.range f) : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := b • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = b • ↑(MonoidHom.range f)) } ≠ GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }

instance GroupCat.SurjectiveOfEpiAuxs.instDecidableEqXWithInfinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : DecidableEq (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

Equations

• GroupCat.SurjectiveOfEpiAuxs.instDecidableEqXWithInfinity f = Classical.decEq (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

noncomputable def GroupCat.SurjectiveOfEpiAuxs.tau {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : Equiv.Perm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

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

Equations

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

theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_infinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : (GroupCat.SurjectiveOfEpiAuxs.tau f) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : (GroupCat.SurjectiveOfEpiAuxs.tau f) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) (hx : x ∈ MonoidHom.range f) : (GroupCat.SurjectiveOfEpiAuxs.tau f) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := x • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = x • ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : (GroupCat.SurjectiveOfEpiAuxs.tau f).symm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : (GroupCat.SurjectiveOfEpiAuxs.tau f).symm GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }

def GroupCat.SurjectiveOfEpiAuxs.g {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : ↑B →* Equiv.Perm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

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.

def GroupCat.SurjectiveOfEpiAuxs.h {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : ↑B →* Equiv.Perm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f)

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

Equations

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

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 • ↑(MonoidHom.range f))) : ((GroupCat.SurjectiveOfEpiAuxs.g f) x) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset y) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := x • ↑y, property := (_ : x • ↑y ∈ Set.range fun (x : ↑B) => x • ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_infinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) : ((GroupCat.SurjectiveOfEpiAuxs.g f) x) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_infinity {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) (hx : x ∈ MonoidHom.range f) : ((GroupCat.SurjectiveOfEpiAuxs.h f) x) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) : ((GroupCat.SurjectiveOfEpiAuxs.h f) x) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) (b : ↑B) (hb : b ∈ MonoidHom.range f) : ((GroupCat.SurjectiveOfEpiAuxs.h f) x) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := b • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = b • ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := b • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = b • ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) (hx : x ∈ MonoidHom.range f) (b : ↑B) (hb : b ∉ MonoidHom.range f) : ((GroupCat.SurjectiveOfEpiAuxs.h f) x) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := b • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = b • ↑(MonoidHom.range f)) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (x * b) • ↑(MonoidHom.range f), property := (_ : ∃ (y : ↑B), (fun (x : ↑B) => x • ↑(MonoidHom.range f)) y = (x * b) • ↑(MonoidHom.range f)) }

theorem GroupCat.SurjectiveOfEpiAuxs.agree {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : ↑(MonoidHom.range f) = {x : ↑B | (GroupCat.SurjectiveOfEpiAuxs.h f) x = (GroupCat.SurjectiveOfEpiAuxs.g f) x}

theorem GroupCat.SurjectiveOfEpiAuxs.comp_eq {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f (let_fun this := GroupCat.SurjectiveOfEpiAuxs.g f; this) = CategoryTheory.CategoryStruct.comp f (let_fun this := GroupCat.SurjectiveOfEpiAuxs.h f; this)

theorem GroupCat.SurjectiveOfEpiAuxs.g_ne_h {A : GroupCat} {B : GroupCat} (f : A ⟶ B) (x : ↑B) (hx : x ∉ MonoidHom.range f) : GroupCat.SurjectiveOfEpiAuxs.g f ≠ GroupCat.SurjectiveOfEpiAuxs.h f

theorem GroupCat.surjective_of_epi {A : GroupCat} {B : GroupCat} (f : A ⟶ B) [CategoryTheory.Epi f] : Function.Surjective ⇑f

theorem GroupCat.epi_iff_surjective {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem GroupCat.epi_iff_range_eq_top {A : GroupCat} {B : GroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ MonoidHom.range f = ⊤

theorem AddGroupCat.epi_iff_surjective {A : AddGroupCat} {B : AddGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem AddGroupCat.epi_iff_range_eq_top {A : AddGroupCat} {B : AddGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ AddMonoidHom.range f = ⊤

instance AddGroupCat.forget_groupCat_preserves_mono : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget AddGroupCat)

Equations

• AddGroupCat.forget_groupCat_preserves_mono = (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget AddGroupCat))

instance GroupCat.forget_groupCat_preserves_mono : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget GroupCat)

Equations

• GroupCat.forget_groupCat_preserves_mono = (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget GroupCat))

instance AddGroupCat.forget_groupCat_preserves_epi : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget AddGroupCat)

Equations

• AddGroupCat.forget_groupCat_preserves_epi = (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget AddGroupCat))

instance GroupCat.forget_groupCat_preserves_epi : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget GroupCat)

Equations

• GroupCat.forget_groupCat_preserves_epi = (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget GroupCat))

theorem AddCommGroupCat.ker_eq_bot_of_mono {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) [CategoryTheory.Mono f] : AddMonoidHom.ker f = ⊥

theorem CommGroupCat.ker_eq_bot_of_mono {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) [CategoryTheory.Mono f] : MonoidHom.ker f = ⊥

theorem AddCommGroupCat.mono_iff_ker_eq_bot {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ AddMonoidHom.ker f = ⊥

theorem CommGroupCat.mono_iff_ker_eq_bot {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ MonoidHom.ker f = ⊥

theorem AddCommGroupCat.mono_iff_injective {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem CommGroupCat.mono_iff_injective {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem AddCommGroupCat.range_eq_top_of_epi {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) [CategoryTheory.Epi f] : AddMonoidHom.range f = ⊤

theorem CommGroupCat.range_eq_top_of_epi {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) [CategoryTheory.Epi f] : MonoidHom.range f = ⊤

instance AddCommGroupCat.instAddCommGroupObjAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryTypeTypesToPrefunctorForgetConcreteCategory (G : AddCommGroupCat) : AddCommGroup ((CategoryTheory.forget AddCommGroupCat).toPrefunctor.obj G)

Equations

• AddCommGroupCat.instAddCommGroupObjAddCommGroupCatToQuiverToCategoryStructInstAddCommGroupCatLargeCategoryTypeTypesToPrefunctorForgetConcreteCategory G = G.str

instance CommGroupCat.instCommGroupObjCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryTypeTypesToPrefunctorForgetConcreteCategory (G : CommGroupCat) : CommGroup ((CategoryTheory.forget CommGroupCat).toPrefunctor.obj G)

Equations

• CommGroupCat.instCommGroupObjCommGroupCatToQuiverToCategoryStructInstCommGroupCatLargeCategoryTypeTypesToPrefunctorForgetConcreteCategory G = G.str

theorem AddCommGroupCat.epi_iff_range_eq_top {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ AddMonoidHom.range f = ⊤

theorem CommGroupCat.epi_iff_range_eq_top {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ MonoidHom.range f = ⊤

theorem AddCommGroupCat.epi_iff_surjective {A : AddCommGroupCat} {B : AddCommGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem CommGroupCat.epi_iff_surjective {A : CommGroupCat} {B : CommGroupCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

instance AddCommGroupCat.forget_commGroupCat_preserves_mono : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget AddCommGroupCat)

Equations

• AddCommGroupCat.forget_commGroupCat_preserves_mono = (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget AddCommGroupCat))

instance CommGroupCat.forget_commGroupCat_preserves_mono : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget CommGroupCat)

Equations

• CommGroupCat.forget_commGroupCat_preserves_mono = (_ : CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.forget CommGroupCat))

instance AddCommGroupCat.forget_commGroupCat_preserves_epi : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget AddCommGroupCat)

Equations

• AddCommGroupCat.forget_commGroupCat_preserves_epi = (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget AddCommGroupCat))

instance CommGroupCat.forget_commGroupCat_preserves_epi : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget CommGroupCat)

Equations

• CommGroupCat.forget_commGroupCat_preserves_epi = (_ : CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.forget CommGroupCat))