Documentation

Mathlib.GroupTheory.GroupExtension.Defs

Group Extensions #

This file defines extensions of multiplicative and additive groups and their associated structures such as splittings and equivalences.

Main definitions #

For multiplicative groups:
      ↗︎ E  ↘
1 → N   ↓    G → 1
      ↘︎ E' ↗︎️

For additive groups:
      ↗︎ E  ↘
0 → N   ↓    G → 0
      ↘︎ E' ↗︎️

TODO #

If N is abelian,

structure AddGroupExtension (N : Type u_1) (E : Type u_2) (G : Type u_3) [AddGroup N] [AddGroup E] [AddGroup G] :
Type (max (max u_1 u_2) u_3)

AddGroupExtension N E G is a short exact sequence of additive groups 0 → N → E → G → 0.

Instances For
    structure GroupExtension (N : Type u_1) (E : Type u_2) (G : Type u_3) [Group N] [Group E] [Group G] :
    Type (max (max u_1 u_2) u_3)

    GroupExtension N E G is a short exact sequence of groups 1 → N → E → G → 1.

    Instances For
      structure AddGroupExtension.Equiv {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) {E' : Type u_4} [AddGroup E'] (S' : AddGroupExtension N E' G) extends E →+ E' :
      Type (max u_2 u_4)

      AddGroupExtensions are equivalent iff there is a homomorphism making a commuting diagram.

      Instances For
        structure AddGroupExtension.Section {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
        Type (max u_2 u_3)

        Section of an additive group extension is a right inverse to S.rightHom.

        Instances For
          structure AddGroupExtension.Splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) extends G →+ E, S.Section :
          Type (max u_2 u_3)

          Splitting of an additive group extension is a section homomorphism.

          Instances For
            instance GroupExtension.normal_inl_range {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :

            The range of the inclusion map is a normal subgroup.

            instance AddGroupExtension.normal_inl_range {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :

            The range of the inclusion map is a normal additive subgroup.

            @[simp]
            theorem GroupExtension.rightHom_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (n : N) :
            S.rightHom (S.inl n) = 1
            @[simp]
            theorem AddGroupExtension.rightHom_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (n : N) :
            S.rightHom (S.inl n) = 0
            @[simp]
            theorem GroupExtension.rightHom_comp_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
            @[simp]
            theorem AddGroupExtension.rightHom_comp_inl {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
            noncomputable def GroupExtension.conjAct {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :

            E acts on N by conjugation.

            Equations
            Instances For
              theorem GroupExtension.inl_conjAct_comm {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {e : E} {n : N} :
              S.inl ((S.conjAct e) n) = e * S.inl n * e⁻¹

              The inclusion and a conjugation commute.

              structure GroupExtension.Equiv {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) {E' : Type u_4} [Group E'] (S' : GroupExtension N E' G) extends E →* E' :
              Type (max u_2 u_4)

              GroupExtensions are equivalent iff there is a homomorphism making a commuting diagram.

              Instances For
                structure GroupExtension.Section {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                Type (max u_2 u_3)

                Section of a group extension is a right inverse to S.rightHom.

                Instances For
                  instance GroupExtension.Section.instFunLike {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                  Equations
                  instance AddGroupExtension.Section.instFunLike {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
                  Equations
                  @[simp]
                  theorem GroupExtension.Section.coe_mk {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : GE) (hσ : Function.RightInverse σ S.rightHom) :
                  @[simp]
                  @[simp]
                  theorem GroupExtension.Section.rightHom_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : S.Section) (g : G) :
                  S.rightHom (σ g) = g
                  @[simp]
                  theorem AddGroupExtension.Section.rightHom_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (σ : S.Section) (g : G) :
                  S.rightHom (σ g) = g
                  @[simp]
                  theorem GroupExtension.Section.rightHom_comp_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (σ : S.Section) :
                  @[simp]
                  theorem AddGroupExtension.Section.rightHom_comp_section {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (σ : S.Section) :
                  structure GroupExtension.Splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) extends G →* E, S.Section :
                  Type (max u_2 u_3)

                  Splitting of a group extension is a section homomorphism.

                  Instances For
                    instance GroupExtension.Splitting.instFunLike {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                    Equations
                    instance AddGroupExtension.Splitting.instFunLike {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
                    Equations
                    instance GroupExtension.Splitting.instMonoidHomClass {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                    @[simp]
                    @[simp]
                    theorem GroupExtension.Splitting.rightHom_splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (s : S.Splitting) (g : G) :
                    S.rightHom (s g) = g
                    @[simp]
                    theorem AddGroupExtension.Splitting.rightHom_splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (s : S.Splitting) (g : G) :
                    S.rightHom (s g) = g
                    @[simp]
                    theorem GroupExtension.Splitting.rightHom_comp_splitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (s : S.Splitting) :
                    def GroupExtension.IsConj {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) (s s' : S.Splitting) :

                    A splitting of an extension S is N-conjugate to another iff there exists n : N such that the section homomorphism is a conjugate of the other section homomorphism by S.inl n.

                    Equations
                    Instances For
                      def AddGroupExtension.IsConj {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) (s s' : S.Splitting) :

                      A splitting of an extension S is N-conjugate to another iff there exists n : N such that the section homomorphism is a conjugate of the other section homomorphism by S.inl n.

                      Equations
                      Instances For
                        def SemidirectProduct.toGroupExtension {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) :

                        The group extension associated to the semidirect product

                        Equations
                        Instances For

                          A canonical splitting of the group extension associated to the semidirect product

                          Equations
                          Instances For