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.

Equations
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) :
    @[simp]
    theorem LieSubmodule.lcs_sup {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} {N₂ : LieSubmodule R L M} {k : } :
    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.

    Equations
    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 LieSubmodule.lowerCentralSeries_map_eq_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] [LieModule R L M] (k : ) (N : LieSubmodule R L M) :
      theorem LieModule.eventually_iInf_lowerCentralSeries_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] [IsArtinian R M] :
      ∀ᶠ (l : ) in Filter.atTop, ⨅ (k : ), LieModule.lowerCentralSeries R L M k = LieModule.lowerCentralSeries R L M l
      theorem LieModule.iterate_toEnd_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) (m : M) (k : ) :
      theorem LieModule.iterate_toEnd_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 : ) :
      (((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y))^[k] m LieModule.lowerCentralSeries R L M (2 * 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] (k : ) {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] (f : M →ₗ⁅R,L M₂) :
      theorem LieModule.map_lowerCentralSeries_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] (k : ) {M₂ : Type w₁} [AddCommGroup M₂] [Module R M₂] [LieRingModule L M₂] [LieModule R L M₂] {f : M →ₗ⁅R,L M₂} (hf : Function.Surjective f) :
      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 LieModule.IsNilpotent.nilpotent {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [self : LieModule.IsNilpotent R L M] :
        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 N ∃ (k : ), LieSubmodule.lcs k N =
        @[instance 100]
        Equations
        • =
        theorem LieModule.exists_forall_pow_toEnd_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.toEnd R L M) x ^ k = 0
        theorem LieModule.isNilpotent_toEnd_of_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] [LieModule R L M] [LieModule.IsNilpotent R L M] (x : L) (y : L) :
        IsNilpotent ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y)
        @[simp]
        theorem LieModule.maxGenEigenSpace_toEnd_eq_top (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] [LieModule.IsNilpotent R L M] (x : L) :
        ((LieModule.toEnd R L M) x).maxGenEigenspace 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.

        theorem LieModule.isNilpotent_quotient_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) :
        theorem LieModule.iInf_lcs_le_of_isNilpotent_quot (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 : LieModule.IsNilpotent R L (M N)) :
        ⨅ (k : ), LieModule.lowerCentralSeries R L M k N
        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.

        Equations
        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, .

          Equations
          Instances For

            For a nilpotent Lie module M of a Lie algebra L, the first term in the lower central series of M contains a non-zero element on which L acts trivially unless the entire action is trivial.

            Taking M = L, this provides a useful characterisation of Abelian-ness for nilpotent Lie algebras.

            @[simp]
            theorem LieModule.coe_lcs_range_toEnd_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] (k : ) :
            @[simp]
            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.

            Equations
            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 : ) :
              LieSubmodule.ucs (k + 1) N = (LieSubmodule.ucs k N).normalizer
              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 : N₁.normalizer = 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 : N₁.normalizer = 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 : ) :
              GaloisConnection (fun (N : LieSubmodule R L M) => LieSubmodule.lcs k N) fun (N : LieSubmodule R L M) => LieSubmodule.ucs k N
              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 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) :
              @[instance 100]
              Equations
              • =
              @[reducible, inline]
              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.

              Equations
              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 (I) (I) k) (LieModule.lowerCentralSeries R L (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_toEnd_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.

                Equations
                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] :
                  I.lcs M 0 =
                  @[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 : ) :
                  I.lcs M (k + 1) = I, I.lcs 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 : ) :
                  (I.lcs M k) = (LieModule.lowerCentralSeries R (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 : K} (h : IsNilpotent ((LieAlgebra.ad R L) 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 : L} (h : IsNilpotent x) :
                  instance LieModule.instIsNilpotentTensor (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [CommRing A] [Algebra R A] [LieModule.IsNilpotent R L M] :
                  Equations
                  • =