The admissible doubled minuscule lattice of type E6

This file extends the integral doubled minuscule representation V(ϖ₁) ⊕ V(ϖ₆) to the rational type-E₆ Serre algebra and proves that its coordinate ℤ-lattice is preserved by the Serre Kostant form. Its raising and lowering matrices are square-zero, and its coordinate basis consists of Cartan weight vectors with weights TauCeti.DynkinType.e6DoubledMinusculeWeight.

The resulting admissible lattice is both full-weight and stable under the type-E₆ diagram symmetry at the level of its weight basis. It is therefore the lattice input for the graph-stable type-E₆ Chevalley--Demazure carrier required by Layer 9 of the ReductiveGroups roadmap and by the ²E₆ branch of the CFSGStatement roadmap.

The rationalization and coordinate-lattice argument specialize the formal pattern of TauCeti/Algebra/Lie/E6/Minuscule/AdmissibleLattice.lean; the mathematical change is the contragredient second block and its doubled weight basis.

Main declarations

• TauCeti.E6DoubledMinuscule.rationalSerreRepresentation: the rational doubled minuscule representation.
• TauCeti.E6DoubledMinuscule.rep: its universal-enveloping-algebra representation.
• TauCeti.E6DoubledMinuscule.isSl2Triple_rep_serreRootGenerator: the represented generators at every node form an sl₂ triple.
• TauCeti.E6DoubledMinuscule.lattice: the coordinate ℤ-lattice.
• TauCeti.E6DoubledMinuscule.rep_serreKostantForm_mem_lattice: the Serre Kostant form preserves the lattice.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• R. W. Carter, Simple Groups of Lie Type, §12.2.

The rational representation

noncomputable def TauCeti.E6DoubledMinuscule.raisingMatrixQ (i : Fin 6) : Matrix (Fin 27 ⊕ Fin 27) (Fin 27 ⊕ Fin 27) ℚ

The rational raising matrices of the doubled minuscule representation.

Equations

• TauCeti.E6DoubledMinuscule.raisingMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E6DoubledMinuscule.raisingMatrix i)

noncomputable def TauCeti.E6DoubledMinuscule.loweringMatrixQ (i : Fin 6) : Matrix (Fin 27 ⊕ Fin 27) (Fin 27 ⊕ Fin 27) ℚ

The rational lowering matrices of the doubled minuscule representation.

Equations

• TauCeti.E6DoubledMinuscule.loweringMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E6DoubledMinuscule.loweringMatrix i)

noncomputable def TauCeti.E6DoubledMinuscule.cartanGeneratorMatrixQ (i : Fin 6) : Matrix (Fin 27 ⊕ Fin 27) (Fin 27 ⊕ Fin 27) ℚ

The rational Cartan generators of the doubled minuscule representation.

Equations

• TauCeti.E6DoubledMinuscule.cartanGeneratorMatrixQ i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E6DoubledMinuscule.cartanGeneratorMatrix i)

@[simp]

theorem TauCeti.E6DoubledMinuscule.raisingMatrixQ_apply (i : Fin 6) (a b : Fin 27 ⊕ Fin 27) : raisingMatrixQ i a b = if DynkinType.e6DoubledMinusculeWeight b i = -1 ∧ a = (reflection i) b then ↑(summandSign b) else 0

Entry formula for a rational raising matrix.

@[simp]

theorem TauCeti.E6DoubledMinuscule.loweringMatrixQ_apply (i : Fin 6) (a b : Fin 27 ⊕ Fin 27) : loweringMatrixQ i a b = if DynkinType.e6DoubledMinusculeWeight b i = 1 ∧ a = (reflection i) b then ↑(summandSign b) else 0

Entry formula for a rational lowering matrix.

@[simp]

theorem TauCeti.E6DoubledMinuscule.cartanGeneratorMatrixQ_apply (i : Fin 6) (a b : Fin 27 ⊕ Fin 27) : cartanGeneratorMatrixQ i a b = if a = b then ↑(DynkinType.e6DoubledMinusculeWeight b i) else 0

A rational Cartan generator is diagonal with the doubled minuscule weights on its diagonal.

theorem TauCeti.E6DoubledMinuscule.isSerreSystemQ : IsSerreSystem ℚ (CartanMatrix.E 6).transpose cartanGeneratorMatrixQ raisingMatrixQ loweringMatrixQ

The rational doubled minuscule matrices satisfy the type-E₆ Serre relations.

theorem TauCeti.E6DoubledMinuscule.isSl2TripleQ (i : Fin 6) : IsSl2Triple (cartanGeneratorMatrixQ i) (raisingMatrixQ i) (loweringMatrixQ i)

At every node, the rational Cartan, raising, and lowering matrices of the doubled minuscule representation form an sl₂ triple.

noncomputable def TauCeti.E6DoubledMinuscule.rationalSerreRepresentation : Matrix.ToLieAlgebra ℚ (CartanMatrix.E 6).transpose →ₗ⁅ℚ⁆ Matrix (Fin 27 ⊕ Fin 27) (Fin 27 ⊕ Fin 27) ℚ

The rational 54-dimensional doubled minuscule representation.

Equations

• TauCeti.E6DoubledMinuscule.rationalSerreRepresentation = TauCeti.serreLift TauCeti.E6DoubledMinuscule.isSerreSystemQ

@[simp]

theorem TauCeti.E6DoubledMinuscule.rationalSerreRepresentation_serreH (i : Fin 6) : rationalSerreRepresentation (serreH ℚ (CartanMatrix.E 6).transpose i) = cartanGeneratorMatrixQ i

