mathlib3documentation

algebra.category.Group.epi_mono

Monomorphisms and epimorphisms in Group#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we prove monomorphisms in category of group are injective homomorphisms and epimorphisms are surjective homomorphisms.

theorem monoid_hom.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) :
theorem add_monoid_hom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [add_group A] [add_group B] {f : A →+ B} (h : (u v : (f.ker) →+ A), f.comp u = f.comp v u = v) :
theorem monoid_hom.range_eq_top_of_cancel {A : Type u} {B : Type v} [comm_group A] [comm_group B] {f : A →* B} (h : (u v : B →* B f.range), u.comp f = v.comp f u = v) :
theorem add_monoid_hom.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 f u = v) :
theorem Group.ker_eq_bot_of_mono {A B : Group} (f : A B)  :
theorem Group.mono_iff_ker_eq_bot {A B : Group} (f : A B) :
theorem Group.mono_iff_injective {A B : Group} (f : A B) :
@[nolint]
inductive Group.surjective_of_epi_auxs.X_with_infinity {A B : Group} (f : A B) :

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

Instances for Group.surjective_of_epi_auxs.X_with_infinity
@[protected, instance]
Equations
theorem Group.surjective_of_epi_auxs.mul_smul {A B : Group} (f : A B) (b b' : B)  :
(b * b') x = b b' x
theorem Group.surjective_of_epi_auxs.one_smul {A B : Group} (f : A B)  :
1 x = x
theorem Group.surjective_of_epi_auxs.from_coset_eq_of_mem_range {A B : Group} (f : A B) {b : B} (hb : b ) :
theorem Group.surjective_of_epi_auxs.from_coset_ne_of_nin_range {A B : Group} (f : A B) {b : B} (hb : b ) :
@[protected, instance]
Equations
noncomputable def Group.surjective_of_epi_auxs.tau {A B : Group} (f : A B) :

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

Equations
theorem Group.surjective_of_epi_auxs.τ_apply_from_coset' {A B : Group} (f : A B) (x : B) (hx : x ) :
def Group.surjective_of_epi_auxs.G {A B : Group} (f : A B) :

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.

Equations
noncomputable def Group.surjective_of_epi_auxs.H {A B : Group} (f : A B) :

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

Equations

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 Group.surjective_of_epi_auxs.g_apply_from_coset {A B : Group} (f : A B) (x : B) (y : ) :
theorem Group.surjective_of_epi_auxs.h_apply_infinity {A B : Group} (f : A B) (x : B) (hx : x ) :
theorem Group.surjective_of_epi_auxs.h_apply_from_coset' {A B : Group} (f : A B) (x b : B) (hb : b ) :
theorem Group.surjective_of_epi_auxs.h_apply_from_coset_nin_range {A B : Group} (f : A B) (x : B) (hx : x ) (b : B) (hb : b ) :
theorem Group.surjective_of_epi_auxs.agree {A B : Group} (f : A B) :
= {x : B |
theorem Group.surjective_of_epi_auxs.comp_eq {A B : Group} (f : A B) :
(f show , from =
theorem Group.surjective_of_epi_auxs.g_ne_h {A B : Group} (f : A B) (x : B) (hx : x ) :
theorem Group.surjective_of_epi {A B : Group} (f : A B)  :
theorem Group.epi_iff_surjective {A B : Group} (f : A B) :
theorem Group.epi_iff_range_eq_top {A B : Group} (f : A B) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem CommGroup.ker_eq_bot_of_mono {A B : CommGroup} (f : A B)  :