mathlib documentation

algebra.category.Group.epi_mono

Monomorphisms and epimorphisms in Group #

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 vu = 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 vu = 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 fu = v) :
theorem add_monoid_hom.range_eq_top_of_cancel {A : Type u} {B : Type v} [add_comm_group A] [add_comm_group B] {f : A →+ B} (h : ∀ (u v : B →+ B f.range), u.comp f = v.comp fu = v) :
@[nolint]
inductive Group.surjective_of_epi_auxs.X_with_infinity {A B : Group} (f : A B) :
Type u

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) (x : Group.surjective_of_epi_auxs.X_with_infinity f) :
(b * b') x = b b' x

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

The strategy is the following: assuming epi f