Documentation

Mathlib.Algebra.Lie.Weights.Cartan

Weights and roots of Lie modules and Lie algebras with respect to Cartan subalgebras #

Given a Lie algebra L which is not necessarily nilpotent, it may be useful to study its representations by restricting them to a nilpotent subalgebra (e.g., a Cartan subalgebra). In the particular case when we view L as a module over itself via the adjoint action, the weight spaces of L restricted to a nilpotent subalgebra are known as root spaces.

Basic definitions and properties of the above ideas are provided in this file.

Main definitions #

@[reducible, inline]
noncomputable abbrev LieAlgebra.rootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (χ : HR) :
LieSubmodule R (H) L

Given a nilpotent Lie subalgebra H ⊆ L, the root space of a map χ : H → R is the weight space of L regarded as a module of H via the adjoint action.

Equations
Instances For
    @[simp]
    theorem LieAlgebra.rootSpace_comap_eq_weightSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (χ : HR) :
    theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R H] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : HR} {χ₂ : HR} {x : L} {m : M} (hx : x LieAlgebra.rootSpace H χ₁) (hm : m LieModule.weightSpace M χ₂) :
    x, m LieModule.weightSpace M (χ₁ + χ₂)
    theorem LieAlgebra.toEnd_pow_apply_mem {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R H] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : HR} {χ₂ : HR} {x : L} {m : M} (hx : x LieAlgebra.rootSpace H χ₁) (hm : m LieModule.weightSpace M χ₂) (n : ) :
    ((LieModule.toEnd R L M) x ^ n) m LieModule.weightSpace M (n χ₁ + χ₂)
    noncomputable def LieAlgebra.rootSpaceWeightSpaceProductAux (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ : HR} {χ₂ : HR} {χ₃ : HR} (hχ : χ₁ + χ₂ = χ₃) :
    (LieAlgebra.rootSpace H χ₁) →ₗ[R] (LieModule.weightSpace M χ₂) →ₗ[R] (LieModule.weightSpace M χ₃)

    Auxiliary definition for rootSpaceWeightSpaceProduct, which is close to the deterministic timeout limit.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def LieAlgebra.rootSpaceWeightSpaceProduct (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) :
      TensorProduct R (LieAlgebra.rootSpace H χ₁) (LieModule.weightSpace M χ₂) →ₗ⁅R,H (LieModule.weightSpace M χ₃)

      Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural R-bilinear product of root vectors and weight vectors, compatible with the actions of H.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem LieAlgebra.coe_rootSpaceWeightSpaceProduct_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) (x : (LieAlgebra.rootSpace H χ₁)) (m : (LieModule.weightSpace M χ₂)) :
        ((LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ ) (x ⊗ₜ[R] m)) = x, m
        theorem LieAlgebra.mapsTo_toEnd_weightSpace_add_of_mem_rootSpace (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (α : HR) (χ : HR) {x : L} (hx : x LieAlgebra.rootSpace H α) :
        noncomputable def LieAlgebra.rootSpaceProduct (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) :
        TensorProduct R (LieAlgebra.rootSpace H χ₁) (LieAlgebra.rootSpace H χ₂) →ₗ⁅R,H (LieAlgebra.rootSpace H χ₃)

        Given a nilpotent Lie subalgebra H ⊆ L together with χ₁ χ₂ : H → R, there is a natural R-bilinear product of root vectors, compatible with the actions of H.

        Equations
        Instances For
          theorem LieAlgebra.rootSpaceProduct_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) (x : (LieAlgebra.rootSpace H χ₁)) (y : (LieAlgebra.rootSpace H χ₂)) :
          ((LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ ) (x ⊗ₜ[R] y)) = x, y
          noncomputable def LieAlgebra.zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] :

          Given a nilpotent Lie subalgebra H ⊆ L, the root space of the zero map 0 : H → R is a Lie subalgebra of L.

          Equations
          Instances For
            @[simp]
            theorem LieAlgebra.coe_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] :
            theorem LieAlgebra.mem_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (x : L) :
            x LieAlgebra.zeroRootSubalgebra R L H ∀ (y : H), ∃ (k : ), ((LieModule.toEnd R (H) L) y ^ k) x = 0

            This enables the instance Zero (Weight R H L).

            Equations
            • =
            theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieAlgebra.IsNilpotent R H] (h : LieAlgebra.zeroRootSubalgebra R L H = H) :
            H.IsCartanSubalgebra

            If the zero root subalgebra of a nilpotent Lie subalgebra H is just H then H is a Cartan subalgebra.

            When L is Noetherian, it follows from Engel's theorem that the converse holds. See LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

            @[simp]
            theorem LieAlgebra.zeroRootSubalgebra_eq_of_is_cartan (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [IsNoetherian R L] :
            @[simp]
            theorem LieAlgebra.rootSpace_zero_eq (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [IsNoetherian R L] :
            LieAlgebra.rootSpace H 0 = H.toLieSubmodule
            noncomputable def LieAlgebra.corootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : HR) :
            LieIdeal R H

            Given a root α relative to a Cartan subalgebra H, this is the span of all products of an element of the α root space and an element of the root space. Informally it is often denoted ⁅H(α), H(-α)⁆.

            If the Killing form is non-degenerate and the coefficients are a perfect field, this space is one-dimensional. See LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton and LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'.

            Note that the name "coroot space" is not standard as this space does not seem to have a name in the informal literature.

            Equations
            Instances For
              theorem LieAlgebra.mem_corootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : HR) {x : H} :
              x LieAlgebra.corootSpace α x Submodule.span R {x : L | yLieAlgebra.rootSpace H α, zLieAlgebra.rootSpace H (-α), y, z = x}
              theorem LieAlgebra.mem_corootSpace' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieAlgebra.IsNilpotent R H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : HR) {x : H} :
              x LieAlgebra.corootSpace α x Submodule.span R {x : H | yLieAlgebra.rootSpace H α, zLieAlgebra.rootSpace H (-α), y, z = x}