The admissible lattice of a minuscule weight table

The rational representation of a minuscule weight table acts on the rational coordinate space of its index type, and the Kostant form of its Serre generators carries the integral lattice of that space into itself.

Two properties of the table make that so. Each root generator is square-zero: the raising operator at a node carries a weight of coordinate -1 to its reflection, whose coordinate is 1, and kills every weight of coordinate 1. And each root generator has integer entries, so it carries integral coordinate vectors to integral coordinate vectors. The Cartan generators are diagonal with the table's weights on the diagonal, so every standard coordinate vector is a weight vector with an integral weight. Divided powers of a square-zero operator and binomial coefficients of an operator with integral eigenvalues are what the Kostant form is generated by.

Main declarations

• TauCeti.MinusculeWeightTable.rep: the rational representation extended to the universal enveloping algebra.

Main results

• TauCeti.MinusculeWeightTable.rep_serreRootGenerator_pow_two and isNilpotent_rep_serreRootGenerator: the represented root generators are square-zero.
• TauCeti.MinusculeWeightTable.rep_serreRootGenerator_inl_coordinateLatticeBasis_eq_sum and rep_serreRootGenerator_inr_coordinateLatticeBasis_eq_sum: their matrices in the coordinate lattice basis are the table's integral raising and lowering matrices.
• TauCeti.MinusculeWeightTable.isCartanWeightVector_single: each standard coordinate vector is a Cartan weight vector with its weight in the table.
• TauCeti.MinusculeWeightTable.isSl2Triple_rep_serreRootGenerator: the represented positive, negative, and Cartan generators at a node form an sl₂ triple.
• TauCeti.MinusculeWeightTable.rep_serreKostantForm_mem_lattice: the Serre Kostant form carries TauCeti.coordinateLattice into itself.
• TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_rep_ι_serreRootGenerator: the coordinate permutation TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv of a table symmetry intertwines the represented root generators along TauCeti.MinusculeWeightTable.Symmetry.rootPerm, and it preserves the coordinate lattice by moduleEquiv_mem_coordinateLattice_iff. These are the module-level inputs for descending a table symmetry to a Kostant toral-closure carrier.

References

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

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_mem_coordinateLattice_iff {B : Type u_1} {ι : Type u_2} {T : MinusculeWeightTable B ι} (S : T.Symmetry) [Finite ι] (v : ι → ℚ) : S.moduleEquiv v ∈ coordinateLattice ι ↔ v ∈ coordinateLattice ι

The coordinate permutation of a symmetry preserves the integral coordinate lattice, in both directions.

The enveloping-algebra representation

noncomputable def TauCeti.MinusculeWeightTable.rep {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ T.cartanMatrix) →ₐ[ℚ] Module.End ℚ (ι → ℚ)

The rational representation extended to the universal enveloping algebra.

Equations

• T.rep = (UniversalEnvelopingAlgebra.lift ℚ) ((↑(Matrix.toLinAlgEquiv (Pi.basisFun ℚ ι))).toLieHom.comp T.rationalSerreRepresentation)

theorem TauCeti.MinusculeWeightTable.rep_ι_apply {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (x : Matrix.ToLieAlgebra ℚ T.cartanMatrix) (v : ι → ℚ) : (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (T.rationalSerreRepresentation x).mulVec v

The enveloping-algebra representation acts on an included Lie element by matrix-vector multiplication.

theorem TauCeti.MinusculeWeightTable.rep_serreRootGenerator_pow_two {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (k : B ⊕ B) : T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix k)) ^ 2 = 0

Every represented positive or negative Serre root generator is square-zero.

theorem TauCeti.MinusculeWeightTable.isNilpotent_rep_serreRootGenerator {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (k : B ⊕ B) : IsNilpotent (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix k)))

Every represented positive or negative Serre root generator acts nilpotently.

theorem TauCeti.MinusculeWeightTable.nilpotencyClass_rep_serreRootGenerator_le_two {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (k : B ⊕ B) : nilpotencyClass (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix k))) ≤ 2

The nilpotency class of every represented positive or negative root generator is at most two.

theorem TauCeti.MinusculeWeightTable.rep_serreRootGenerator_inl_coordinateLatticeBasis_eq_sum {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) (s : ι) : (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix (Sum.inl i)))) ↑((coordinateLatticeBasis ι) s) = ∑ r : ι, T.raisingMatrix i r s • ↑((coordinateLatticeBasis ι) r)

A positive root generator has the table's integral raising matrix in the coordinate lattice basis.

theorem TauCeti.MinusculeWeightTable.rep_serreRootGenerator_inr_coordinateLatticeBasis_eq_sum {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) (s : ι) : (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix (Sum.inr i)))) ↑((coordinateLatticeBasis ι) s) = ∑ r : ι, T.loweringMatrix i r s • ↑((coordinateLatticeBasis ι) r)

A negative root generator has the table's integral lowering matrix in the coordinate lattice basis.

theorem TauCeti.MinusculeWeightTable.isSl2Triple_rep_serreRootGenerator {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (i : B) (hi : ∃ (a : ι), T.weight a i ≠ 0) : IsSl2Triple (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ T.cartanMatrix i))) (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix (Sum.inl i)))) (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix (Sum.inr i))))

The represented Cartan, positive, and negative Serre generators at a node form an sl₂ triple whenever the weight table contains a weight of nonzero coordinate at that node.

Stability of the coordinate lattice

theorem TauCeti.MinusculeWeightTable.rep_serreRootGenerator_mem_lattice {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (k : B ⊕ B) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix k))) v ∈ coordinateLattice ι

Every represented Serre root generator preserves the coordinate lattice.

theorem TauCeti.MinusculeWeightTable.isCartanWeightVector_single {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (a : ι) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ T.cartanMatrix) T.rep (T.weight a) (Pi.single a 1)

Each standard coordinate vector is a Cartan weight vector with its weight in the table.

theorem TauCeti.MinusculeWeightTable.isCartanWeightVector_coordinateLatticeBasis {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (a : ι) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ T.cartanMatrix) T.rep (T.weight a) ↑((coordinateLatticeBasis ι) a)

Every coordinate-lattice basis vector is a Cartan weight vector with its weight in the table.

theorem TauCeti.MinusculeWeightTable.rep_serreKostantForm_mem_lattice {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ T.cartanMatrix)} (hu : u ∈ serreKostantForm T.cartanMatrix) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (T.rep u) v ∈ coordinateLattice ι

The coordinate lattice is admissible for the Serre Kostant form of a minuscule weight table.

theorem TauCeti.MinusculeWeightTable.rep_kostantForm_mem_lattice {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (T : MinusculeWeightTable B ι) [DecidableEq B] (u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ T.cartanMatrix)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator T.cartanMatrix) (serreH ℚ T.cartanMatrix)) (v : ι → ℚ) (hv : v ∈ coordinateLattice ι) : (T.rep u) v ∈ coordinateLattice ι

The coordinate lattice is stable under the generic Kostant form built from the Serre generators. This is the form consumed by the carrier and base-change APIs.

Symmetries on the rational module

theorem TauCeti.MinusculeWeightTable.Symmetry.moduleEquiv_rep_ι_serreRootGenerator {B : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {T : MinusculeWeightTable B ι} [DecidableEq B] (S : T.Symmetry) (k : B ⊕ B) (v : ι → ℚ) : S.moduleEquiv ((T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix k))) v) = (T.rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator T.cartanMatrix (S.rootPerm k)))) (S.moduleEquiv v)

The coordinate permutation of a table symmetry intertwines the represented positive and negative simple-root generators along the induced root permutation.