The integral short-root representation of type F4

This file realizes the Chevalley generators of type F₄ on the twenty-six-element weight diagram TauCeti.DynkinType.f4ShortRootWeight, whose weights are the twenty-four short roots and the zero weight taken twice. On the coordinate vector belonging to the bth weight, the Cartan generator H_i acts by the simple-coroot coordinate of that weight, and each raising generator E_i and lowering generator F_i carries the coordinate vector to an integer multiple of a single coordinate vector, read from explicit target and coefficient tables. Every generator is therefore a step matrix, a matrix each of whose columns has at most one nonzero entry, and products of step matrices are again step matrices.

The resulting integer matrices satisfy the Chevalley--Serre relations for the transpose of the Bourbaki Cartan matrix of type F₄, which is the convention under which ⁅H_i, E_j⁆ is the pairing of the jth simple root with the ith simple coroot times E_j. The universal property of the Serre presentation gives the explicit integral twenty-six-dimensional representation. The two long simple raising and lowering generators square to zero. The two short ones do not: their squares are twice an integral matrix, the divided square, and their cubes vanish. Those divided squares are what an admissible lattice built on this weight basis must be stable under.

The two zero-weight coordinate vectors are the images of the two short simple lowering generators applied to the coordinate vectors of the corresponding simple roots, and the tables record how each short simple raising generator returns them: the one from its own root with coefficient two, the other with coefficient one.

No identification with the abstract irreducible highest-weight module is asserted here, and the zero-weight basis is the explicitly tabulated one rather than one characterized by a generation property. The construction is explicit: every matrix entry is read from the weight, target and coefficient tables.

Main definitions

• TauCeti.F4ShortRoot.cartanMatrix, raisingMatrix, and loweringMatrix: the integral Cartan, raising, and lowering matrices.
• TauCeti.F4ShortRoot.raisingDividedSquareMatrix and loweringDividedSquareMatrix: the divided squares of the raising and lowering matrices.
• TauCeti.F4ShortRoot.isSerreSystem: the Chevalley--Serre relations between them over ℤ, with TauCeti.F4ShortRoot.isSl2Triple the sl₂ triple at each node.
• TauCeti.F4ShortRoot.serreRepresentation: the induced representation of the type-F₄ Serre Lie algebra.

Main results

• TauCeti.F4ShortRoot.raisingMatrix_mul_self and loweringMatrix_mul_self: each square is twice the divided square.
• TauCeti.F4ShortRoot.raisingMatrix_mul_raisingDividedSquareMatrix and its three siblings: each generator annihilates its own divided square on either side, so each generator cubes to zero.
• TauCeti.F4ShortRoot.raisingMatrix_mul_self_of_lt_two and loweringMatrix_mul_self_of_lt_two: the two long simple generators square to zero.

References

The numbering follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII. The admissible lattice generated from a highest weight vector by divided-power lowering operators is the one of B. Kostant, Groups over ℤ, and R. Steinberg, Lectures on Chevalley Groups, §12. The construction of the twenty-six-dimensional module from its weight diagram and the Serre presentation follows J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§18 and 27.

Step matrices

The tables

def TauCeti.F4ShortRoot.raisingTarget : Fin 4 → Fin 26 → Fin 26

The target index of each coordinate vector under the ith raising generator; a column with coefficient zero has itself as its target.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.raisingCoeff : Fin 4 → Fin 26 → ℤ

The coefficient of each coordinate vector under the ith raising generator.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.loweringTarget : Fin 4 → Fin 26 → Fin 26

The target index of each coordinate vector under the ith lowering generator; a column with coefficient zero has itself as its target.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.loweringCoeff : Fin 4 → Fin 26 → ℤ

The coefficient of each coordinate vector under the ith lowering generator.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.raisingDividedSquareTarget : Fin 4 → Fin 26 → Fin 26

The target index of each coordinate vector under the divided square of the ith raising generator. Only the two short simple roots contribute, each moving the coordinate vector of the negative of its root to that of the root itself.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.raisingDividedSquareCoeff : Fin 4 → Fin 26 → ℤ

The coefficient of each coordinate vector under the divided square of the ith raising generator.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.loweringDividedSquareTarget : Fin 4 → Fin 26 → Fin 26

The target index of each coordinate vector under the divided square of the ith lowering generator.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.F4ShortRoot.loweringDividedSquareCoeff : Fin 4 → Fin 26 → ℤ

The coefficient of each coordinate vector under the divided square of the ith lowering generator.

Equations

• One or more equations did not get rendered due to their size.

