Documentation

Mathlib.GroupTheory.Nilpotent

Nilpotent groups #

An API for nilpotent groups, that is, groups for which the upper central series reaches .

Main definitions #

Recall that if H K : Subgroup G then ⁅H, K⁆ : Subgroup G is the subgroup of G generated by the commutators hkh⁻¹k⁻¹. Recall also Lean's conventions that denotes the subgroup G of G, and denotes the trivial subgroup {1}.

Main theorems #

G is defined to be nilpotent if the upper central series reaches .

Warning #

A "central series" is usually defined to be a finite sequence of normal subgroups going from to with the property that each subquotient is contained within the centre of the associated quotient of G. This means that if G is not nilpotent, then none of what we have called upperCentralSeries G, lowerCentralSeries G or the sequences satisfying IsAscendingCentralSeries or IsDescendingCentralSeries are actually central series. Note that the fact that the upper and lower central series are not central series if G is not nilpotent is a standard abuse of notation.

def upperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] :

If H is a normal subgroup of G, then the set {x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ H} is a subgroup of G (because it is the preimage in G of the centre of the quotient group G/H.)

Equations
Instances For
    theorem mem_upperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] (x : G) :
    x upperCentralSeriesStep H ∀ (y : G), x * y * x⁻¹ * y⁻¹ H

    The proof that upperCentralSeriesStep H is the preimage of the centre of G/H under the canonical surjection.

    instance instNormalUpperCentralSeriesStep {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] :
    Equations
    • =
    def upperCentralSeriesAux (G : Type u_1) [Group G] :
    (H : Subgroup G) ×' H.Normal

    An auxiliary type-theoretic definition defining both the upper central series of a group, and a proof that it is normal, all in one go.

    Equations
    Instances For
      def upperCentralSeries (G : Type u_1) [Group G] (n : ) :

      upperCentralSeries G n is the nth term in the upper central series of G.

      Equations
      Instances For
        instance upperCentralSeries_normal (G : Type u_1) [Group G] (n : ) :
        (upperCentralSeries G n).Normal
        Equations
        • =
        @[simp]
        theorem mem_upperCentralSeries_succ_iff {G : Type u_1} [Group G] {n : } {x : G} :
        x upperCentralSeries G (n + 1) ∀ (y : G), x * y * x⁻¹ * y⁻¹ upperCentralSeries G n

        The n+1st term of the upper central series H i has underlying set equal to the x such that ⁅x,G⁆ ⊆ H n

        @[simp]
        theorem comap_upperCentralSeries {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : H ≃* G) (n : ) :
        class Group.IsNilpotent (G : Type u_2) [Group G] :

        A group G is nilpotent if its upper central series is eventually G.

        Instances
          theorem Group.IsNilpotent.nilpotent' {G : Type u_2} :
          ∀ {inst : Group G} [self : Group.IsNilpotent G], ∃ (n : ), upperCentralSeries G n =
          theorem Group.isNilpotent_congr {G : Type u_1} [Group G] {H : Type u_2} [Group H] (e : G ≃* H) :

          A group G is virtually nilpotent if it has a nilpotent cofinite subgroup N.

          Equations
          Instances For
            def IsAscendingCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) :

            A sequence of subgroups of G is an ascending central series if H 0 is trivial and ⁅H (n + 1), G⁆ ⊆ H n for all n. Note that we do not require that H n = G for some n.

            Equations
            Instances For
              def IsDescendingCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) :

              A sequence of subgroups of G is a descending central series if H 0 is G and ⁅H n, G⁆ ⊆ H (n + 1) for all n. Note that we do not require that H n = {1} for some n.

              Equations
              Instances For

                Any ascending central series for a group is bounded above by the upper central series.

                The upper central series of a group is an ascending central series.

                A group G is nilpotent iff there exists an ascending central series which reaches G in finitely many steps.

                theorem is_decending_rev_series_of_is_ascending (G : Type u_1) [Group G] {H : Subgroup G} {n : } (hn : H n = ) (hasc : IsAscendingCentralSeries H) :
                IsDescendingCentralSeries fun (m : ) => H (n - m)
                theorem is_ascending_rev_series_of_is_descending (G : Type u_1) [Group G] {H : Subgroup G} {n : } (hn : H n = ) (hdesc : IsDescendingCentralSeries H) :
                IsAscendingCentralSeries fun (m : ) => H (n - m)

                A group G is nilpotent iff there exists a descending central series which reaches the trivial group in a finite time.

                def lowerCentralSeries (G : Type u_2) [Group G] :

                The lower central series of a group G is a sequence H n of subgroups of G, defined by H 0 is all of G and for n≥1, H (n + 1) = ⁅H n, G⁆

                Equations
                Instances For
                  @[simp]
                  theorem mem_lowerCentralSeries_succ_iff {G : Type u_1} [Group G] (n : ) (q : G) :
                  q lowerCentralSeries G (n + 1) q Subgroup.closure {x : G | plowerCentralSeries G n, q, p * q * p⁻¹ * q⁻¹ = x}
                  theorem lowerCentralSeries_succ {G : Type u_1} [Group G] (n : ) :
                  lowerCentralSeries G (n + 1) = Subgroup.closure {x : G | plowerCentralSeries G n, q, p * q * p⁻¹ * q⁻¹ = x}
                  instance lowerCentralSeries_normal {G : Type u_1} [Group G] (n : ) :
                  (lowerCentralSeries G n).Normal
                  Equations
                  • =

                  The lower central series of a group is a descending central series.

                  Any descending central series for a group is bounded below by the lower central series.

                  A group is nilpotent if and only if its lower central series eventually reaches the trivial subgroup.

                  noncomputable def Group.nilpotencyClass (G : Type u_1) [Group G] [hG : Group.IsNilpotent G] :

                  The nilpotency class of a nilpotent group is the smallest natural n such that the n'th term of the upper central series is G.

                  Equations
                  Instances For

                    The nilpotency class of a nilpotent G is equal to the smallest n for which an ascending central series reaches G in its n'th term.

                    The nilpotency class of a nilpotent G is equal to the smallest n for which the descending central series reaches in its n'th term.

                    The nilpotency class of a nilpotent G is equal to the length of the lower central series.

                    instance Subgroup.isNilpotent {G : Type u_1} [Group G] (H : Subgroup G) [hG : Group.IsNilpotent G] :

                    A subgroup of a nilpotent group is nilpotent

                    Equations
                    • =

                    The nilpotency class of a subgroup is less or equal to the nilpotency class of the group

                    @[instance 100]
                    Equations
                    • =
                    theorem upperCentralSeries.map {G : Type u_1} [Group G] {H : Type u_2} [Group H] {f : G →* H} (h : Function.Surjective f) (n : ) :
                    theorem lowerCentralSeries.map {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (n : ) :
                    theorem isNilpotent_of_ker_le_center {G : Type u_1} [Group G] {H : Type u_2} [Group H] (f : G →* H) (hf1 : f.ker Subgroup.center G) (hH : Group.IsNilpotent H) :

                    The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained in the center

                    theorem nilpotent_of_surjective {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] [h : Group.IsNilpotent G] (f : G →* G') (hf : Function.Surjective f) :

                    The range of a surjective homomorphism from a nilpotent group is nilpotent

                    The nilpotency class of the range of a surjective homomorphism from a nilpotent group is less or equal the nilpotency class of the domain

                    theorem nilpotent_of_mulEquiv {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] [_h : Group.IsNilpotent G] (f : G ≃* G') :

                    Nilpotency respects isomorphisms

                    instance nilpotent_quotient_of_nilpotent {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [_h : Group.IsNilpotent G] :

                    A quotient of a nilpotent group is nilpotent

                    Equations
                    • =

                    The nilpotency class of a quotient of G is less or equal the nilpotency class of G

                    Quotienting the center G reduces the nilpotency class by 1

                    The nilpotency class of a non-trivial group is one more than its quotient by the center

                    If the quotient by center G is nilpotent, then so is G.

                    theorem nilpotent_center_quotient_ind {P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop} (G : Type u_2) [Group G] [Group.IsNilpotent G] (hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G) (hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G Subgroup.center G)P G) :
                    P G

                    A custom induction principle for nilpotent groups. The base case is a trivial group (subsingleton G), and in the induction step, one can assume the hypothesis for the group quotiented by its center.

                    @[instance 100]

                    Abelian groups are nilpotent

                    Equations
                    • =

                    Abelian groups have nilpotency class at most one

                    Groups with nilpotency class at most one are abelian

                    Equations
                    Instances For
                      theorem lowerCentralSeries_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] (n : ) :
                      lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
                      instance isNilpotent_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂] :
                      Group.IsNilpotent (G₁ × G₂)

                      Products of nilpotent groups are nilpotent

                      Equations
                      • =
                      theorem nilpotencyClass_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂] :

                      The nilpotency class of a product is the max of the nilpotency classes of the factors

                      theorem lowerCentralSeries_pi_le {η : Type u_2} {Gs : ηType u_3} [(i : η) → Group (Gs i)] (n : ) :
                      lowerCentralSeries ((i : η) → Gs i) n Subgroup.pi Set.univ fun (i : η) => lowerCentralSeries (Gs i) n
                      theorem isNilpotent_pi_of_bounded_class {η : Type u_2} {Gs : ηType u_3} [(i : η) → Group (Gs i)] [∀ (i : η), Group.IsNilpotent (Gs i)] (n : ) (h : ∀ (i : η), Group.nilpotencyClass (Gs i) n) :
                      Group.IsNilpotent ((i : η) → Gs i)

                      products of nilpotent groups are nilpotent if their nilpotency class is bounded

                      theorem lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : ηType u_3} [(i : η) → Group (Gs i)] [Finite η] (n : ) :
                      lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun (i : η) => lowerCentralSeries (Gs i) n
                      instance isNilpotent_pi {η : Type u_2} {Gs : ηType u_3} [(i : η) → Group (Gs i)] [Finite η] [∀ (i : η), Group.IsNilpotent (Gs i)] :
                      Group.IsNilpotent ((i : η) → Gs i)

                      n-ary products of nilpotent groups are nilpotent

                      Equations
                      • =
                      theorem nilpotencyClass_pi {η : Type u_2} {Gs : ηType u_3} [(i : η) → Group (Gs i)] [Fintype η] [∀ (i : η), Group.IsNilpotent (Gs i)] :
                      Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun (i : η) => Group.nilpotencyClass (Gs i)

                      The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors

                      @[instance 100]

                      A nilpotent subgroup is solvable

                      Equations
                      • =
                      theorem IsPGroup.isNilpotent {G : Type u_1} [hG : Group G] [Finite G] {p : } [hp : Fact (Nat.Prime p)] (h : IsPGroup p G) :

                      A p-group is nilpotent

                      theorem isNilpotent_of_product_of_sylow_group {G : Type u_1} [hG : Group G] [Finite G] (e : ((p : { x : // x (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → P) ≃* G) :

                      If a finite group is the direct product of its Sylow groups, it is nilpotent

                      theorem isNilpotent_of_finite_tfae {G : Type u_1} [hG : Group G] [Finite G] :
                      [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom HH.Normal, ∀ (p : ), Fact (Nat.Prime p)∀ (P : Sylow p G), (↑P).Normal, Nonempty (((p : { x : // x (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → P) ≃* G)].TFAE

                      A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow groups.

                      @[deprecated isNilpotent_of_finite_tfae]
                      theorem isNilpotent_of_finite_tFAE {G : Type u_1} [hG : Group G] [Finite G] :
                      [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom HH.Normal, ∀ (p : ), Fact (Nat.Prime p)∀ (P : Sylow p G), (↑P).Normal, Nonempty (((p : { x : // x (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → P) ≃* G)].TFAE

                      Alias of isNilpotent_of_finite_tfae.


                      A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow groups.