Documentation

Mathlib.GroupTheory.Abelianization

The abelianization of a group #

This file defines the commutator and the abelianization of a group. It furthermore prepares for the result that the abelianization is left adjoint to the forgetful functor from abelian groups to groups, which can be found in Algebra/Category/Group/Adjunctions.

Main definitions #

def commutator (G : Type u) [Group G] :

The commutator subgroup of a group G is the normal subgroup generated by the commutators [p,q]=p*q*p⁻¹*q⁻¹.

Equations
Instances For
    instance instNormalCommutator (G : Type u) [Group G] :
    (commutator G).Normal
    Equations
    • =
    instance commutator_characteristic (G : Type u) [Group G] :
    (commutator G).Characteristic
    Equations
    • =
    def Abelianization (G : Type u) [Group G] :

    The abelianization of G is the quotient of G by its commutator subgroup.

    Equations
    Instances For
      Equations
      • =

      of is the canonical projection from G to its abelianization.

      Equations
      • Abelianization.of = { toFun := QuotientGroup.mk, map_one' := , map_mul' := }
      Instances For
        @[simp]
        theorem Abelianization.mk_eq_of {G : Type u} [Group G] (a : G) :
        Quot.mk Setoid.r a = Abelianization.of a
        theorem Abelianization.commutator_subset_ker {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) :
        commutator G f.ker
        def Abelianization.lift {G : Type u} [Group G] {A : Type v} [CommGroup A] :

        If f : G → A is a group homomorphism to an abelian group, then lift f is the unique map from the abelianization of a G to A that factors through f.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Abelianization.lift.of {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (x : G) :
          (Abelianization.lift f) (Abelianization.of x) = f x
          theorem Abelianization.lift.unique {G : Type u} [Group G] {A : Type v} [CommGroup A] (f : G →* A) (φ : Abelianization G →* A) (hφ : ∀ (x : G), φ (Abelianization.of x) = f x) {x : Abelianization G} :
          φ x = (Abelianization.lift f) x
          @[simp]
          theorem Abelianization.lift_of {G : Type u} [Group G] :
          Abelianization.lift Abelianization.of = MonoidHom.id (Abelianization G)
          theorem Abelianization.hom_ext {G : Type u} [Group G] {A : Type v} [Monoid A] (φ : Abelianization G →* A) (ψ : Abelianization G →* A) (h : φ.comp Abelianization.of = ψ.comp Abelianization.of) :
          φ = ψ

          See note [partially-applied ext lemmas].

          def Abelianization.map {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :

          The map operation of the Abelianization functor

          Equations
          Instances For
            @[simp]
            theorem Abelianization.lift_of_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) :
            Abelianization.lift (Abelianization.of.comp f) = Abelianization.map f

            Use map as the preferred simp normal form.

            @[simp]
            theorem Abelianization.map_of {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) (x : G) :
            (Abelianization.map f) (Abelianization.of x) = Abelianization.of (f x)
            @[simp]
            theorem Abelianization.map_comp {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] (g : H →* I) :
            @[simp]
            theorem Abelianization.map_map_apply {G : Type u} [Group G] {H : Type v} [Group H] (f : G →* H) {I : Type w} [Group I] {g : H →* I} {x : Abelianization G} :

            Equivalent groups have equivalent abelianizations

            Equations
            Instances For
              @[simp]
              theorem abelianizationCongr_of {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) (x : G) :
              e.abelianizationCongr (Abelianization.of x) = Abelianization.of (e x)
              @[simp]
              theorem abelianizationCongr_refl {G : Type u} [Group G] :
              (MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)
              @[simp]
              theorem abelianizationCongr_symm {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) :
              e.abelianizationCongr.symm = e.symm.abelianizationCongr
              @[simp]
              theorem abelianizationCongr_trans {G : Type u} [Group G] {H : Type v} [Group H] (e : G ≃* H) {I : Type v} [Group I] (e₂ : H ≃* I) :
              e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr
              @[simp]
              theorem Abelianization.equivOfComm_apply {H : Type u_1} [CommGroup H] (a : H) :
              Abelianization.equivOfComm a = Abelianization.of a
              @[simp]
              theorem Abelianization.equivOfComm_symm_apply {H : Type u_1} [CommGroup H] (a : Abelianization H) :
              Abelianization.equivOfComm.symm a = (Abelianization.lift (MonoidHom.id H)) a

              An Abelian group is equivalent to its own abelianization.

              Equations
              • Abelianization.equivOfComm = let __src := Abelianization.of; { toFun := Abelianization.of, invFun := (Abelianization.lift (MonoidHom.id H)), left_inv := , right_inv := , map_mul' := }
              Instances For
                def commutatorRepresentatives (G : Type u) [Group G] :
                Set (G × G)

                Representatives (g₁, g₂) : G × G of commutators ⁅g₁, g₂⁆ ∈ G.

                Equations
                Instances For

                  Subgroup generated by representatives g₁ g₂ : G of commutators ⁅g₁, g₂⁆ ∈ G.

                  Equations
                  Instances For