Documentation

Mathlib.Algebra.Lie.Nilpotent

Nilpotent Lie algebras #

Like groups, Lie algebras admit a natural concept of nilpotency. More generally, any Lie module carries a natural concept of nilpotency. We define these here via the lower central series.

Main definitions #

Tags #

lie algebra, lower central series, nilpotent

def LieSubmodule.lcs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) :
LieSubmodule R L MLieSubmodule R L M

A generalisation of the lower central series. The zeroth term is a specified Lie submodule of a Lie module. In the case when we specify the top ideal of the Lie algebra, regarded as a Lie module over itself, we get the usual lower central series of a Lie algebra.

It can be more convenient to work with this generalisation when considering the lower central series of a Lie submodule, regarded as a Lie module in its own right, since it provides a type-theoretic expression of the fact that the terms of the Lie submodule's lower central series are also Lie submodules of the enclosing Lie module.

See also LieSubmodule.lowerCentralSeries_eq_lcs_comap and LieSubmodule.lowerCentralSeries_map_eq_lcs below, as well as LieSubmodule.ucs.

Instances For
    @[simp]
    theorem LieSubmodule.lcs_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :
    @[simp]
    theorem LieSubmodule.lcs_succ {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) (N : LieSubmodule R L M) :
    def LieModule.lowerCentralSeries (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) :

    The lower central series of Lie submodules of a Lie module.

    Instances For
      theorem LieSubmodule.lcs_le_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) (N : LieSubmodule R L M) :
      theorem LieModule.iterate_toEndomorphism_mem_lowerCentralSeries₂ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (y : L) (m : M) (k : ) :
      theorem LieModule.map_lowerCentralSeries_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (k : ) (f : M →ₗ⁅R,L M₂) :
      class LieModule.IsNilpotent (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

      A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of steps).

      Instances
        theorem LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
        LieModule.IsNilpotent R L { x // x N } k, LieSubmodule.lcs k N =
        theorem LieModule.exists_forall_pow_toEndomorphism_eq_zero (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [hM : LieModule.IsNilpotent R L M] :
        k, ∀ (x : L), ↑(LieModule.toEndomorphism R L M) x ^ k = 0
        theorem LieModule.nilpotentOfNilpotentQuotient (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N : LieSubmodule R L M} (h₁ : N LieModule.maxTrivSubmodule R L M) (h₂ : LieModule.IsNilpotent R L (M N)) :

        If the quotient of a Lie module M by a Lie submodule on which the Lie algebra acts trivially is nilpotent then M is nilpotent.

        This is essentially the Lie module equivalent of the fact that a central extension of nilpotent Lie algebras is nilpotent. See LieAlgebra.nilpotent_of_nilpotent_quotient below for the corresponding result for Lie algebras.

        noncomputable def LieModule.nilpotencyLength (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

        Given a nilpotent Lie module M with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥, this is the natural number k (the number of inclusions).

        For a non-nilpotent module, we use the junk value 0.

        Instances For
          noncomputable def LieModule.lowerCentralSeriesLast (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

          Given a non-trivial nilpotent Lie module M with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥, this is the k-1th term in the lower central series (the last non-trivial term).

          For a trivial or non-nilpotent module, this is the bottom submodule, .

          Instances For
            def LieSubmodule.ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ) :
            LieSubmodule R L MLieSubmodule R L M

            The upper (aka ascending) central series.

            See also LieSubmodule.lcs.

            Instances For
              @[simp]
              theorem LieSubmodule.ucs_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
              @[simp]
              theorem LieSubmodule.ucs_succ {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (k : ) :
              theorem LieSubmodule.ucs_add {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (k : ) (l : ) :
              theorem LieSubmodule.ucs_mono {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (k : ) (h : N₁ N₂) :
              theorem LieSubmodule.ucs_eq_self_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} (h : LieSubmodule.normalizer N₁ = N₁) (k : ) :
              LieSubmodule.ucs k N₁ = N₁
              theorem LieSubmodule.ucs_le_of_normalizer_eq_self {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} (h : LieSubmodule.normalizer N₁ = N₁) (k : ) :

              If a Lie module M contains a self-normalizing Lie submodule N, then all terms of the upper central series of M are contained in N.

              An important instance of this situation arises from a Cartan subalgebra H ⊆ L with the roles of L, M, N played by H, L, H, respectively.

              theorem LieSubmodule.lcs_add_le_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (l : ) (k : ) :
              theorem LieSubmodule.lcs_le_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {N₁ : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (k : ) :
              LieSubmodule.lcs k N₁ N₂ N₁ LieSubmodule.ucs k N₂
              theorem LieSubmodule.gc_lcs_ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ) :
              theorem LieSubmodule.ucs_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) (k : ) :
              theorem LieSubmodule.isNilpotent_iff_exists_self_le_ucs {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :
              LieModule.IsNilpotent R L { x // x N } k, N LieSubmodule.ucs k
              theorem Function.Surjective.lieModule_lcs_map_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : Function.Surjective f) (hg : Function.Surjective g) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) (k : ) :
              theorem Function.Surjective.lieModuleIsNilpotent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] {f : L →ₗ⁅R L₂} {g : M →ₗ[R] M₂} (hf : Function.Surjective f) (hg : Function.Surjective g) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) [LieModule.IsNilpotent R L M] :
              theorem Equiv.lieModule_isNilpotent_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {L₂ : Type u_1} {M₂ : Type u_2} [LieRing L₂] [LieAlgebra R L₂] [AddCommGroup M₂] [Module R M₂] [LieRingModule L₂ M₂] [LieModule R L₂ M₂] (f : L ≃ₗ⁅R L₂) (g : M ≃ₗ[R] M₂) (hfg : ∀ (x : L) (m : M), f x, g m = g x, m) :
              @[simp]
              theorem LieModule.isNilpotent_of_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] :
              @[inline, reducible]
              abbrev LieAlgebra.IsNilpotent (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

              We say a Lie algebra is nilpotent when it is nilpotent as a Lie module over itself via the adjoint representation.

              Instances For
                theorem LieAlgebra.nilpotent_ad_of_nilpotent_algebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsNilpotent R L] :
                k, ∀ (x : L), ↑(LieAlgebra.ad R L) x ^ k = 0
                theorem coe_lowerCentralSeries_ideal_quot_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (k : ) :

                Given an ideal I of a Lie algebra L, the lower central series of L ⧸ I is the same whether we regard L ⧸ I as an L module or an L ⧸ I module.

                TODO: This result obviously generalises but the generalisation requires the missing definition of morphisms between Lie modules over different Lie algebras.

                theorem LieModule.coe_lowerCentralSeries_ideal_le {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (k : ) :
                ↑(LieModule.lowerCentralSeries R { x // x I } { x // x I } k) ↑(LieModule.lowerCentralSeries R L { x // x I } k)

                Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular 2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with k = 1.

                A central extension of nilpotent Lie algebras is nilpotent.

                theorem LieHom.isNilpotent_range {R : Type u} {L : Type v} {L' : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra.IsNilpotent R L] (f : L →ₗ⁅R L') :
                @[simp]

                Note that this result is not quite a special case of LieModule.isNilpotent_range_toEndomorphism_iff which concerns nilpotency of the (ad R L).range-module L, whereas this result concerns nilpotency of the (ad R L).range-module (ad R L).range.

                def LieIdeal.lcs {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) :

                Given a Lie module M over a Lie algebra L together with an ideal I of L, this is the lower central series of M as an I-module. The advantage of using this definition instead of LieModule.lowerCentralSeries R I M is that its terms are Lie submodules of M as an L-module, rather than just as an I-module.

                See also LieIdeal.coe_lcs_eq.

                Instances For
                  @[simp]
                  theorem LieIdeal.lcs_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] :
                  @[simp]
                  theorem LieIdeal.lcs_succ {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) :
                  theorem LieIdeal.lcs_top {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] (k : ) :
                  theorem LieIdeal.coe_lcs_eq {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (k : ) :
                  ↑(LieIdeal.lcs I M k) = ↑(LieModule.lowerCentralSeries R { x // x I } M k)
                  theorem LieAlgebra.ad_nilpotent_of_nilpotent (R : Type u) {A : Type v} [CommRing R] [Ring A] [Algebra R A] {a : A} (h : IsNilpotent a) :
                  theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {R : Type u} [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) {x : { x // x K }} (h : IsNilpotent (↑(LieAlgebra.ad R L) x)) :
                  IsNilpotent (↑(LieAlgebra.ad R { x // x K }) x)
                  theorem LieAlgebra.isNilpotent_ad_of_isNilpotent {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] {L : LieSubalgebra R A} {x : { x // x L }} (h : IsNilpotent x) :
                  IsNilpotent (↑(LieAlgebra.ad R { x // x L }) x)