The integral generator matrices

def TauCeti.F4ShortRoot.cartanMatrix (i : Fin 4) : Matrix (Fin 26) (Fin 26) ℤ

The Cartan generator H_i in the short-root weight basis.

Equations

• TauCeti.F4ShortRoot.cartanMatrix i = Matrix.diagonal fun (a : Fin 26) => TauCeti.DynkinType.f4ShortRootWeight a i

def TauCeti.F4ShortRoot.raisingMatrix (i : Fin 4) : Matrix (Fin 26) (Fin 26) ℤ

The raising generator E_i in the short-root weight basis.

Equations

• TauCeti.F4ShortRoot.raisingMatrix i = TauCeti.F4ShortRoot.stepMatrix✝ (TauCeti.F4ShortRoot.raisingTarget i) (TauCeti.F4ShortRoot.raisingCoeff i)

def TauCeti.F4ShortRoot.loweringMatrix (i : Fin 4) : Matrix (Fin 26) (Fin 26) ℤ

The lowering generator F_i in the short-root weight basis.

Equations

• TauCeti.F4ShortRoot.loweringMatrix i = TauCeti.F4ShortRoot.stepMatrix✝ (TauCeti.F4ShortRoot.loweringTarget i) (TauCeti.F4ShortRoot.loweringCoeff i)

def TauCeti.F4ShortRoot.raisingDividedSquareMatrix (i : Fin 4) : Matrix (Fin 26) (Fin 26) ℤ

The divided square E_i^(2) = E_i² / 2 of the raising generator, an integral matrix.

Equations

• TauCeti.F4ShortRoot.raisingDividedSquareMatrix i = TauCeti.F4ShortRoot.stepMatrix✝ (TauCeti.F4ShortRoot.raisingDividedSquareTarget i) (TauCeti.F4ShortRoot.raisingDividedSquareCoeff i)

def TauCeti.F4ShortRoot.loweringDividedSquareMatrix (i : Fin 4) : Matrix (Fin 26) (Fin 26) ℤ

The divided square F_i^(2) = F_i² / 2 of the lowering generator, an integral matrix.

Equations

• TauCeti.F4ShortRoot.loweringDividedSquareMatrix i = TauCeti.F4ShortRoot.stepMatrix✝ (TauCeti.F4ShortRoot.loweringDividedSquareTarget i) (TauCeti.F4ShortRoot.loweringDividedSquareCoeff i)

@[simp]

theorem TauCeti.F4ShortRoot.cartanMatrix_apply (i : Fin 4) (a b : Fin 26) : cartanMatrix i a b = if a = b then DynkinType.f4ShortRootWeight a i else 0

The entrywise formula for the diagonal Cartan generator matrix.

@[simp]

theorem TauCeti.F4ShortRoot.raisingMatrix_apply (i : Fin 4) (a b : Fin 26) : raisingMatrix i a b = if a = raisingTarget i b then raisingCoeff i b else 0

The entrywise formula for the raising generator matrix.

@[simp]

theorem TauCeti.F4ShortRoot.loweringMatrix_apply (i : Fin 4) (a b : Fin 26) : loweringMatrix i a b = if a = loweringTarget i b then loweringCoeff i b else 0

The entrywise formula for the lowering generator matrix.

@[simp]

theorem TauCeti.F4ShortRoot.raisingDividedSquareMatrix_apply (i : Fin 4) (a b : Fin 26) : raisingDividedSquareMatrix i a b = if a = raisingDividedSquareTarget i b then raisingDividedSquareCoeff i b else 0

The entrywise formula for the divided square of the raising generator.

@[simp]

theorem TauCeti.F4ShortRoot.loweringDividedSquareMatrix_apply (i : Fin 4) (a b : Fin 26) : loweringDividedSquareMatrix i a b = if a = loweringDividedSquareTarget i b then loweringDividedSquareCoeff i b else 0

The entrywise formula for the divided square of the lowering generator.

Chevalley--Serre relations

theorem TauCeti.F4ShortRoot.isSerreSystem : IsSerreSystem ℤ CartanMatrix.F₄.transpose cartanMatrix raisingMatrix loweringMatrix

The integral short-root generator matrices satisfy the Chevalley--Serre relations of type F₄, for the transpose of the Bourbaki Cartan matrix, in Bourbaki numbering.

theorem TauCeti.F4ShortRoot.isSl2Triple (i : Fin 4) : IsSl2Triple (cartanMatrix i) (raisingMatrix i) (loweringMatrix i)

