A tripled weight representation of the type-D4 Serre presentation

This file constructs a 24-dimensional integral representation of the type-D₄ Serre presentation. Its coordinate basis is indexed by the table TauCeti.DynkinType.d4TripledWeight, whose three blocks are the weights of the natural and two half-spin representations.

For a simple root i, the raising matrix sends the basis vector of weight μ to the basis vector of weight μ + αᵢ when ⟨μ, αᵢ∨⟩ = -1, and to zero otherwise. The lowering matrix is defined dually. The Cartan generator acts diagonally by the simple-coroot coordinate of the weight. Every nonzero entry of a raising or lowering matrix is 1, and the diagonal entries of the Cartan generators are the weight coordinates, in {-1, 0, 1}: on a minuscule weight table no sign is needed, which is what makes the triality symmetry of the table an unsigned symmetry of this representation, recorded entrywise in raisingMatrix_trialityPerm, loweringMatrix_trialityPerm and cartanGeneratorMatrix_trialityPerm. These integral matrices satisfy the Serre relations for the type-D₄ Cartan matrix. Identifying this presentation with the split semisimple Lie algebra of type D₄, and hence interpreting these matrices as a representation of that algebra, remains downstream.

This is the representation-theoretic input for the tripled type-D₄ Chevalley carrier, a full-weight carrier stable under triality. The weights span the full character lattice by TauCeti.DynkinType.span_range_d4TripledWeight_eq_top; constructing the associated Kostant carrier, its group scheme and its triality automorphism remains downstream.

Main declarations

• TauCeti.D4Tripled.weightTable: the minuscule weight table the construction reads, with weightTable_cartanMatrix, weightTable_weight and weightTable_reflection evaluating its three data fields.
• TauCeti.D4Tripled.raisingMatrix, loweringMatrix, and cartanGeneratorMatrix: the integral Chevalley generators on the tripled weight basis.
• TauCeti.D4Tripled.raisingMatrix_trialityPerm, loweringMatrix_trialityPerm, and cartanGeneratorMatrix_trialityPerm: triality carries each generator at node i to the generator at node trialityPermD4 i, entrywise along d4TripledTrialityPerm.
• TauCeti.D4Tripled.isSerreSystem: the generators satisfy the type-D₄ Serre relations.
• TauCeti.D4Tripled.serreRepresentation: the induced homomorphism from the integral type-D₄ Serre presentation.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§13.4 and 27.
• R. W. Carter, Simple Groups of Lie Type, §12.2.
• The construction follows the formal template of TauCeti.Algebra.Lie.E6.Minuscule.Basic, specialized to the tripled weight table of type D₄.

The weight table

def TauCeti.D4Tripled.weightTable : MinusculeWeightTable (Fin 4) (Fin 24)

The twenty-four tripled weights of type D₄, as a minuscule weight table. The type-D₄ Cartan matrix is symmetric, so no transpose is needed to place the coroot index first.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.weightTable_cartanMatrix : weightTable.cartanMatrix = CartanMatrix.D 4

The Cartan matrix of the tripled type-D₄ weight table is the D₄ Cartan matrix.

@[simp]

theorem TauCeti.D4Tripled.weightTable_weight : weightTable.weight = DynkinType.d4TripledWeight

The weights of the tripled type-D₄ weight table are the tripled weights.

@[simp]

theorem TauCeti.D4Tripled.weightTable_reflection (i : Fin 4) : weightTable.reflection i = ⇑(DynkinType.d4TripledReflection i)

The simple reflections of the tripled type-D₄ weight table are the tripled reflections.

Triality symmetry

def TauCeti.D4Tripled.trialitySymmetry : weightTable.Symmetry

Triality as a symmetry of the tripled minuscule weight table. It acts simultaneously on the type-D₄ nodes and on the twenty-four weight indices.

Equations

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

@[simp]

theorem TauCeti.D4Tripled.trialitySymmetry_nodePerm : trialitySymmetry.nodePerm = trialityPermD4

The node permutation of the bundled triality symmetry is diagram triality.

@[simp]

theorem TauCeti.D4Tripled.trialitySymmetry_indexPerm : trialitySymmetry.indexPerm = DynkinType.d4TripledTrialityPerm

