The Kostant form of a Serre presentation

For an integer matrix CM, Mathlib's Matrix.ToLieAlgebra ℚ CM is the Lie algebra presented by the Serre generators and relations. This file equips its enveloping algebra with the subring generated by the divided powers of the simple raising and lowering generators and by the binomial coefficients in the Cartan generators:

Eᵢ⁽ⁿ⁾,  Fᵢ⁽ⁿ⁾,  and  (Hᵢ choose n).

This subring serves as the Serre-generator candidate integral form, providing the explicit presentation-level input for the Chevalley--Demazure construction. For an arbitrary integer matrix CM, it is defined by the simple generator families; identification with the canonical all-root Kostant ℤ-form is deferred until suitable root-datum hypotheses and comparison theorems are available.

The form spans the rational enveloping algebra: the Serre generators generate the presented Lie algebra, and the general spanning theorem for kostantForm applies. It is also stable under both symmetries visible in the presentation. A diagram automorphism permutes the three families of generators, while the Chevalley involution exchanges the E and F families with signs and negates the H family. The latter uses the integral identity expressing (-H choose n) in terms of the coefficients (H choose k).

Main definitions and results

• TauCeti.serreRootGenerator: the combined family of simple raising and lowering generators.
• TauCeti.lie_serreH_serreRootGenerator_inl and TauCeti.lie_serreH_serreRootGenerator_inr: the Cartan weights of the combined generators.
• TauCeti.serreKostantForm: the Serre-generator integral subring of the presentation.
• TauCeti.span_serreKostantForm_eq_top: the form spans the rational enveloping algebra.
• TauCeti.serreDiagramKostantEquiv: a diagram automorphism restricted to the integral form, with refl, trans, and symm laws.
• TauCeti.serreChevalleyKostantEquiv: the Chevalley involution restricted to the integral form, with self-inverse and commutation laws.

Roadmap

This supplies the concrete Kostant-form input to the Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. That construction starts from the Serre presentation of a pinned Cartan matrix; the generic form with arbitrary root and Cartan families is not yet the explicit integral object attached to that presentation. The resulting pinned group schemes are consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25--26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

noncomputable def TauCeti.serreRootGenerator {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : B ⊕ B → Matrix.ToLieAlgebra ℚ CM

The raising and lowering generators of a Serre presentation, combined into one family. The left summand indexes Eᵢ and the right summand indexes Fᵢ.

Equations

• TauCeti.serreRootGenerator CM = Sum.elim (TauCeti.serreE ℚ CM) (TauCeti.serreF ℚ CM)

@[simp]

theorem TauCeti.serreRootGenerator_inl {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i : B) : serreRootGenerator CM (Sum.inl i) = serreE ℚ CM i

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

@[simp]

theorem TauCeti.serreRootGenerator_inr {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i : B) : serreRootGenerator CM (Sum.inr i) = serreF ℚ CM i

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

theorem TauCeti.lie_serreH_serreRootGenerator_inl {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i j : B) : ⁅serreH ℚ CM j, serreRootGenerator CM (Sum.inl i)⁆ = ↑(CM j i) • serreRootGenerator CM (Sum.inl i)

A raising generator in the combined Serre family has the corresponding Cartan-matrix column as its Cartan weight.

theorem TauCeti.lie_serreH_serreRootGenerator_inr {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i j : B) : ⁅serreH ℚ CM j, serreRootGenerator CM (Sum.inr i)⁆ = ↑(-CM j i) • serreRootGenerator CM (Sum.inr i)

A lowering generator in the combined Serre family has the negative of the corresponding Cartan-matrix column as its Cartan weight.

noncomputable def TauCeti.serreKostantForm {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : Subring (UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CM))

The Kostant integral subring of the Serre presentation: the Serre-generator candidate subring generated by every divided power of a simple raising or lowering generator and every binomial coefficient in a Cartan generator.

Equations

• TauCeti.serreKostantForm CM = TauCeti.UniversalEnvelopingAlgebra.kostantForm (TauCeti.serreRootGenerator CM) (TauCeti.serreH ℚ CM)

theorem TauCeti.serreKostantForm_def {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : serreKostantForm CM = UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator CM) (serreH ℚ CM)

The Serre Kostant form is the general Kostant form for the combined E/F family and the Cartan family. This is its unfolding lemma; the definition itself remains sealed.

theorem TauCeti.dividedPower_serreE_mem {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i : B) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ CM i)) ∈ serreKostantForm CM

Every divided power of a raising generator belongs to the Serre Kostant form.

theorem TauCeti.dividedPower_serreF_mem {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i : B) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ CM i)) ∈ serreKostantForm CM

Every divided power of a lowering generator belongs to the Serre Kostant form.

theorem TauCeti.ringChoose_serreH_mem {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (i : B) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ CM i)) n ∈ serreKostantForm CM

Every binomial coefficient in a Cartan generator belongs to the Serre Kostant form.

@[simp]

theorem TauCeti.serreKostantForm_le_iff {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (T : Subring (UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CM))) : serreKostantForm CM ≤ T ↔ (∀ (i : B) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (serreE ℚ CM i)) ∈ T) ∧ (∀ (i : B) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (serreF ℚ CM i)) ∈ T) ∧ ∀ (i : B) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ CM i)) n ∈ T

The universal property of the Serre Kostant form, split into its three generator families.

