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

• LieAlgebra.rootSpace
• LieAlgebra.corootSpace
• LieAlgebra.rootSpaceWeightSpaceProduct
• LieAlgebra.rootSpaceProduct
• LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan

@[reducible, inline]

abbrev LieAlgebra.rootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (χ : ↥H → R) : 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.

theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] : rootSpace ⊤ 0 = ⊤

@[simp]

theorem LieAlgebra.rootSpace_comap_eq_genWeightSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (χ : ↥H → R) : LieSubmodule.comap H.incl' (rootSpace H χ) = LieModule.genWeightSpace (↥H) χ

theorem LieAlgebra.lie_mem_genWeightSpace_of_mem_genWeightSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ χ₂ : ↥H → R} {x : L} {m : M} (hx : x ∈ rootSpace H χ₁) (hm : m ∈ LieModule.genWeightSpace M χ₂) : ⁅x, m⁆ ∈ LieModule.genWeightSpace 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} [LieRing.IsNilpotent ↥H] {M : Type u_3} [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ χ₂ : ↥H → R} {x : L} {m : M} (hx : x ∈ rootSpace H χ₁) (hm : m ∈ LieModule.genWeightSpace M χ₂) (n : ℕ) : ((LieModule.toEnd R L M) x ^ n) m ∈ LieModule.genWeightSpace M (n • χ₁ + χ₂)

def LieAlgebra.rootSpaceWeightSpaceProductAux (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {χ₁ χ₂ χ₃ : ↥H → R} (hχ : χ₁ + χ₂ = χ₃) : ↥(rootSpace H χ₁) →ₗ[R] ↥(LieModule.genWeightSpace M χ₂) →ₗ[R] ↥(LieModule.genWeightSpace M χ₃)

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

def LieAlgebra.rootSpaceWeightSpaceProduct (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃) : TensorProduct R ↥(rootSpace H χ₁) ↥(LieModule.genWeightSpace M χ₂) →ₗ⁅R,↥H⁆ ↥(LieModule.genWeightSpace 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.

@[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) [LieRing.IsNilpotent ↥H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃) (x : ↥(rootSpace H χ₁)) (m : ↥(LieModule.genWeightSpace M χ₂)) : ↑((rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] m)) = ⁅↑x, ↑m⁆

theorem LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (M : Type u_3) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (α χ : ↥H → R) {x : L} (hx : x ∈ rootSpace H α) : Set.MapsTo ⇑((LieModule.toEnd R L M) x) ↑(LieModule.genWeightSpace M χ) ↑(LieModule.genWeightSpace M (α + χ))

def LieAlgebra.rootSpaceProduct (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃) : TensorProduct R ↥(rootSpace H χ₁) ↥(rootSpace H χ₂) →ₗ⁅R,↥H⁆ ↥(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.

@[simp]

theorem LieAlgebra.rootSpaceProduct_def (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : rootSpaceProduct R L H = rootSpaceWeightSpaceProduct R L H L

theorem LieAlgebra.rootSpaceProduct_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃) (x : ↥(rootSpace H χ₁)) (y : ↥(rootSpace H χ₂)) : ↑((rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ) (x ⊗ₜ[R] y)) = ⁅↑x, ↑y⁆

def LieAlgebra.zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : LieSubalgebra R L

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

@[simp]

theorem LieAlgebra.coe_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : (zeroRootSubalgebra R L H).toSubmodule = ↑(rootSpace H 0)

theorem LieAlgebra.mem_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] (x : L) : x ∈ zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ (k : ℕ), ((LieModule.toEnd R (↥H) L) y ^ k) x = 0

theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : H.toLieSubmodule ≤ rootSpace H 0

instance LieAlgebra.instNontrivialSubtypeMemLieSubmoduleLieSubalgebraGenWeightSpaceOfNatForall (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] [Nontrivial ↥H] : Nontrivial ↥(LieModule.genWeightSpace L 0)

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

theorem LieAlgebra.le_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : H ≤ zeroRootSubalgebra R L H

@[simp]

theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] : (zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H

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) [LieRing.IsNilpotent ↥H] (h : 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] : zeroRootSubalgebra R L H = H

theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (H : LieSubalgebra R L) [LieRing.IsNilpotent ↥H] [IsNoetherian R L] : zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra

@[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] : rootSpace H 0 = H.toLieSubmodule

def LieAlgebra.corootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : ↥H → R) : 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.

theorem LieAlgebra.mem_corootSpace {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [LieRing.IsNilpotent ↥H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : ↥H → R) {x : ↥H} : x ∈ corootSpace α ↔ ↑x ∈ Submodule.span R {x : L | ∃ y ∈ rootSpace H α, ∃ z ∈ 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} [LieRing.IsNilpotent ↥H] [H.IsCartanSubalgebra] [IsNoetherian R L] (α : ↥H → R) {x : ↥H} : x ∈ corootSpace α ↔ x ∈ Submodule.span R {x : ↥H | ∃ y ∈ rootSpace H α, ∃ z ∈ rootSpace H (-α), ⁅y, z⁆ = ↑x}