The weight-index permutation of the bundled triality symmetry is triality on the tripled weight table.

@[simp]

theorem TauCeti.D4Tripled.trialitySymmetry_pow_three : trialitySymmetry ^ 3 = 1

The bundled triality symmetry has order dividing three.

The Chevalley generators

def TauCeti.D4Tripled.raisingMatrix (i : Fin 4) : Matrix (Fin 24) (Fin 24) ℤ

The raising matrix of the i-th simple root on the integral tripled weight basis.

Equations

• TauCeti.D4Tripled.raisingMatrix i = TauCeti.D4Tripled.weightTable.raisingMatrix i

def TauCeti.D4Tripled.loweringMatrix (i : Fin 4) : Matrix (Fin 24) (Fin 24) ℤ

The lowering matrix of the i-th simple root on the integral tripled weight basis.

Equations

• TauCeti.D4Tripled.loweringMatrix i = TauCeti.D4Tripled.weightTable.loweringMatrix i

def TauCeti.D4Tripled.cartanGeneratorMatrix (i : Fin 4) : Matrix (Fin 24) (Fin 24) ℤ

The diagonal matrix of the i-th simple coroot on the integral tripled weight basis.

Equations

• TauCeti.D4Tripled.cartanGeneratorMatrix i = TauCeti.D4Tripled.weightTable.cartanGeneratorMatrix i

theorem TauCeti.D4Tripled.raisingMatrix_def (i : Fin 4) : raisingMatrix i = weightTable.raisingMatrix i

The raising matrix is the raising matrix of the tripled weight table.

theorem TauCeti.D4Tripled.loweringMatrix_def (i : Fin 4) : loweringMatrix i = weightTable.loweringMatrix i

The lowering matrix is the lowering matrix of the tripled weight table.

@[simp]

theorem TauCeti.D4Tripled.raisingMatrix_apply (i : Fin 4) (a b : Fin 24) : raisingMatrix i a b = if DynkinType.d4TripledWeight b i = -1 ∧ a = (DynkinType.d4TripledReflection i) b then 1 else 0

The entry formula for a simple raising matrix.

@[simp]

theorem TauCeti.D4Tripled.loweringMatrix_apply (i : Fin 4) (a b : Fin 24) : loweringMatrix i a b = if DynkinType.d4TripledWeight b i = 1 ∧ a = (DynkinType.d4TripledReflection i) b then 1 else 0

The entry formula for a simple lowering matrix.

@[simp]

theorem TauCeti.D4Tripled.cartanGeneratorMatrix_apply (i : Fin 4) (a b : Fin 24) : cartanGeneratorMatrix i a b = if a = b then DynkinType.d4TripledWeight b i else 0

The entry formula for a simple Cartan generator matrix.

Triality on the generators

Triality permutes the weight basis by d4TripledTrialityPerm and the nodes by trialityPermD4, and it carries each Chevalley generator at a node to the generator at the image node, with no change of sign: reading a generator at the image node in the image basis gives back the generator at the original node.

None of the three equations is a simp lemma: the entry formulas raisingMatrix_apply, loweringMatrix_apply and cartanGeneratorMatrix_apply are, and they already rewrite both sides to conditions on the weight table, so the left-hand sides below are not simp-normal.

theorem TauCeti.D4Tripled.raisingMatrix_trialityPerm (i : Fin 4) (a b : Fin 24) : raisingMatrix (trialityPermD4 i) (DynkinType.d4TripledTrialityPerm a) (DynkinType.d4TripledTrialityPerm b) = raisingMatrix i a b

Triality carries the raising matrix at node i to the raising matrix at node trialityPermD4 i, entrywise along d4TripledTrialityPerm.

theorem TauCeti.D4Tripled.loweringMatrix_trialityPerm (i : Fin 4) (a b : Fin 24) : loweringMatrix (trialityPermD4 i) (DynkinType.d4TripledTrialityPerm a) (DynkinType.d4TripledTrialityPerm b) = loweringMatrix i a b

Triality carries the lowering matrix at node i to the lowering matrix at node trialityPermD4 i, entrywise along d4TripledTrialityPerm.

