Documentation

TauCeti.Algebra.Lie.F4.ShortRoot.AdmissibleLattice

The admissible lattice of the short-root representation of type F4 #

This file extends the integral twenty-six-dimensional representation of type F₄ from TauCeti.Algebra.Lie.F4.ShortRoot.Basic to the rationals, lifts it to the universal enveloping algebra of the rational type-F₄ Serre Lie algebra, and proves that the coordinate ℤ-lattice of the rational module is admissible for the Serre Kostant form: it is stable under every divided power of a simple root generator and every binomial coefficient in a Cartan generator.

The long simple root generators square to zero on the module, so for them only the first divided power is nonzero. The short simple root generators have nilpotence index three: their squares are twice the integral divided-square matrices of TauCeti.Algebra.Lie.F4.ShortRoot.Basic, so their second divided powers are integral and their higher ones vanish. This is what distinguishes the short-root module from a minuscule one, and it is why the admissibility statement goes through the general divided-power criterion rather than the square-zero shortcut.

Main definitions #

TauCeti.F4ShortRoot.rationalSerreRepresentation: the rational Serre representation.
TauCeti.F4ShortRoot.rep: its extension to the universal enveloping algebra.
TauCeti.F4ShortRoot.lattice and TauCeti.F4ShortRoot.latticeBasis: the coordinate lattice and its standard basis.

Main results #

TauCeti.F4ShortRoot.pow_three_rep_serreRootGenerator_eq_zero and TauCeti.F4ShortRoot.isNilpotent_rep_serreRootGenerator: every represented simple root generator cubes to zero.
TauCeti.F4ShortRoot.isSl2Triple_rep_serreRootGenerator: the represented Cartan, raising and lowering generators at each node form an sl₂ triple.
TauCeti.F4ShortRoot.rep_dividedPower_serreRootGenerator_apply_mem_lattice: every divided power of a simple root generator preserves the lattice.
TauCeti.F4ShortRoot.isCartanWeightVector_latticeBasis: each lattice basis vector is a weight vector for the Cartan generators, with weight read from the weight table.
TauCeti.F4ShortRoot.rep_serreKostantForm_apply_mem_lattice: the lattice is admissible.

References #

B. Kostant, Groups over ℤ, in Algebraic Groups and Discontinuous Subgroups, Proc. Sympos. Pure Math. IX (1966).
R. Steinberg, Lectures on Chevalley Groups, §12, for admissible lattices and the lattice generated from a highest weight vector by divided powers.
J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §27.

Extension from the integral representation #

noncomputable def TauCeti.F4ShortRoot.raisingMatrixRat (i : Fin 4) :

Matrix (Fin 26) (Fin 26) ℚ

The rational raising matrix obtained from the integral short-root representation.

Equations

TauCeti.F4ShortRoot.raisingMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.F4ShortRoot.raisingMatrix i)

Instances For

noncomputable def TauCeti.F4ShortRoot.loweringMatrixRat (i : Fin 4) :

Matrix (Fin 26) (Fin 26) ℚ

The rational lowering matrix obtained from the integral short-root representation.

Equations

TauCeti.F4ShortRoot.loweringMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.F4ShortRoot.loweringMatrix i)

Instances For

noncomputable def TauCeti.F4ShortRoot.cartanMatrixRat (i : Fin 4) :

Matrix (Fin 26) (Fin 26) ℚ

The rational Cartan matrix obtained from the integral short-root representation.

Equations

TauCeti.F4ShortRoot.cartanMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.F4ShortRoot.cartanMatrix i)

Instances For

@[simp]

theorem TauCeti.F4ShortRoot.raisingMatrixRat_apply (i : Fin 4) (a b : Fin 26) :

raisingMatrixRat i a b = if a = raisingTarget i b then ↑(raisingCoeff i b) else 0

The entries of the rational raising matrix are the integral raising coefficients.

@[simp]

theorem TauCeti.F4ShortRoot.loweringMatrixRat_apply (i : Fin 4) (a b : Fin 26) :

loweringMatrixRat i a b = if a = loweringTarget i b then ↑(loweringCoeff i b) else 0

The entries of the rational lowering matrix are the integral lowering coefficients.

@[simp]

theorem TauCeti.F4ShortRoot.cartanMatrixRat_apply (i : Fin 4) (a b : Fin 26) :

cartanMatrixRat i a b = if a = b then ↑(DynkinType.f4ShortRootWeight a i) else 0

The rational Cartan matrix is diagonal with the short-root weights on its diagonal.

theorem TauCeti.F4ShortRoot.isSerreSystemRat :

IsSerreSystem ℚ CartanMatrix.F₄.transpose cartanMatrixRat raisingMatrixRat loweringMatrixRat

The rational short-root matrices satisfy the type-F₄ Serre relations.

theorem TauCeti.F4ShortRoot.isSl2TripleRat (i : Fin 4) :

IsSl2Triple (cartanMatrixRat i) (raisingMatrixRat i) (loweringMatrixRat i)

At each simple node, the three rational matrices form an sl₂ triple.