At each simple node, the integral Cartan, raising and lowering matrices form an sl₂ triple: the raising and lowering matrices bracket to the nonzero Cartan matrix, which brackets with them to 2 and -2 times themselves. So each node spans a copy of sl₂ inside the matrix Lie algebra of the integral short-root module.

noncomputable def TauCeti.F4ShortRoot.serreRepresentation : Matrix.ToLieAlgebra ℤ CartanMatrix.F₄.transpose →ₗ⁅ℤ⁆ Matrix (Fin 26) (Fin 26) ℤ

The explicit integral twenty-six-dimensional representation of the type-F₄ Serre Lie algebra.

Equations

• TauCeti.F4ShortRoot.serreRepresentation = TauCeti.serreLift TauCeti.F4ShortRoot.isSerreSystem

@[simp]

theorem TauCeti.F4ShortRoot.serreRepresentation_serreH (i : Fin 4) : serreRepresentation (serreH ℤ CartanMatrix.F₄.transpose i) = cartanMatrix i

The integral Serre representation sends H_i to the Cartan generator matrix.

@[simp]

theorem TauCeti.F4ShortRoot.serreRepresentation_serreE (i : Fin 4) : serreRepresentation (serreE ℤ CartanMatrix.F₄.transpose i) = raisingMatrix i

The integral Serre representation sends E_i to the raising generator matrix.

@[simp]

theorem TauCeti.F4ShortRoot.serreRepresentation_serreF (i : Fin 4) : serreRepresentation (serreF ℤ CartanMatrix.F₄.transpose i) = loweringMatrix i

The integral Serre representation sends F_i to the lowering generator matrix.

Squares and cubes of the generators

theorem TauCeti.F4ShortRoot.raisingMatrix_mul_self (i : Fin 4) : raisingMatrix i * raisingMatrix i = 2 • raisingDividedSquareMatrix i

The square of a raising generator is twice its divided square.

theorem TauCeti.F4ShortRoot.loweringMatrix_mul_self (i : Fin 4) : loweringMatrix i * loweringMatrix i = 2 • loweringDividedSquareMatrix i

The square of a lowering generator is twice its divided square.

@[simp]

theorem TauCeti.F4ShortRoot.raisingMatrix_mul_raisingDividedSquareMatrix (i : Fin 4) : raisingMatrix i * raisingDividedSquareMatrix i = 0

A raising generator annihilates its divided square on the left.

@[simp]

theorem TauCeti.F4ShortRoot.raisingDividedSquareMatrix_mul_raisingMatrix (i : Fin 4) : raisingDividedSquareMatrix i * raisingMatrix i = 0

A raising generator annihilates its divided square on the right.

@[simp]

theorem TauCeti.F4ShortRoot.loweringMatrix_mul_loweringDividedSquareMatrix (i : Fin 4) : loweringMatrix i * loweringDividedSquareMatrix i = 0

A lowering generator annihilates its divided square on the left.

@[simp]

theorem TauCeti.F4ShortRoot.loweringDividedSquareMatrix_mul_loweringMatrix (i : Fin 4) : loweringDividedSquareMatrix i * loweringMatrix i = 0

A lowering generator annihilates its divided square on the right.

@[simp]

theorem TauCeti.F4ShortRoot.raisingMatrix_pow_three (i : Fin 4) : raisingMatrix i ^ 3 = 0

Every raising generator cubes to zero.

@[simp]

theorem TauCeti.F4ShortRoot.loweringMatrix_pow_three (i : Fin 4) : loweringMatrix i ^ 3 = 0

Every lowering generator cubes to zero.

theorem TauCeti.F4ShortRoot.raisingDividedSquareMatrix_eq_zero_of_lt_two (i : Fin 4) (hi : ↑i < 2) : raisingDividedSquareMatrix i = 0

The divided square of a long simple raising generator vanishes.

theorem TauCeti.F4ShortRoot.loweringDividedSquareMatrix_eq_zero_of_lt_two (i : Fin 4) (hi : ↑i < 2) : loweringDividedSquareMatrix i = 0

The divided square of a long simple lowering generator vanishes.

@[simp]

theorem TauCeti.F4ShortRoot.raisingMatrix_mul_self_of_lt_two (i : Fin 4) (hi : ↑i < 2) : raisingMatrix i * raisingMatrix i = 0

The long simple raising generators square to zero.

@[simp]

theorem TauCeti.F4ShortRoot.loweringMatrix_mul_self_of_lt_two (i : Fin 4) (hi : ↑i < 2) : loweringMatrix i * loweringMatrix i = 0

The long simple lowering generators square to zero.