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 MonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [Group A] [Group B] {f : A →* B} (h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v) : f.ker = ⊥

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

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 ⧸ f.range), u.comp f = v.comp f → u = v) : f.range = ⊤

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 ⧸ f.range), u.comp f = v.comp f → u = v) : f.range = ⊤

theorem GrpCat.ker_eq_bot_of_mono {A B : GrpCat} (f : A ⟶ B) [CategoryTheory.Mono f] : (Hom.hom f).ker = ⊥

theorem AddGrpCat.ker_eq_bot_of_mono {A B : AddGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f] : (Hom.hom f).ker = ⊥

theorem GrpCat.mono_iff_ker_eq_bot {A B : GrpCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ (Hom.hom f).ker = ⊥

theorem AddGrpCat.mono_iff_ker_eq_bot {A B : AddGrpCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ (Hom.hom f).ker = ⊥

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

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

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

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

• fromCoset {A B : GrpCat} {f : A ⟶ B} : ↑(Set.range fun (x : ↑B) => x • ↑(Hom.hom f).range) → XWithInfinity f
• infinity {A B : GrpCat} {f : A ⟶ B} : XWithInfinity f

@[implicit_reducible]

instance GrpCat.SurjectiveOfEpiAuxs.instSMulCarrierXWithInfinity {A B : GrpCat} (f : A ⟶ B) : SMul (↑B) (XWithInfinity f)

theorem GrpCat.SurjectiveOfEpiAuxs.mul_smul {A B : GrpCat} (f : A ⟶ B) (b b' : ↑B) (x : XWithInfinity f) : (b * b') • x = b • b' • x

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

theorem GrpCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range {A B : GrpCat} (f : A ⟶ B) {b : ↑B} (hb : b ∈ (Hom.hom f).range) : XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

theorem GrpCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A B : GrpCat} (f : A ⟶ B) {b : ↑B} (hb : b ∉ (Hom.hom f).range) : XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

@[implicit_reducible]

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

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

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

theorem GrpCat.SurjectiveOfEpiAuxs.τ_apply_infinity {A B : GrpCat} (f : A ⟶ B) : (tau f) XWithInfinity.infinity = XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

theorem GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset {A B : GrpCat} (f : A ⟶ B) : (tau f) (XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.infinity

theorem GrpCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' {A B : GrpCat} (f : A ⟶ B) (x : ↑B) (hx : x ∈ (Hom.hom f).range) : (tau f) (XWithInfinity.fromCoset ⟨x • ↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.infinity

theorem GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset {A B : GrpCat} (f : A ⟶ B) : (Equiv.symm (tau f)) (XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.infinity

theorem GrpCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity {A B : GrpCat} (f : A ⟶ B) : (Equiv.symm (tau f)) XWithInfinity.infinity = XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

def GrpCat.SurjectiveOfEpiAuxs.g {A B : GrpCat} (f : A ⟶ B) : ↑B →* Equiv.Perm (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.

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

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

The strategy is the following: assuming epi f

• prove that f.hom.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.hom.range, then h x ≠ g x at the coset f.hom.range.

theorem GrpCat.SurjectiveOfEpiAuxs.g_apply_fromCoset {A B : GrpCat} (f : A ⟶ B) (x : ↑B) (y : ↑(Set.range fun (x : ↑B) => x • ↑(Hom.hom f).range)) : ((g f) x) (XWithInfinity.fromCoset y) = XWithInfinity.fromCoset ⟨x • ↑y, ⋯⟩

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

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

theorem GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset {A B : GrpCat} (f : A ⟶ B) (x : ↑B) : ((h f) x) (XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

theorem GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset' {A B : GrpCat} (f : A ⟶ B) (x b : ↑B) (hb : b ∈ (Hom.hom f).range) : ((h f) x) (XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩

theorem GrpCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range {A B : GrpCat} (f : A ⟶ B) (x : ↑B) (hx : x ∈ (Hom.hom f).range) (b : ↑B) (hb : b ∉ (Hom.hom f).range) : ((h f) x) (XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩) = XWithInfinity.fromCoset ⟨(x * b) • ↑(Hom.hom f).range, ⋯⟩

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

theorem GrpCat.SurjectiveOfEpiAuxs.comp_eq {A B : GrpCat} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp f (ofHom (g f)) = CategoryTheory.CategoryStruct.comp f (ofHom (h f))

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

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

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

theorem GrpCat.epi_iff_range_eq_top {A B : GrpCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ (Hom.hom f).range = ⊤

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

theorem AddGrpCat.epi_iff_range_eq_top {A B : AddGrpCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ (Hom.hom f).range = ⊤

instance GrpCat.forget_grp_preserves_mono : (CategoryTheory.forget GrpCat).PreservesMonomorphisms

instance AddGrpCat.forget_grp_preserves_mono : (CategoryTheory.forget AddGrpCat).PreservesMonomorphisms

instance GrpCat.forget_grp_preserves_epi : (CategoryTheory.forget GrpCat).PreservesEpimorphisms

instance AddGrpCat.forget_grp_preserves_epi : (CategoryTheory.forget AddGrpCat).PreservesEpimorphisms

theorem CommGrpCat.ker_eq_bot_of_mono {A B : CommGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f] : (Hom.hom f).ker = ⊥

theorem AddCommGrpCat.ker_eq_bot_of_mono {A B : AddCommGrpCat} (f : A ⟶ B) [CategoryTheory.Mono f] : (Hom.hom f).ker = ⊥

theorem CommGrpCat.mono_iff_ker_eq_bot {A B : CommGrpCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ (Hom.hom f).ker = ⊥

theorem AddCommGrpCat.mono_iff_ker_eq_bot {A B : AddCommGrpCat} (f : A ⟶ B) : CategoryTheory.Mono f ↔ (Hom.hom f).ker = ⊥

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

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

theorem CommGrpCat.range_eq_top_of_epi {A B : CommGrpCat} (f : A ⟶ B) [CategoryTheory.Epi f] : (Hom.hom f).range = ⊤

theorem AddCommGrpCat.range_eq_top_of_epi {A B : AddCommGrpCat} (f : A ⟶ B) [CategoryTheory.Epi f] : (Hom.hom f).range = ⊤

theorem CommGrpCat.epi_iff_range_eq_top {A B : CommGrpCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ (Hom.hom f).range = ⊤

theorem AddCommGrpCat.epi_iff_range_eq_top {A B : AddCommGrpCat} (f : A ⟶ B) : CategoryTheory.Epi f ↔ (Hom.hom f).range = ⊤

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

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

instance CommGrpCat.forget_commGrp_preserves_mono : (CategoryTheory.forget CommGrpCat).PreservesMonomorphisms

instance AddCommGrpCat.forget_commGrp_preserves_mono : (CategoryTheory.forget AddCommGrpCat).PreservesMonomorphisms

instance CommGrpCat.forget_commGrp_preserves_epi : (CategoryTheory.forget CommGrpCat).PreservesEpimorphisms

instance AddCommGrpCat.forget_commGrp_preserves_epi : (CategoryTheory.forget AddCommGrpCat).PreservesEpimorphisms