A simple-generator Kostant form of the pinned split Lie algebra of a Dynkin type

TauCeti.DynkinType.lieAlgebra is the split Lie algebra of a valid Dynkin type, realized by Geck's construction as an explicit Lie subalgebra of GeckIndex-indexed rational matrices, with Chevalley generators TauCeti.DynkinType.lieBasis numbered by Bourbaki node. This file attaches the simple-generator Kostant subring of its universal enveloping algebra to that pinned data, and records the defining matrix representation through which the subring acts.

The form is generated by divided powers of the simple raising and lowering generators and by binomial coefficients in the simple Cartan generators. Identifying it with the canonical all-root Kostant ℤ-form is a separate theorem and is not claimed here.

Four things are needed before the divided powers of the Kostant form can be exponentiated into root subgroups, and all four are supplied here.

The form itself. TauCeti.DynkinType.kostantForm is LieAlgebra.Basis.kostantForm applied to the pinned Lie algebra basis. Because the raising and lowering generators already generate the whole Lie algebra, TauCeti.DynkinType.span_kostantForm_eq_top says the form spans U(L) over ℚ without further hypotheses.

A representation to act in. Geck's Lie algebra consists of actual matrices, so its defining action on GeckIndex → ℚ is available with no representation theory at all: TauCeti.DynkinType.geckRepresentation is the algebra map extending it, and it is faithful on the Lie algebra by TauCeti.DynkinType.geckRepresentation_ι_injective.

Nilpotency and weights. TauCeti.DynkinType.isNilpotent_geckRepresentation_rootGenerator says every numbered root generator acts nilpotently, which makes its divided-power exponential a finite sum; and TauCeti.DynkinType.isCartanWeightVector_geckRepresentation_single says each standard coordinate vector is a joint eigenvector of the Cartan generators, with the integer eigenvalue TauCeti.DynkinType.geckWeight. In the Bourbaki numbering that weight is zero on the pinned base support coordinates and is the Cartan pairing ⟨α_k, α_i^∨⟩ on the coordinate of the root α_k.

A ℤ-module to act on. TauCeti.DynkinType.geckOrbit is the ℤ-span of the images of the standard coordinate vectors under the whole Kostant form. It is stable under the form by construction and spans the Geck module over ℚ, so it discharges the stability hypothesis that every Kostant root-subgroup consumer has so far carried.

The orbit is in fact finitely generated over ℤ: it coincides with the coordinate lattice of TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/GeckLattice/Basic.lean, because that lattice is preserved by the whole form, so it is a full lattice in the sense of Humphreys §27. Nor is the pinned Lie algebra asserted to be semisimple, which TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/LieAlgebra/Basic.lean already records as not claimed. This file is the numbered input those later steps consume.

Main definitions

• TauCeti.DynkinType.kostantForm: the pinned simple-generator Kostant form.
• TauCeti.DynkinType.geckRepresentation: the defining matrix representation of U(L).
• TauCeti.DynkinType.geckWeight: the integral weight of a Geck coordinate.
• TauCeti.DynkinType.rootGeneratorWeight: the integral root of a numbered raising or lowering generator.
• TauCeti.DynkinType.geckOrbit: the integral orbit of the standard coordinate vectors.

Main results

• TauCeti.DynkinType.span_kostantForm_eq_top: the Kostant form spans the enveloping algebra over ℚ.
• TauCeti.DynkinType.geckRepresentation_ι_injective: the defining representation is faithful on the Lie algebra.
• TauCeti.DynkinType.isNilpotent_geckRepresentation_rootGenerator: each numbered root generator acts nilpotently.
• TauCeti.DynkinType.isCartanWeightVector_geckRepresentation_single: the standard coordinate vectors are Cartan weight vectors with integer weights.
• TauCeti.DynkinType.lie_lieBasis_h_rootGenerator: the Cartan action on each numbered root generator is given by its integral root.
• TauCeti.DynkinType.rootGeneratorWeight_inl_eq_root_simpleIndex and TauCeti.DynkinType.rootGeneratorWeight_inr_eq_neg_root_simpleIndex: that integral root is the simple root of TauCeti.DynkinType.simplyConnectedRootDatum with the same Bourbaki node number, respectively its negative.
• TauCeti.DynkinType.geckRepresentation_mem_geckOrbit and TauCeti.DynkinType.span_geckOrbit_eq_top: the integral orbit is stable under the Kostant form and spans the Geck module over ℚ.
• In …/GeckLattice/Basic.lean, TauCeti.DynkinType.geckOrbit_eq_geckCoordinateLattice and TauCeti.DynkinType.instIsLatticeGeckOrbit: the orbit equals the coordinate lattice and is a full, finitely generated lattice.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.
• M. Geck, On the construction of semisimple Lie algebras and Chevalley groups, Proc. Amer. Math. Soc. 145 (2017), 3233--3247.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for the split reductive group scheme over ℤ to be constructed "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra". The concrete Geck matrix carrier is used here because its defining faithful representation supplies the module on which the root subgroups will act. The separate TauCeti.serreKostantForm is the presentation-level simple-generator form used to study the symmetries before passing to this concrete carrier. No comparison between those two forms is yet proved; such a comparison is required before presentation-level results are transported here, and the two forms are not intended to define independent group schemes. The consumer of the assembled pinned construction is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

