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 : { x // x AddMonoidHom.ker f } →+ A), AddMonoidHom.comp f u = AddMonoidHom.comp f vu = v) :
theorem MonoidHom.ker_eq_bot_of_cancel {A : Type u} {B : Type v} [Group A] [Group B] {f : A →* B} (h : ∀ (u v : { x // x MonoidHom.ker f } →* A), MonoidHom.comp f u = MonoidHom.comp f vu = v) :
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 MonoidHom.range f), MonoidHom.comp u f = MonoidHom.comp v fu = v) :

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) (x : GroupCat.SurjectiveOfEpiAuxs.XWithInfinity f) :
    (b * b') x = b b' x
    theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_eq_of_mem_range {A : GroupCat} {B : GroupCat} (f : A B) {b : B} (hb : b MonoidHom.range f) :
    GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = leftCoset b (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
    theorem GroupCat.SurjectiveOfEpiAuxs.fromCoset_ne_of_nin_range {A : GroupCat} {B : GroupCat} (f : A B) {b : B} (hb : ¬b MonoidHom.range f) :
    GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := leftCoset b (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = leftCoset b (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) } GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }

    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.tau f) GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }
      theorem GroupCat.SurjectiveOfEpiAuxs.τ_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
      ↑(GroupCat.SurjectiveOfEpiAuxs.tau f) (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
      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 { val := leftCoset x (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = leftCoset x (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
      theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_fromCoset {A : GroupCat} {B : GroupCat} (f : A B) :
      (GroupCat.SurjectiveOfEpiAuxs.tau f).symm (GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier) }) = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity
      theorem GroupCat.SurjectiveOfEpiAuxs.τ_symm_apply_infinity {A : GroupCat} {B : GroupCat} (f : A B) :
      (GroupCat.SurjectiveOfEpiAuxs.tau f).symm GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = GroupCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset { val := (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier, property := (_ : y, Function.swap leftCoset (MonoidHom.range f).toSubmonoid.toSubsemigroup.carrier y = (MonoidHom.range f).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

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