noncomputable def TauCeti.F4ShortRoot.rationalSerreRepresentation :

Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose →ₗ⁅ℚ ⁆ Matrix (Fin 26) (Fin 26) ℚ

The rational twenty-six-dimensional short-root representation of the type-F₄ Serre presentation.

Equations

TauCeti.F4ShortRoot.rationalSerreRepresentation = TauCeti.serreLift TauCeti.F4ShortRoot.isSerreSystemRat

Instances For

@[simp]

theorem TauCeti.F4ShortRoot.rationalSerreRepresentation_serreH (i : Fin 4) :

rationalSerreRepresentation (serreH ℚ CartanMatrix.F₄.transpose i) = cartanMatrixRat i

The rational Serre representation sends H_i to the rational Cartan matrix.

@[simp]

theorem TauCeti.F4ShortRoot.rationalSerreRepresentation_serreE (i : Fin 4) :

rationalSerreRepresentation (serreE ℚ CartanMatrix.F₄.transpose i) = raisingMatrixRat i

The rational Serre representation sends E_i to the rational raising matrix.

@[simp]

theorem TauCeti.F4ShortRoot.rationalSerreRepresentation_serreF (i : Fin 4) :

rationalSerreRepresentation (serreF ℚ CartanMatrix.F₄.transpose i) = loweringMatrixRat i

The rational Serre representation sends F_i to the rational lowering matrix.

The enveloping-algebra representation #

noncomputable def TauCeti.F4ShortRoot.rep :

UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose) →ₐ[ℚ ] Module.End ℚ (Fin 26 → ℚ)

The rational short-root representation extended to the universal enveloping algebra.

Equations

TauCeti.F4ShortRoot.rep = (UniversalEnvelopingAlgebra.lift ℚ) ((↑Matrix.toLinAlgEquiv').toLieHom.comp TauCeti.F4ShortRoot.rationalSerreRepresentation)

Instances For

theorem TauCeti.F4ShortRoot.rep_ι (x : Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose) :

rep ((UniversalEnvelopingAlgebra.ι ℚ) x) = Matrix.toLinAlgEquiv' (rationalSerreRepresentation x)

The enveloping-algebra inclusion is represented by the represented matrix.

theorem TauCeti.F4ShortRoot.rep_ι_apply (x : Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose) (v : Fin 26 → ℚ) :

(rep ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (rationalSerreRepresentation x).mulVec v

The enveloping-algebra inclusion acts by multiplying with the represented matrix.

theorem TauCeti.F4ShortRoot.rep_dividedPower_ι_apply (x : Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose) (n : ℕ) (v : Fin 26 → ℚ) :

(rep (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) x))) v = (Associative.dividedPower n (rationalSerreRepresentation x)).mulVec v

The enveloping-algebra representation sends the divided power of the inclusion of a Serre element to the matrix divided power of the represented matrix, acting on v.

theorem TauCeti.F4ShortRoot.rep_ι_pow (x : Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose) (n : ℕ) :

rep ((UniversalEnvelopingAlgebra.ι ℚ) x) ^ n = Matrix.toLinAlgEquiv' (rationalSerreRepresentation x ^ n)

The represented power of an inclusion is the represented matrix power. Powers pass through Matrix.toLinAlgEquiv' because it is an algebra equivalence.

noncomputable def TauCeti.F4ShortRoot.rootMatrixRat :

Fin 4 ⊕ Fin 4 → Matrix (Fin 26) (Fin 26) ℚ

The matrix a simple root generator is represented by: the rational raising or lowering matrix.

Equations

Instances For

def TauCeti.F4ShortRoot.rootMatrix :

Fin 4 ⊕ Fin 4 → Matrix (Fin 26) (Fin 26) ℤ

The integral matrix of a simple root generator: the raising or lowering matrix.

Equations

Instances For

def TauCeti.F4ShortRoot.rootDividedSquareMatrix :

Fin 4 ⊕ Fin 4 → Matrix (Fin 26) (Fin 26) ℤ

The integral divided square of a simple root generator.

Equations

Instances For

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrixRat_inl (i : Fin 4) :

rootMatrixRat (Sum.inl i) = raisingMatrixRat i

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrixRat_inr (i : Fin 4) :

rootMatrixRat (Sum.inr i) = loweringMatrixRat i

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrix_inl (i : Fin 4) :

rootMatrix (Sum.inl i) = raisingMatrix i

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrix_inr (i : Fin 4) :

rootMatrix (Sum.inr i) = loweringMatrix i

@[simp]

theorem TauCeti.F4ShortRoot.rootDividedSquareMatrix_inl (i : Fin 4) :

rootDividedSquareMatrix (Sum.inl i) = raisingDividedSquareMatrix i

@[simp]

theorem TauCeti.F4ShortRoot.rootDividedSquareMatrix_inr (i : Fin 4) :

rootDividedSquareMatrix (Sum.inr i) = loweringDividedSquareMatrix i

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrixRat_apply (k : Fin 4 ⊕ Fin 4) (a b : Fin 26) :

rootMatrixRat k a b = ↑(rootMatrix k a b)

The entries of the rational matrix of a simple root generator are the integral ones.

@[simp]

theorem TauCeti.F4ShortRoot.rationalSerreRepresentation_serreRootGenerator (k : Fin 4 ⊕ Fin 4) :

rationalSerreRepresentation (serreRootGenerator CartanMatrix.F₄.transpose k) = rootMatrixRat k

The rational Serre representation sends a simple root generator to its rational matrix.

The represented Cartan, positive and negative simple generators at a common type-F₄ node form an sl₂ triple.

theorem TauCeti.F4ShortRoot.rootMatrixRat_mul_self (k : Fin 4 ⊕ Fin 4) :

rootMatrixRat k * rootMatrixRat k = 2 • (rootDividedSquareMatrix k).map Int.cast

The square of a rational simple root matrix is twice the cast of its divided square.

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrix_pow_three (k : Fin 4 ⊕ Fin 4) :

rootMatrix k ^ 3 = 0

Every integral simple root matrix cubes to zero.

@[simp]

theorem TauCeti.F4ShortRoot.rootMatrixRat_pow_three (k : Fin 4 ⊕ Fin 4) :

rootMatrixRat k ^ 3 = 0

Every rational simple root matrix cubes to zero.

theorem TauCeti.F4ShortRoot.pow_three_rep_serreRootGenerator_eq_zero (k : Fin 4 ⊕ Fin 4) :

rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.F₄.transpose k)) ^ 3 = 0