The simple-generator Kostant form

noncomputable def TauCeti.DynkinType.kostantForm (t : DynkinType) (ht : t.Valid) : Subring (UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht))

The simple-generator Kostant form of the pinned split Lie algebra: the subring of U(L) generated by divided powers of the numbered simple raising and lowering generators and by binomial coefficients of the numbered Cartan generators.

Identification with the canonical all-root Kostant ℤ-form is not asserted.

Equations

• t.kostantForm ht = (t.lieBasis ht).kostantForm

theorem TauCeti.DynkinType.kostantForm_def (t : DynkinType) (ht : t.Valid) : t.kostantForm ht = (t.lieBasis ht).kostantForm

The pinned form is the basis Kostant form for the pinned Lie algebra basis.

theorem TauCeti.DynkinType.dividedPower_mem_kostantForm (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i)) ∈ t.kostantForm ht

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

theorem TauCeti.DynkinType.ringChoose_mem_kostantForm (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).h i)) n ∈ t.kostantForm ht

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

@[simp]

theorem TauCeti.DynkinType.kostantForm_le_iff (t : DynkinType) (ht : t.Valid) (T : Subring (UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht))) : t.kostantForm ht ≤ T ↔ (∀ (i : Fin t.rank ⊕ Fin t.rank) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i)) ∈ T) ∧ ∀ (i : Fin t.rank) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).h i)) n ∈ T

The universal property of the pinned simple-generator Kostant form.

theorem TauCeti.DynkinType.span_kostantForm_eq_top (t : DynkinType) (ht : t.Valid) : Submodule.span ℚ ↑(t.kostantForm ht) = ⊤

The Kostant form spans the enveloping algebra. Its ℚ-span is the whole universal enveloping algebra of the pinned split Lie algebra.

This is the spanning half of the expected integral-form statement; freeness over ℤ and comparison with the classical all-root form require additional results.

The roots of the numbered generators

noncomputable def TauCeti.DynkinType.rootGeneratorWeight (t : DynkinType) (ht : t.Valid) : Fin t.rank ⊕ Fin t.rank → Fin t.rank → ℤ

The root of a numbered raising or lowering generator, as an integral character of the pinned Cartan generators: the corresponding Bourbaki Cartan-matrix row for a raising generator, and its negative for a lowering generator.

Equations

• t.rootGeneratorWeight ht = (t.lieBasis ht).rootGeneratorWeight

@[simp]

theorem TauCeti.DynkinType.rootGeneratorWeight_inl (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) : t.rootGeneratorWeight ht (Sum.inl i) j = t.cartanMatrix i j

@[simp]

theorem TauCeti.DynkinType.rootGeneratorWeight_inr (t : DynkinType) (ht : t.Valid) (i j : Fin t.rank) : t.rootGeneratorWeight ht (Sum.inr i) j = -t.cartanMatrix i j

The two identifications below read those Cartan-matrix rows as the simple roots of TauCeti.DynkinType.simplyConnectedRootDatum. They are deliberately not simp lemmas: both sides are already simp-normal, since rootGeneratorWeight_inl and root_simpleIndex rewrite them to the same row, and orienting the identification either way would undo one of them.

theorem TauCeti.DynkinType.rootGeneratorWeight_inl_eq_root_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : t.rootGeneratorWeight ht (Sum.inl i) = (t.simplyConnectedRootDatum ht).root (t.simpleIndex ht i)

The root of the i-th numbered raising generator is the i-th pinned simple root. The integral character of the pinned Cartan generators through which they act on that generator is the simple root of t.simplyConnectedRootDatum ht with the same Bourbaki node number.

