The Kostant form attached to a Lie algebra basis

A LieAlgebra.Basis supplies raising, lowering, and Cartan generators. This file combines the raising and lowering generators into one family and attaches the corresponding simple-generator Kostant form. The basis axiom span_ef immediately implies that this form spans the rational universal enveloping algebra.

The resulting subring is defined using only the simple raising and lowering generators. Its identification with the classical all-root Kostant form requires a separate comparison theorem.

Main definitions and results

• LieAlgebra.Basis.rootGenerator: the combined raising and lowering generators.
• LieAlgebra.Basis.rootGeneratorWeight: their weights against the Cartan generators.
• LieAlgebra.Basis.lie_h_rootGenerator: the corresponding Cartan-action relation.
• LieAlgebra.Basis.kostantForm: the associated simple-generator Kostant form.
• LieAlgebra.Basis.kostantForm_le_iff: its universal property.
• LieAlgebra.Basis.span_kostantForm_eq_top: the form spans the enveloping algebra.

def LieAlgebra.Basis.rootGenerator {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : ι ⊕ ι → L

The raising and lowering generators of a Lie algebra basis, combined into one family.

Equations

• b.rootGenerator = Sum.elim b.e b.f

@[simp]

theorem LieAlgebra.Basis.rootGenerator_inl {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i : ι) : b.rootGenerator (Sum.inl i) = b.e i

The combined root-generator family evaluates to the raising generator on the left summand.

@[simp]

theorem LieAlgebra.Basis.rootGenerator_inr {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i : ι) : b.rootGenerator (Sum.inr i) = b.f i

The combined root-generator family evaluates to the lowering generator on the right summand.

def LieAlgebra.Basis.rootGeneratorWeight {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : ι ⊕ ι → ι → ℤ

The integral weights of the combined raising and lowering generators against the Cartan generators.

Equations

• b.rootGeneratorWeight = Sum.elim (fun (i j : ι) => b.A i j) fun (i j : ι) => -b.A i j

@[simp]

theorem LieAlgebra.Basis.rootGeneratorWeight_inl {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i j : ι) : b.rootGeneratorWeight (Sum.inl i) j = b.A i j

A raising generator has the corresponding row of the Cartan matrix as its weight.

@[simp]

theorem LieAlgebra.Basis.rootGeneratorWeight_inr {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i j : ι) : b.rootGeneratorWeight (Sum.inr i) j = -b.A i j

A lowering generator has the negative of the corresponding row of the Cartan matrix as its weight.

theorem LieAlgebra.Basis.lie_h_rootGenerator {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i : ι ⊕ ι) (j : ι) : ⁅b.h j, b.rootGenerator i⁆ = ↑(b.rootGeneratorWeight i j) • b.rootGenerator i

A Cartan generator acts on a combined root generator through its integral weight.

theorem LieAlgebra.Basis.range_rootGenerator {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : Set.range b.rootGenerator = Set.range b.e ∪ Set.range b.f

The combined root generators have the union of the raising and lowering ranges.

theorem LieAlgebra.Basis.lieSpan_range_rootGenerator_union_range_h_eq_top {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : LieSubalgebra.lieSpan ℚ L (Set.range b.rootGenerator ∪ Set.range b.h) = ⊤

The root and Cartan generators of a Lie algebra basis generate the Lie algebra.

def LieAlgebra.Basis.kostantForm {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : Subring (UniversalEnvelopingAlgebra ℚ L)

The simple-generator Kostant form attached to a Lie algebra basis.

Equations

• b.kostantForm = TauCeti.UniversalEnvelopingAlgebra.kostantForm b.rootGenerator b.h

theorem LieAlgebra.Basis.kostantForm_def {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : b.kostantForm = TauCeti.UniversalEnvelopingAlgebra.kostantForm b.rootGenerator b.h

The basis Kostant form is the generic form for the combined root generators and Cartan generators.

theorem LieAlgebra.Basis.dividedPower_mem_kostantForm {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i : ι ⊕ ι) (n : ℕ) : TauCeti.Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (b.rootGenerator i)) ∈ b.kostantForm

Every divided power of a raising or lowering generator lies in the basis Kostant form.

theorem LieAlgebra.Basis.ringChoose_mem_kostantForm {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (i : ι) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (b.h i)) n ∈ b.kostantForm

Every binomial coefficient of a Cartan generator lies in the basis Kostant form.

@[simp]

theorem LieAlgebra.Basis.kostantForm_le_iff {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) (T : Subring (UniversalEnvelopingAlgebra ℚ L)) : b.kostantForm ≤ T ↔ (∀ (i : ι ⊕ ι) (n : ℕ), TauCeti.Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (b.rootGenerator i)) ∈ T) ∧ ∀ (i : ι) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (b.h i)) n ∈ T

The universal property of the basis Kostant form, split into its root and Cartan families.

theorem LieAlgebra.Basis.span_kostantForm_eq_top {ι : Type u_1} {L : Type u_2} [Finite ι] [LieRing L] [LieAlgebra ℚ L] {H : LieSubalgebra ℚ L} (b : Basis ι H) : Submodule.span ℚ ↑b.kostantForm = ⊤

The basis Kostant form spans the rational universal enveloping algebra.