Every simple root generator acts with cube zero in the rational short-root representation.

theorem TauCeti.F4ShortRoot.isNilpotent_rep_serreRootGenerator (k : Fin 4 ⊕ Fin 4) :

IsNilpotent (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.F₄.transpose k)))

Every represented simple root generator is nilpotent, with nilpotence index at most three.

The admissible coordinate lattice #

def TauCeti.F4ShortRoot.lattice :

Submodule ℤ (Fin 26 → ℚ)

The coordinate ℤ-lattice in the rational short-root module.

Equations

TauCeti.F4ShortRoot.lattice = TauCeti.coordinateLattice (Fin 26)

Instances For

@[simp]

theorem TauCeti.F4ShortRoot.mem_lattice_iff {v : Fin 26 → ℚ} :

v ∈ lattice ↔ ∀ (a : Fin 26), ∃ (z : ℤ), ↑z = v a

A short-root module vector belongs to the lattice exactly when every coordinate is integral.

noncomputable def TauCeti.F4ShortRoot.latticeBasis :

Module.Basis (Fin 26) ℤ ↥lattice

The coordinate basis of the short-root lattice.

Equations

TauCeti.F4ShortRoot.latticeBasis = TauCeti.coordinateLatticeBasis (Fin 26)

Instances For

@[simp]

theorem TauCeti.F4ShortRoot.coe_latticeBasis (a : Fin 26) :

↑(latticeBasis a) = Pi.single a 1

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

theorem TauCeti.F4ShortRoot.dividedPower_two_rootMatrixRat (k : Fin 4 ⊕ Fin 4) :

Associative.dividedPower 2 (rootMatrixRat k) = (rootDividedSquareMatrix k).map Int.cast

The divided square of a rational simple root matrix is the cast of its integral divided square.

theorem TauCeti.F4ShortRoot.dividedPower_rootMatrixRat_eq_zero (k : Fin 4 ⊕ Fin 4) {n : ℕ} (hn : 3 ≤ n) :

Associative.dividedPower n (rootMatrixRat k) = 0

The divided powers of a rational simple root matrix of order at least three vanish.

theorem TauCeti.F4ShortRoot.rep_dividedPower_serreRootGenerator_apply_mem_lattice (k : Fin 4 ⊕ Fin 4) (n : ℕ) {v : Fin 26 → ℚ} (hv : v ∈ lattice) :

(rep (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator CartanMatrix.F₄.transpose k)))) v ∈ lattice

Every divided power of a simple root generator preserves the short-root lattice.

theorem TauCeti.F4ShortRoot.isCartanWeightVector_single (a : Fin 26) :

UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ CartanMatrix.F₄.transpose) rep (DynkinType.f4ShortRootWeight a) (Pi.single a 1)

Each coordinate basis vector has the corresponding short-root weight for the Cartan generators.

theorem TauCeti.F4ShortRoot.isCartanWeightVector_latticeBasis (a : Fin 26) :

UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ CartanMatrix.F₄.transpose) rep (DynkinType.f4ShortRootWeight a) ↑(latticeBasis a)

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

theorem TauCeti.F4ShortRoot.rep_serreKostantForm_apply_mem_lattice {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ CartanMatrix.F₄.transpose)} (hu : u ∈ serreKostantForm CartanMatrix.F₄.transpose) {v : Fin 26 → ℚ} (hv : v ∈ lattice) :

(rep u) v ∈ lattice

The short-root coordinate lattice is admissible for the type-F₄ Serre Kostant form.