theorem TauCeti.span_serreKostantForm_eq_top {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : Submodule.span ℚ ↑(serreKostantForm CM) = ⊤

The Serre Kostant form spans the rational universal enveloping algebra.

Diagram automorphisms

theorem TauCeti.kostantForm_serreDiagramAut_eq {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (UniversalEnvelopingAlgebra.kostantForm (fun (i : B ⊕ B) => (serreDiagramAut ℚ CM hσ) (serreRootGenerator CM i)) fun (i : B) => (serreDiagramAut ℚ CM hσ) (serreH ℚ CM i)) = serreKostantForm CM

The families obtained by applying a diagram automorphism generate the original Serre Kostant form. This is the preservation statement before packaging the restricted automorphism.

noncomputable def TauCeti.serreDiagramKostantEquiv {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : ↥(serreKostantForm CM) ≃+* ↥(serreKostantForm CM)

A diagram automorphism of the Serre presentation restricted to its Kostant integral form.

Equations

• TauCeti.serreDiagramKostantEquiv CM hσ = TauCeti.UniversalEnvelopingAlgebra.kostantFormAut (TauCeti.serreDiagramAut ℚ CM hσ) (TauCeti.serreRootGenerator CM) (TauCeti.serreH ℚ CM) ⋯

@[simp]

theorem TauCeti.coe_serreDiagramKostantEquiv_apply {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (x : ↥(serreKostantForm CM)) : ↑((serreDiagramKostantEquiv CM hσ) x) = (UniversalEnvelopingAlgebra.map ℚ (serreDiagramAut ℚ CM hσ).toLieHom) ↑x

The restricted diagram automorphism acts through the induced enveloping-algebra map.

theorem TauCeti.coe_serreDiagramKostantEquiv_symm_apply {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (x : ↥(serreKostantForm CM)) : ↑((serreDiagramKostantEquiv CM hσ).symm x) = (UniversalEnvelopingAlgebra.map ℚ (serreDiagramAut ℚ CM hσ).symm.toLieHom) ↑x

The inverse restricted diagram automorphism acts through the inverse Lie automorphism.

@[simp]

theorem TauCeti.serreDiagramKostantEquiv_refl {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : serreDiagramKostantEquiv CM ⋯ = RingEquiv.refl ↥(serreKostantForm CM)

The identity diagram automorphism restricts to the identity of the Kostant form.

@[simp]

theorem TauCeti.serreDiagramKostantEquiv_trans {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) {τ : Equiv.Perm B} (hτ : CM.submatrix ⇑τ ⇑τ = CM) : (serreDiagramKostantEquiv CM hσ).trans (serreDiagramKostantEquiv CM hτ) = serreDiagramKostantEquiv CM ⋯

Restricted diagram automorphisms compose along the composition of permutations.

@[simp]

theorem TauCeti.serreDiagramKostantEquiv_symm {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (serreDiagramKostantEquiv CM hσ).symm = serreDiagramKostantEquiv CM ⋯

The inverse of a restricted diagram automorphism is the restricted automorphism of the inverse permutation.

The Chevalley involution

theorem TauCeti.kostantForm_serreChevalleyInvolution_eq {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : (UniversalEnvelopingAlgebra.kostantForm (fun (i : B ⊕ B) => (serreChevalleyInvolution ℚ CM) (serreRootGenerator CM i)) fun (i : B) => (serreChevalleyInvolution ℚ CM) (serreH ℚ CM i)) = serreKostantForm CM

The families obtained by applying the Chevalley involution generate the original Serre Kostant form. The divided powers are unchanged up to sign, while the negated Cartan binomial coefficients are integral combinations of the original ones.

noncomputable def TauCeti.serreChevalleyKostantEquiv {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : ↥(serreKostantForm CM) ≃+* ↥(serreKostantForm CM)

The Chevalley involution of the Serre presentation restricted to its Kostant integral form.

Equations

• TauCeti.serreChevalleyKostantEquiv CM = TauCeti.UniversalEnvelopingAlgebra.kostantFormAut (TauCeti.serreChevalleyInvolution ℚ CM) (TauCeti.serreRootGenerator CM) (TauCeti.serreH ℚ CM) ⋯

@[simp]

theorem TauCeti.coe_serreChevalleyKostantEquiv_apply {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (x : ↥(serreKostantForm CM)) : ↑((serreChevalleyKostantEquiv CM) x) = (UniversalEnvelopingAlgebra.map ℚ (serreChevalleyInvolution ℚ CM).toLieHom) ↑x

The restricted Chevalley involution acts through the induced enveloping-algebra map.

theorem TauCeti.coe_serreChevalleyKostantEquiv_symm_apply {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (x : ↥(serreKostantForm CM)) : ↑((serreChevalleyKostantEquiv CM).symm x) = (UniversalEnvelopingAlgebra.map ℚ (serreChevalleyInvolution ℚ CM).symm.toLieHom) ↑x

The inverse restricted Chevalley involution acts through the inverse Lie automorphism.

@[simp]

theorem TauCeti.serreChevalleyKostantEquiv_serreChevalleyKostantEquiv {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) (x : ↥(serreKostantForm CM)) : (serreChevalleyKostantEquiv CM) ((serreChevalleyKostantEquiv CM) x) = x

Applying the restricted Chevalley involution twice returns the original element.

@[simp]

theorem TauCeti.serreChevalleyKostantEquiv_symm {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) : (serreChevalleyKostantEquiv CM).symm = serreChevalleyKostantEquiv CM

The restricted Chevalley involution is its own inverse.

theorem TauCeti.serreChevalleyKostantEquiv_comm_serreDiagramKostantEquiv {B : Type u_1} [DecidableEq B] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (serreChevalleyKostantEquiv CM).trans (serreDiagramKostantEquiv CM hσ) = (serreDiagramKostantEquiv CM hσ).trans (serreChevalleyKostantEquiv CM)

The restricted Chevalley involution commutes with every restricted diagram automorphism.