# 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 #

• LieModule.IsWeight
• LieAlgebra.rootSpace
• LieAlgebra.IsRoot
• LieAlgebra.rootSpaceWeightSpaceProduct
• LieAlgebra.rootSpaceProduct
• LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan
noncomputable def LieModule.IsWeight {R : Type u_1} {L : Type u_2} [] [] [] (H : ) [] (M : Type u_3) [] [Module R M] [] [LieModule R L M] (χ : ) :

Given a Lie module M of a Lie algebra L, a weight of M with respect to a nilpotent subalgebra H ⊆ L is a Lie character whose corresponding weight space is non-empty.

Equations
• = ()
Instances For
theorem LieModule.isWeight_zero_of_nilpotent {R : Type u_1} {L : Type u_2} [] [] [] (M : Type u_3) [] [Module R M] [] [LieModule R L M] [] [] [] :

For a non-trivial nilpotent Lie module over a nilpotent Lie algebra, the zero character is a weight with respect to the ⊤ Lie subalgebra.

@[inline, reducible]
noncomputable abbrev LieAlgebra.rootSpace {R : Type u_1} {L : Type u_2} [] [] [] (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
theorem LieAlgebra.zero_rootSpace_eq_top_of_nilpotent {R : Type u_1} {L : Type u_2} [] [] [] [] :
@[inline, reducible]
noncomputable abbrev LieAlgebra.IsRoot {R : Type u_1} {L : Type u_2} [] [] [] (H : ) [] (χ : ) :

A root of a Lie algebra L with respect to a nilpotent subalgebra H ⊆ L is a weight 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} [] [] [] (H : ) [] (χ : HR) :
theorem LieAlgebra.lie_mem_weightSpace_of_mem_weightSpace {R : Type u_1} {L : Type u_2} [] [] [] {H : } [] {M : Type u_3} [] [Module R M] [] [LieModule R L M] {χ₁ : HR} {χ₂ : HR} {x : L} {m : M} (hx : x ) (hm : m ) :
x, m LieModule.weightSpace M (χ₁ + χ₂)
noncomputable def LieAlgebra.rootSpaceWeightSpaceProductAux (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] (M : Type u_3) [] [Module R M] [] [LieModule R L M] {χ₁ : HR} {χ₂ : HR} {χ₃ : HR} (hχ : χ₁ + χ₂ = χ₃) :
() →ₗ[R] () →ₗ[R] ()

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) [] [] [] (H : ) [] (M : Type u_3) [] [Module R M] [] [LieModule R L M] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) :
TensorProduct R () () →ₗ⁅R,H ()

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) [] [] [] (H : ) [] (M : Type u_3) [] [Module R M] [] [LieModule R L M] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) (x : ()) (m : ()) :
((LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ ) (x ⊗ₜ[R] m)) = x, m
noncomputable def LieAlgebra.rootSpaceProduct (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) :
TensorProduct R () () →ₗ⁅R,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
@[simp]
theorem LieAlgebra.rootSpaceProduct_def (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :
theorem LieAlgebra.rootSpaceProduct_tmul (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] (χ₁ : HR) (χ₂ : HR) (χ₃ : HR) (hχ : χ₁ + χ₂ = χ₃) (x : ()) (y : ()) :
((LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ ) (x ⊗ₜ[R] y)) = x, y
noncomputable def LieAlgebra.zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [] [] [] (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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem LieAlgebra.coe_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :
().toSubmodule = ()
theorem LieAlgebra.mem_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] (x : L) :
∀ (y : H), ∃ (k : ), ((LieModule.toEndomorphism R (H) L) y ^ k) x = 0
theorem LieAlgebra.toLieSubmodule_le_rootSpace_zero (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :
theorem LieAlgebra.le_zeroRootSubalgebra (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :
@[simp]
theorem LieAlgebra.zeroRootSubalgebra_normalizer_eq_self (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :
theorem LieAlgebra.is_cartan_of_zeroRootSubalgebra_eq (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] (h : ) :

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) [] [] [] (H : ) [] :
theorem LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] [] :
@[simp]
theorem LieAlgebra.rootSpace_zero_eq (R : Type u_1) (L : Type u_2) [] [] [] (H : ) [] :