The admissible lattice in the tripled type-D4 representation

This file reads the rational extension of the integral 24-dimensional tripled representation of the type-D₄ Serre presentation, and the admissibility of its coordinate ℤ-lattice for the Serre Kostant form, off the minuscule weight table TauCeti.D4Tripled.weightTable, where they are proved for an arbitrary table.

Thus the tripled coordinate lattice is an admissible lattice for the explicit Serre-generator Kostant form. Its weights already span the full type-D₄ character lattice by TauCeti.DynkinType.span_range_d4TripledWeight_eq_top. Together, these are the lattice inputs needed to construct the tripled type-D₄ Chevalley carrier.

Main declarations

• TauCeti.D4Tripled.rep: the rational representation of the universal enveloping algebra.
• TauCeti.D4Tripled.isSl2Triple_rep_serreRootGenerator: the represented generators at every node form an sl₂ triple.
• TauCeti.D4Tripled.rep_serreRootGenerator_inl_latticeBasis_eq_sum and TauCeti.D4Tripled.rep_serreRootGenerator_inr_latticeBasis_eq_sum: the represented root generators act on the lattice basis by the raising and lowering matrices.
• TauCeti.D4Tripled.lattice: the coordinate ℤ-lattice in the rational module.
• TauCeti.D4Tripled.rep_kostantForm_mem_lattice: the generic Kostant form preserves the lattice.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• The rational representation and admissibility results specialize TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.MinusculeWeightTable.

The enveloping-algebra representation

noncomputable def TauCeti.D4Tripled.rep : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ weightTable.cartanMatrix) →ₐ[ℚ] Module.End ℚ (Fin 24 → ℚ)

The rational tripled representation extended to the universal enveloping algebra.

Equations

• TauCeti.D4Tripled.rep = TauCeti.D4Tripled.weightTable.rep

theorem TauCeti.D4Tripled.rep_def : rep = weightTable.rep

The rational tripled representation is the representation of the tripled weight table.

theorem TauCeti.D4Tripled.isNilpotent_rep_serreRootGenerator (k : Fin 4 ⊕ Fin 4) : IsNilpotent (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator weightTable.cartanMatrix k)))

Every represented positive or negative Serre root generator acts nilpotently.

theorem TauCeti.D4Tripled.isSl2Triple_rep_serreRootGenerator (i : Fin 4) : IsSl2Triple (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ weightTable.cartanMatrix i))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator weightTable.cartanMatrix (Sum.inl i)))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator weightTable.cartanMatrix (Sum.inr i))))

The represented Cartan, positive, and negative Serre generators at every node form an sl₂ triple: each simple-coroot coordinate takes the value -1 on some tripled weight.

The admissible coordinate lattice

def TauCeti.D4Tripled.lattice : Submodule ℤ (Fin 24 → ℚ)

The coordinate ℤ-lattice in the rational tripled module.

Equations

• TauCeti.D4Tripled.lattice = TauCeti.coordinateLattice (Fin 24)

theorem TauCeti.D4Tripled.lattice_def : lattice = coordinateLattice (Fin 24)

The tripled lattice is the standard coordinate lattice.

noncomputable def TauCeti.D4Tripled.latticeBasis : Module.Basis (Fin 24) ℤ ↥lattice

The coordinate basis of the tripled lattice.

Equations

• TauCeti.D4Tripled.latticeBasis = TauCeti.coordinateLatticeBasis (Fin 24)

@[simp]

theorem TauCeti.D4Tripled.coe_latticeBasis (a : Fin 24) : ↑(latticeBasis a) = Pi.single a 1

Coercing a tripled lattice-basis vector to the rational module gives the corresponding coordinate vector.

theorem TauCeti.D4Tripled.isCartanWeightVector_latticeBasis (a : Fin 24) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ weightTable.cartanMatrix) rep (DynkinType.d4TripledWeight a) ↑(latticeBasis a)

Every tripled lattice-basis vector is a Cartan weight vector with its tripled weight.

theorem TauCeti.D4Tripled.rep_serreRootGenerator_inl_latticeBasis_eq_sum (i : Fin 4) (s : Fin 24) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator weightTable.cartanMatrix (Sum.inl i)))) ↑(latticeBasis s) = ∑ r : Fin 24, raisingMatrix i r s • ↑(latticeBasis r)

A represented positive Serre root generator acts on the tripled lattice basis by the raising matrix.

theorem TauCeti.D4Tripled.rep_serreRootGenerator_inr_latticeBasis_eq_sum (i : Fin 4) (s : Fin 24) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator weightTable.cartanMatrix (Sum.inr i)))) ↑(latticeBasis s) = ∑ r : Fin 24, loweringMatrix i r s • ↑(latticeBasis r)

A represented negative Serre root generator acts on the tripled lattice basis by the lowering matrix.

theorem TauCeti.D4Tripled.rep_kostantForm_mem_lattice (u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ weightTable.cartanMatrix)) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix)) (v : Fin 24 → ℚ) (hv : v ∈ lattice) : (rep u) v ∈ lattice

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