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} [AddGroup A] [AddGroup B] {f : A →+ B} (h : ∀ (u v : f.ker →+ A), f.comp u = f.comp vu = v) :
f.ker =
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 vu = v) :
f.ker =
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 fu = v) :
f.range =
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 fu = v) :
f.range =
Equations
  • G.instGroupα_1 = G.str
Equations
  • G.instGroupα_1 = G.str

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

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    theorem GroupCat.SurjectiveOfEpiAuxs.mul_smul {A : GroupCat} {B : GroupCat} (f : A B) (b : B) (b' : B) (x : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f) :
    (b * b') x = b b' x

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

    Equations
    Instances For
      theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset' {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : x MonoidHom.range f) :
      (GroupCat.SurjectiveOfEpiAuxs.tau f) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset x (MonoidHom.range f), ) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity

      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.
      Instances For

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

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

          The strategy is the following: assuming epi f

          theorem GroupCat.SurjectiveOfEpiAuxs.g_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) (x : B) :
          ((GroupCat.SurjectiveOfEpiAuxs.g f) x) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
          theorem GroupCat.SurjectiveOfEpiAuxs.h_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) (x : B) (hx : x MonoidHom.range f) :
          ((GroupCat.SurjectiveOfEpiAuxs.h f) x) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
          Equations
          • G.instCommGroupObjForget = G.str