theorem TauCeti.DynkinType.rootGeneratorWeight_inr_eq_neg_root_simpleIndex (t : DynkinType) (ht : t.Valid) (i : Fin t.rank) : t.rootGeneratorWeight ht (Sum.inr i) = -(t.simplyConnectedRootDatum ht).root (t.simpleIndex ht i)

The root of the i-th numbered lowering generator is the negative of the i-th pinned simple root.

theorem TauCeti.DynkinType.lie_lieBasis_h_rootGenerator (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) (j : Fin t.rank) : ⁅(t.lieBasis ht).h j, (t.lieBasis ht).rootGenerator i⁆ = ↑(t.rootGeneratorWeight ht i j) • (t.lieBasis ht).rootGenerator i

The pinned Cartan generators act on a numbered root generator through its root.

The defining representation

noncomputable def TauCeti.DynkinType.geckRepresentation (t : DynkinType) (ht : t.Valid) : UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht) →ₐ[ℚ] Module.End ℚ (t.GeckIndex ht → ℚ)

The defining representation of the pinned split Lie algebra, extended to its universal enveloping algebra. Geck's Lie algebra is a Lie subalgebra of matrices, so the representation is the matrix action on coordinate vectors; no existence theorem for a faithful representation is invoked.

Equations

• t.geckRepresentation ht = (t.lieAlgebra ht).matrixRepresentation

theorem TauCeti.DynkinType.geckRepresentation_def (t : DynkinType) (ht : t.Valid) : t.geckRepresentation ht = (t.lieAlgebra ht).matrixRepresentation

The Geck representation is the defining representation of its matrix Lie subalgebra.

theorem TauCeti.DynkinType.geckRepresentation_ι (t : DynkinType) (ht : t.Valid) (x : ↥(t.lieAlgebra ht)) : (t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) x) = Matrix.toLinAlgEquiv' ↑x

A Lie generator acts through its underlying matrix.

theorem TauCeti.DynkinType.geckRepresentation_ι_apply (t : DynkinType) (ht : t.Valid) (x : ↥(t.lieAlgebra ht)) (v : t.GeckIndex ht → ℚ) : ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (↑x).mulVec v

The pointwise form of TauCeti.DynkinType.geckRepresentation_ι: a Lie generator acts by multiplying a coordinate vector by its underlying matrix.

theorem TauCeti.DynkinType.geckRepresentation_ι_injective (t : DynkinType) (ht : t.Valid) : Function.Injective fun (x : ↥(t.lieAlgebra ht)) => (t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) x)

The defining representation is faithful on the Lie algebra. Distinct elements of the pinned Lie algebra act differently, so the Lie algebra embeds in the endomorphisms of the Geck module.

Nilpotency of the numbered generators

theorem TauCeti.DynkinType.isNilpotent_geckRepresentation_rootGenerator (t : DynkinType) (ht : t.Valid) (i : Fin t.rank ⊕ Fin t.rank) : IsNilpotent ((t.geckRepresentation ht) ((UniversalEnvelopingAlgebra.ι ℚ) ((t.lieBasis ht).rootGenerator i)))

Every numbered root generator acts nilpotently. This is what makes the divided-power exponential of a root vector a finite sum, hence an automorphism of any stable lattice over any value ring.

The weights of the Geck module

noncomputable def TauCeti.DynkinType.geckWeight (t : DynkinType) (ht : t.Valid) : t.GeckIndex ht → Fin t.rank → ℤ

The integral weight of a Geck coordinate, in the Bourbaki numbering: zero on the coordinates indexed by the pinned base support, and the Cartan pairing ⟨α_k, α_i^∨⟩ on the coordinate indexed by the root α_k.

The matrix of each of Geck's Cartan generators is diagonal (RootPairing.GeckConstruction.h_eq_diagonal) with these entries, so this is the weight function of the standard coordinate vectors, and it takes values in ℤ rather than merely in ℚ.

Equations

• t.geckWeight ht = Sum.elim 0 fun (k : Fin t.numRoots) (i : Fin t.rank) => (t.rationalRootSystem ht).pairingIn ℤ k ↑((t.simpleSupportEquiv ht) i)

@[simp]

theorem TauCeti.DynkinType.geckWeight_inl (t : DynkinType) (ht : t.Valid) (x : ↥(t.rationalBase ht).support) (i : Fin t.rank) : t.geckWeight ht (Sum.inl x) i = 0

@[simp]

