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.

  • inl : N →+ E

    The inclusion homomorphism N →+ E

  • rightHom : E →+ G

    The projection homomorphism E →+ G

  • inl_injective : Function.Injective self.inl

    The inclusion map is injective.

  • range_inl_eq_ker_rightHom : self.inl.range = self.rightHom.ker

    The range of the inclusion map is equal to the kernel of the projection map.

  • rightHom_surjective : Function.Surjective self.rightHom

    The projection map is surjective.

Instances For
    theorem AddGroupExtension.inl_injective {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) :
    Function.Injective self.inl

    The inclusion map is injective.

    theorem AddGroupExtension.range_inl_eq_ker_rightHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) :
    self.inl.range = self.rightHom.ker

    The range of the inclusion map is equal to the kernel of the projection map.

    theorem AddGroupExtension.rightHom_surjective {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (self : AddGroupExtension N E G) :
    Function.Surjective self.rightHom

    The projection map is surjective.

    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.

    • inl : N →* E

      The inclusion homomorphism N →* E

    • rightHom : E →* G

      The projection homomorphism E →* G

    • inl_injective : Function.Injective self.inl

      The inclusion map is injective.

    • range_inl_eq_ker_rightHom : self.inl.range = self.rightHom.ker

      The range of the inclusion map is equal to the kernel of the projection map.

    • rightHom_surjective : Function.Surjective self.rightHom

      The projection map is surjective.

    Instances For
      theorem GroupExtension.inl_injective {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) :
      Function.Injective self.inl

      The inclusion map is injective.

      theorem GroupExtension.range_inl_eq_ker_rightHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) :
      self.inl.range = self.rightHom.ker

      The range of the inclusion map is equal to the kernel of the projection map.

      theorem GroupExtension.rightHom_surjective {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (self : GroupExtension N E G) :
      Function.Surjective self.rightHom

      The projection map is surjective.

      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) :
      Type (max u_2 u_4)

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

      • toAddMonoidHom : E →+ E'

        The homomorphism

      • inl_comm : self.toAddMonoidHom.comp S.inl = S'.inl

        The left-hand side of the diagram commutes.

      • rightHom_comm : S'.rightHom.comp self.toAddMonoidHom = S.rightHom

        The right-hand side of the diagram commutes.

      Instances For
        theorem AddGroupExtension.Equiv.inl_comm {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} (self : S.Equiv S') :
        self.toAddMonoidHom.comp S.inl = S'.inl

        The left-hand side of the diagram commutes.

        theorem AddGroupExtension.Equiv.rightHom_comm {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} (self : S.Equiv S') :
        S'.rightHom.comp self.toAddMonoidHom = S.rightHom

        The right-hand side of the diagram commutes.

        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) :
        Type (max u_2 u_3)

        Splitting of an additive group extension is a section homomorphism.

        • sectionHom : G →+ E

          A section homomorphism

        • rightHom_comp_sectionHom : S.rightHom.comp self.sectionHom = AddMonoidHom.id G

          The section is a left inverse of the projection map.

        Instances For
          theorem AddGroupExtension.Splitting.rightHom_comp_sectionHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] {S : AddGroupExtension N E G} (self : S.Splitting) :
          S.rightHom.comp self.sectionHom = AddMonoidHom.id G

          The section is a left inverse of the projection map.

          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) :
          S.inl.range.Normal

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

          Equations
          • =
          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) :
          S.inl.range.Normal

          The range of the inclusion map is a normal subgroup.

          Equations
          • =
          @[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_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_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) :
          S.rightHom.comp S.inl = 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) :
          S.rightHom.comp S.inl = 1
          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) :
            Type (max u_2 u_4)

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

            • toMonoidHom : E →* E'

              The homomorphism

            • inl_comm : self.toMonoidHom.comp S.inl = S'.inl

              The left-hand side of the diagram commutes.

            • rightHom_comm : S'.rightHom.comp self.toMonoidHom = S.rightHom

              The right-hand side of the diagram commutes.

            Instances For
              theorem GroupExtension.Equiv.inl_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' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S') :
              self.toMonoidHom.comp S.inl = S'.inl

              The left-hand side of the diagram commutes.

              theorem GroupExtension.Equiv.rightHom_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' : Type u_4} [Group E'] {S' : GroupExtension N E' G} (self : S.Equiv S') :
              S'.rightHom.comp self.toMonoidHom = S.rightHom

              The right-hand side of the diagram commutes.

              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) :
              Type (max u_2 u_3)

              Splitting of a group extension is a section homomorphism.

              • sectionHom : G →* E

                A section homomorphism

              • rightHom_comp_sectionHom : S.rightHom.comp self.sectionHom = MonoidHom.id G

                The section is a left inverse of the projection map.

              Instances For
                theorem GroupExtension.Splitting.rightHom_comp_sectionHom {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] {S : GroupExtension N E G} (self : S.Splitting) :
                S.rightHom.comp self.sectionHom = MonoidHom.id G

                The section is a left inverse of the projection map.

                instance AddGroupExtension.instFunLikeSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
                FunLike S.Splitting G E
                Equations
                • S.instFunLikeSplitting = { coe := fun (s : S.Splitting) => s.sectionHom, coe_injective' := }
                theorem AddGroupExtension.instFunLikeSplitting.proof_1 {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
                ∀ ⦃h : S.Splitting⦄ ⦃a₂ : S.Splitting⦄, (fun (s : S.Splitting) => s.sectionHom) h = (fun (s : S.Splitting) => s.sectionHom) a₂h = a₂
                instance GroupExtension.instFunLikeSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                FunLike S.Splitting G E
                Equations
                • S.instFunLikeSplitting = { coe := fun (s : S.Splitting) => s.sectionHom, coe_injective' := }
                instance AddGroupExtension.instAddMonoidHomClassSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [AddGroup N] [AddGroup E] [AddGroup G] (S : AddGroupExtension N E G) :
                AddMonoidHomClass S.Splitting G E
                Equations
                • =
                instance GroupExtension.instMonoidHomClassSplitting {N : Type u_1} {E : Type u_2} {G : Type u_3} [Group N] [Group E] [Group G] (S : GroupExtension N E G) :
                MonoidHomClass S.Splitting G E
                Equations
                • =
                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.Splitting) (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
                • S.IsConj s s' = ∃ (n : N), s.sectionHom = fun (g : G) => S.inl n + s'.sectionHom g + -S.inl n
                Instances For
                  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.Splitting) (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
                  • S.IsConj s s' = ∃ (n : N), s.sectionHom = fun (g : G) => S.inl n * s'.sectionHom g * (S.inl n)⁻¹
                  Instances For
                    def SemidirectProduct.toGroupExtension {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) :
                    GroupExtension N (N ⋊[φ] G) G

                    The group extension associated to the semidirect product

                    Equations
                    • SemidirectProduct.toGroupExtension φ = { inl := SemidirectProduct.inl, rightHom := SemidirectProduct.rightHom, inl_injective := , range_inl_eq_ker_rightHom := , rightHom_surjective := }
                    Instances For
                      theorem SemidirectProduct.toGroupExtension_inl {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) :
                      (SemidirectProduct.toGroupExtension φ).inl = SemidirectProduct.inl
                      theorem SemidirectProduct.toGroupExtension_rightHom {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) :
                      (SemidirectProduct.toGroupExtension φ).rightHom = SemidirectProduct.rightHom
                      def SemidirectProduct.inr_splitting {N : Type u_1} {G : Type u_3} [Group G] [Group N] (φ : G →* MulAut N) :

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

                      Equations
                      Instances For