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 = ⊤

instance Grp.instGroupCarrier (G : Grp) : Group ↑G

Equations

• G.instGroupCarrier = G.str

instance AddGrp.instAddGroupCarrier (G : AddGrp) : AddGroup ↑G

Equations

• G.instAddGroupCarrier = G.str

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

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

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

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

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

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

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

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

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

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

Equations

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

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

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

theorem Grp.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range {A B : Grp} (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 Grp.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A B : Grp} (f : A ⟶ B) {b : ↑B} (hb : b ∉ (Hom.hom f).range) : XWithInfinity.fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ ≠ XWithInfinity.fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

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

Equations

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

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

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

Equations

• Grp.SurjectiveOfEpiAuxs.tau f = Equiv.swap (Grp.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(Grp.Hom.hom f).range, ⋯⟩) Grp.SurjectiveOfEpiAuxs.XWithInfinity.infinity

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

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

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

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

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

def Grp.SurjectiveOfEpiAuxs.g {A B : Grp} (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.

Equations

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

def Grp.SurjectiveOfEpiAuxs.h {A B : Grp} (f : A ⟶ B) : ↑B →* Equiv.Perm (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.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 Grp.SurjectiveOfEpiAuxs.g_apply_fromCoset {A B : Grp} (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 Grp.SurjectiveOfEpiAuxs.g_apply_infinity {A B : Grp} (f : A ⟶ B) (x : ↑B) : ((g f) x) XWithInfinity.infinity = XWithInfinity.infinity

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

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

theorem Grp.SurjectiveOfEpiAuxs.h_apply_fromCoset' {A B : Grp} (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 Grp.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range {A B : Grp} (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 Grp.SurjectiveOfEpiAuxs.agree {A B : Grp} (f : A ⟶ B) : ↑(Hom.hom f).range = {x : ↑B | (h f) x = (g f) x}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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