theorem TauCeti.D4Tripled.cartanGeneratorMatrix_trialityPerm (i : Fin 4) (a b : Fin 24) : cartanGeneratorMatrix (trialityPermD4 i) (DynkinType.d4TripledTrialityPerm a) (DynkinType.d4TripledTrialityPerm b) = cartanGeneratorMatrix i a b

Triality carries the Cartan generator at node i to the Cartan generator at node trialityPermD4 i, entrywise along d4TripledTrialityPerm.

@[simp]

theorem TauCeti.D4Tripled.raisingMatrix_trialityPerm_submatrix (i : Fin 4) : (raisingMatrix (trialityPermD4 i)).submatrix ⇑DynkinType.d4TripledTrialityPerm ⇑DynkinType.d4TripledTrialityPerm = raisingMatrix i

Triality carries the raising matrix at node i to the raising matrix at node trialityPermD4 i, as a matrix reindexing identity.

@[simp]

theorem TauCeti.D4Tripled.loweringMatrix_trialityPerm_submatrix (i : Fin 4) : (loweringMatrix (trialityPermD4 i)).submatrix ⇑DynkinType.d4TripledTrialityPerm ⇑DynkinType.d4TripledTrialityPerm = loweringMatrix i

Triality carries the lowering matrix at node i to the lowering matrix at node trialityPermD4 i, as a matrix reindexing identity.

@[simp]

theorem TauCeti.D4Tripled.cartanGeneratorMatrix_trialityPerm_submatrix (i : Fin 4) : (cartanGeneratorMatrix (trialityPermD4 i)).submatrix ⇑DynkinType.d4TripledTrialityPerm ⇑DynkinType.d4TripledTrialityPerm = cartanGeneratorMatrix i

Triality carries the Cartan generator at node i to the Cartan generator at node trialityPermD4 i, as a matrix reindexing identity.

@[simp]

theorem TauCeti.D4Tripled.raisingMatrix_pow_two (i : Fin 4) : raisingMatrix i ^ 2 = 0

Every raising matrix of the tripled weight table squares to zero.

@[simp]

theorem TauCeti.D4Tripled.loweringMatrix_pow_two (i : Fin 4) : loweringMatrix i ^ 2 = 0

Every lowering matrix of the tripled weight table squares to zero.

The Serre relations

theorem TauCeti.D4Tripled.isSl2Triple (i : Fin 4) : IsSl2Triple (cartanGeneratorMatrix i) (raisingMatrix i) (loweringMatrix i)

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

theorem TauCeti.D4Tripled.isSerreSystem : IsSerreSystem ℤ (CartanMatrix.D 4) cartanGeneratorMatrix raisingMatrix loweringMatrix

The integral 24-dimensional tripled matrices satisfy the Serre relations of type D₄. The type-D₄ Cartan matrix is symmetric, so no transpose is needed to place the coroot index first.

noncomputable def TauCeti.D4Tripled.serreRepresentation : Matrix.ToLieAlgebra ℤ (CartanMatrix.D 4) →ₗ⁅ℤ⁆ Matrix (Fin 24) (Fin 24) ℤ

The integral 24-dimensional tripled representation of the type-D₄ Serre presentation.

Equations

• TauCeti.D4Tripled.serreRepresentation = TauCeti.D4Tripled.weightTable.serreRepresentation

@[simp]

theorem TauCeti.D4Tripled.serreRepresentation_serreH (i : Fin 4) : serreRepresentation (serreH ℤ (CartanMatrix.D 4) i) = cartanGeneratorMatrix i

The tripled representation sends a Cartan generator to its diagonal weight matrix.

@[simp]

theorem TauCeti.D4Tripled.serreRepresentation_serreE (i : Fin 4) : serreRepresentation (serreE ℤ (CartanMatrix.D 4) i) = raisingMatrix i

The tripled representation sends a positive generator to its raising matrix.

@[simp]

theorem TauCeti.D4Tripled.serreRepresentation_serreF (i : Fin 4) : serreRepresentation (serreF ℤ (CartanMatrix.D 4) i) = loweringMatrix i

The tripled representation sends a negative generator to its lowering matrix.