theorem TauCeti.DynkinType.geckWeight_inr (t : DynkinType) (ht : t.Valid) (k : Fin t.numRoots) (i : Fin t.rank) : t.geckWeight ht (Sum.inr k) i = (t.rationalRootSystem ht).pairingIn ℤ k ↑((t.simpleSupportEquiv ht) i)

theorem TauCeti.DynkinType.isCartanWeightVector_geckRepresentation_single (t : DynkinType) (ht : t.Valid) (x : t.GeckIndex ht) : UniversalEnvelopingAlgebra.IsCartanWeightVector (t.lieBasis ht).h (t.geckRepresentation ht) (t.geckWeight ht x) (Pi.single x 1)

The standard coordinate vectors are joint eigenvectors of the Cartan generators, with the integer eigenvalues recorded by TauCeti.DynkinType.geckWeight.

This is the pinned split torus in embryo: the diagonal action of the Cartan subalgebra on the standard lattice of the Geck module is by integral characters, numbered by Bourbaki node.

The integral orbit of the standard coordinates

noncomputable def TauCeti.DynkinType.geckOrbit (t : DynkinType) (ht : t.Valid) : Submodule ℤ (t.GeckIndex ht → ℚ)

The integral orbit of the standard coordinates of the Geck module: the ℤ-span of the images of the standard coordinate vectors under the simple-generator Kostant form.

Every downstream consumer of a Kostant root subgroup takes a ℤ-submodule preserved by the whole integral form as a hypothesis. This one is preserved by construction, by TauCeti.DynkinType.geckRepresentation_mem_geckOrbit, and it is full by TauCeti.DynkinType.span_geckOrbit_eq_top. Its finite generation over ℤ is proved in TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/GeckLattice/Basic.lean, where the orbit is identified with the coordinate lattice.

Equations

• t.geckOrbit ht = TauCeti.UniversalEnvelopingAlgebra.orbitOfRep (t.kostantForm ht) (t.geckRepresentation ht) (Set.range fun (x : t.GeckIndex ht) => Pi.single x 1)

theorem TauCeti.DynkinType.geckOrbit_def (t : DynkinType) (ht : t.Valid) : t.geckOrbit ht = UniversalEnvelopingAlgebra.orbitOfRep (t.kostantForm ht) (t.geckRepresentation ht) (Set.range fun (x : t.GeckIndex ht) => Pi.single x 1)

The pinned integral orbit is the generic represented orbit of the standard coordinate vectors.

theorem TauCeti.DynkinType.geckRepresentation_single_mem_geckOrbit (t : DynkinType) (ht : t.Valid) {u : UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht)} (hu : u ∈ t.kostantForm ht) (x : t.GeckIndex ht) : ((t.geckRepresentation ht) u) (Pi.single x 1) ∈ t.geckOrbit ht

A Kostant-form translate of a standard coordinate vector lies in the integral orbit.

theorem TauCeti.DynkinType.single_mem_geckOrbit (t : DynkinType) (ht : t.Valid) (x : t.GeckIndex ht) : Pi.single x 1 ∈ t.geckOrbit ht

Every standard coordinate vector lies in the integral orbit, the identity of the enveloping algebra being one of the elements the orbit is taken over.

theorem TauCeti.DynkinType.geckRepresentation_mem_geckOrbit (t : DynkinType) (ht : t.Valid) {u : UniversalEnvelopingAlgebra ℚ ↥(t.lieAlgebra ht)} (hu : u ∈ t.kostantForm ht) {v : t.GeckIndex ht → ℚ} (hv : v ∈ t.geckOrbit ht) : ((t.geckRepresentation ht) u) v ∈ t.geckOrbit ht

The integral orbit is stable under the Kostant form. This is the hypothesis a Kostant root subgroup needs of the stable ℤ-submodule it acts on, and it holds here because the orbit is taken over a subring: acting again multiplies inside the form.

theorem TauCeti.DynkinType.geckOrbit_le_iff (t : DynkinType) (ht : t.Valid) (N : Submodule ℤ (t.GeckIndex ht → ℚ)) : t.geckOrbit ht ≤ N ↔ ∀ u ∈ t.kostantForm ht, ∀ (x : t.GeckIndex ht), ((t.geckRepresentation ht) u) (Pi.single x 1) ∈ N

The elimination principle for the pinned integral orbit.

theorem TauCeti.DynkinType.span_geckOrbit_eq_top (t : DynkinType) (ht : t.Valid) : Submodule.span ℚ ↑(t.geckOrbit ht) = ⊤

The integral orbit is full. It spans the Geck module over ℚ, because it already contains the standard coordinate vectors.