@[simp]

theorem TauCeti.E6DoubledMinuscule.rationalSerreRepresentation_serreE (i : Fin 6) : rationalSerreRepresentation (serreE ℚ (CartanMatrix.E 6).transpose i) = raisingMatrixQ i

@[simp]

theorem TauCeti.E6DoubledMinuscule.rationalSerreRepresentation_serreF (i : Fin 6) : rationalSerreRepresentation (serreF ℚ (CartanMatrix.E 6).transpose i) = loweringMatrixQ i

The enveloping-algebra action

noncomputable def TauCeti.E6DoubledMinuscule.rep : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 6).transpose) →ₐ[ℚ] Module.End ℚ (Fin 27 ⊕ Fin 27 → ℚ)

The rational doubled minuscule representation extended to the universal enveloping algebra.

Equations

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

theorem TauCeti.E6DoubledMinuscule.rep_ι_apply (x : Matrix.ToLieAlgebra ℚ (CartanMatrix.E 6).transpose) (v : Fin 27 ⊕ Fin 27 → ℚ) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (rationalSerreRepresentation x).mulVec v

Included Lie elements act by matrix-vector multiplication.

@[simp]

theorem TauCeti.E6DoubledMinuscule.raisingMatrixQ_sq (i : Fin 6) : raisingMatrixQ i ^ 2 = 0

Every rational raising matrix is square-zero.

@[simp]

theorem TauCeti.E6DoubledMinuscule.loweringMatrixQ_sq (i : Fin 6) : loweringMatrixQ i ^ 2 = 0

Every rational lowering matrix is square-zero.

theorem TauCeti.E6DoubledMinuscule.rep_serreRootGenerator_sq (k : Fin 6 ⊕ Fin 6) : rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose k)) ^ 2 = 0

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

theorem TauCeti.E6DoubledMinuscule.isNilpotent_rep_serreRootGenerator (k : Fin 6 ⊕ Fin 6) : IsNilpotent (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose k)))

Every represented Serre root generator acts nilpotently.

theorem TauCeti.E6DoubledMinuscule.isSl2Triple_rep_serreRootGenerator (i : Fin 6) : IsSl2Triple (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreH ℚ (CartanMatrix.E 6).transpose i))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose (Sum.inl i)))) (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose (Sum.inr i))))

The represented Cartan, positive, and negative Serre generators at every node form an sl₂ triple.

The admissible coordinate lattice

def TauCeti.E6DoubledMinuscule.lattice : Submodule ℤ (Fin 27 ⊕ Fin 27 → ℚ)

The coordinate ℤ-lattice in the rational doubled minuscule module.

Equations

• TauCeti.E6DoubledMinuscule.lattice = TauCeti.coordinateLattice (Fin 27 ⊕ Fin 27)

@[simp]

theorem TauCeti.E6DoubledMinuscule.mem_lattice_iff {v : Fin 27 ⊕ Fin 27 → ℚ} : v ∈ lattice ↔ ∀ (a : Fin 27 ⊕ Fin 27), ∃ (z : ℤ), ↑z = v a

A vector belongs to the doubled minuscule lattice exactly when every coordinate is integral.

theorem TauCeti.E6DoubledMinuscule.single_mem_lattice (a : Fin 27 ⊕ Fin 27) : Pi.single a 1 ∈ lattice

Every standard coordinate vector belongs to the doubled minuscule lattice.

noncomputable def TauCeti.E6DoubledMinuscule.latticeBasis : Module.Basis (Fin 27 ⊕ Fin 27) ℤ ↥lattice

The coordinate basis of the doubled minuscule lattice.

Equations

• TauCeti.E6DoubledMinuscule.latticeBasis = TauCeti.coordinateLatticeBasis (Fin 27 ⊕ Fin 27)

@[simp]

theorem TauCeti.E6DoubledMinuscule.coe_latticeBasis (a : Fin 27 ⊕ Fin 27) : ↑(latticeBasis a) = Pi.single a 1

Coercing a lattice-basis vector gives the corresponding coordinate vector.

theorem TauCeti.E6DoubledMinuscule.rep_serreRootGenerator_mem_lattice (k : Fin 6 ⊕ Fin 6) {v : Fin 27 ⊕ Fin 27 → ℚ} (hv : v ∈ lattice) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose k))) v ∈ lattice

Every represented Serre root generator preserves the doubled minuscule lattice.

theorem TauCeti.E6DoubledMinuscule.isCartanWeightVector_single (a : Fin 27 ⊕ Fin 27) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.E 6).transpose) rep (DynkinType.e6DoubledMinusculeWeight a) (Pi.single a 1)

Every standard coordinate vector has its named doubled minuscule weight.

theorem TauCeti.E6DoubledMinuscule.isCartanWeightVector_latticeBasis (a : Fin 27 ⊕ Fin 27) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.E 6).transpose) rep (DynkinType.e6DoubledMinusculeWeight a) ↑(latticeBasis a)

Every doubled minuscule lattice-basis vector has its named Cartan weight.

theorem TauCeti.E6DoubledMinuscule.rep_serreKostantForm_mem_lattice {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 6).transpose)} (hu : u ∈ serreKostantForm (CartanMatrix.E 6).transpose) {v : Fin 27 ⊕ Fin 27 → ℚ} (hv : v ∈ lattice) : (rep u) v ∈ lattice

The doubled minuscule coordinate lattice is admissible for the type-E₆ Serre Kostant form.