# Documentation

Mathlib.Algebra.Category.GroupCat.EpiMono

# 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 : { x // } →+ A), u = v) :
theorem MonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [] [] {f : A →* B} (h : ∀ (u v : { x // } →* A), = u = v) :
theorem AddMonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [] [] {f : A →+ B} (h : ∀ (u v : B →+ ), u = v) :
theorem MonoidHom.range_eq_top_of_cancel {A : Type u} {B : Type v} [] [] {f : A →* B} (h : ∀ (u v : B →* ), = u = v) :
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
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 : ) :
GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset b ().toSubmonoid.toSubsemigroup.carrier) } = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }
theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A : GroupCat} {B : GroupCat} (f : A B) {b : B} (hb : ¬) :
GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset b ().toSubmonoid.toSubsemigroup.carrier) } GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }
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.

Instances For
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) :
↑() GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
↑() (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : ) :
↑() (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset x ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset x ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
().symm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) :
().symm GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }

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 β *l y.

Instances For

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

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 (Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier))) :
= GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset x y, property := (_ : leftCoset x y Set.range (Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier)) }
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) :
↑() (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = ().toSubmonoid.toSubsemigroup.carrier) }
theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (b : B) (hb : ) :
↑() (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset b ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset b ().toSubmonoid.toSubsemigroup.carrier) }
theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_fromCoset_nin_range {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : ) (b : B) (hb : ¬) :
↑() (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset b ().toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset (x * b) ().toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset ().toSubmonoid.toSubsemigroup.carrier y = leftCoset (x * b) ().toSubmonoid.toSubsemigroup.carrier) }
theorem GroupCat.SurjectiveOfEpiAuxs.agree {A : GroupCat} {B : GroupCat} (f : A B) :
().toSubmonoid.toSubsemigroup.carrier = {x | }
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 : ¬) :
theorem GroupCat.surjective_of_epi {A : GroupCat} {B : GroupCat} (f : A B) :
theorem GroupCat.epi_iff_surjective {A : GroupCat} {B : GroupCat} (f : A B) :