The admissible lattice in the type-E7 minuscule representation

This file extends the integral 56-dimensional minuscule representation of the type-E₇ Serre presentation to the rational Serre algebra and proves that its coordinate ℤ-lattice is preserved by the Serre Kostant form. The raising and lowering matrices have integral entries, are square-zero, and preserve the coordinate lattice. The Cartan matrices act diagonally through the weights TauCeti.DynkinType.e7MinusculeWeight.

Thus the minuscule coordinate lattice is an admissible lattice for the explicit Serre-generator Kostant form. Its weights span the full type-E₇ character lattice by TauCeti.DynkinType.span_range_e7MinusculeWeight_eq_top. These are the lattice inputs needed for the full-weight type-E₇ Chevalley--Demazure carrier in Layer 9 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.E7Minuscule.rationalSerreRepresentation: the rational minuscule representation.
• TauCeti.E7Minuscule.rep: its extension to the universal enveloping algebra.
• TauCeti.E7Minuscule.isSl2Triple_rep_serreRootGenerator: the represented generators at every simple node form an sl₂ triple.
• TauCeti.E7Minuscule.isNilpotent_rep_serreRootGenerator: the simple-root generators act nilpotently.
• TauCeti.E7Minuscule.lattice: the coordinate ℤ-lattice in the rational module.
• TauCeti.E7Minuscule.rep_serreKostantForm_apply_mem_lattice: the Serre Kostant form preserves the lattice.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§13 and 26--27.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.

The formal organization follows the parallel type-E₆ admissible-lattice development in TauCetiProject/TauCeti#5204, specialized here to the already constructed E₇ minuscule Serre system.

Extension from the integral representation

noncomputable def TauCeti.E7Minuscule.raisingMatrixRat (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℚ

The rational raising matrix obtained from the integral minuscule representation.

Equations

• TauCeti.E7Minuscule.raisingMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E7Minuscule.raisingMatrix i)

noncomputable def TauCeti.E7Minuscule.loweringMatrixRat (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℚ

The rational lowering matrix obtained from the integral minuscule representation.

Equations

• TauCeti.E7Minuscule.loweringMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E7Minuscule.loweringMatrix i)

noncomputable def TauCeti.E7Minuscule.cartanMatrixRat (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℚ

The rational Cartan matrix obtained from the integral minuscule representation.

Equations

• TauCeti.E7Minuscule.cartanMatrixRat i = (TauCeti.matrixIntCastLieHom ℚ) (TauCeti.E7Minuscule.cartanMatrix i)

@[simp]

theorem TauCeti.E7Minuscule.raisingMatrixRat_apply (i : Fin 7) (a b : Fin 56) : raisingMatrixRat i a b = if DynkinType.e7MinusculeWeight b i = -1 ∧ a = (DynkinType.e7MinusculeReflection i) b then 1 else 0

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

@[simp]

theorem TauCeti.E7Minuscule.loweringMatrixRat_apply (i : Fin 7) (a b : Fin 56) : loweringMatrixRat i a b = if DynkinType.e7MinusculeWeight b i = 1 ∧ a = (DynkinType.e7MinusculeReflection i) b then 1 else 0

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

@[simp]

theorem TauCeti.E7Minuscule.cartanMatrixRat_apply (i : Fin 7) (a b : Fin 56) : cartanMatrixRat i a b = if a = b then ↑(DynkinType.e7MinusculeWeight a i) else 0

The rational Cartan matrix is diagonal with the minuscule weights on its diagonal.

theorem TauCeti.E7Minuscule.isSerreSystemRat : IsSerreSystem ℚ (CartanMatrix.E 7) cartanMatrixRat raisingMatrixRat loweringMatrixRat

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

theorem TauCeti.E7Minuscule.isSl2TripleRat (i : Fin 7) : IsSl2Triple (cartanMatrixRat i) (raisingMatrixRat i) (loweringMatrixRat i)

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

noncomputable def TauCeti.E7Minuscule.rationalSerreRepresentation : Matrix.ToLieAlgebra ℚ (CartanMatrix.E 7) →ₗ⁅ℚ⁆ Matrix (Fin 56) (Fin 56) ℚ

The rational 56-dimensional minuscule representation of the type-E₇ Serre presentation.

Equations

• TauCeti.E7Minuscule.rationalSerreRepresentation = TauCeti.serreLift TauCeti.E7Minuscule.isSerreSystemRat

@[simp]

theorem TauCeti.E7Minuscule.rationalSerreRepresentation_serreH (i : Fin 7) : rationalSerreRepresentation (serreH ℚ (CartanMatrix.E 7) i) = cartanMatrixRat i

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

@[simp]

theorem TauCeti.E7Minuscule.rationalSerreRepresentation_serreE (i : Fin 7) : rationalSerreRepresentation (serreE ℚ (CartanMatrix.E 7) i) = raisingMatrixRat i

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

@[simp]

theorem TauCeti.E7Minuscule.rationalSerreRepresentation_serreF (i : Fin 7) : rationalSerreRepresentation (serreF ℚ (CartanMatrix.E 7) i) = loweringMatrixRat i

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

The enveloping-algebra representation

noncomputable def TauCeti.E7Minuscule.rep : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 7)) →ₐ[ℚ] Module.End ℚ (Fin 56 → ℚ)

The rational minuscule representation extended to the universal enveloping algebra.

Equations

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

theorem TauCeti.E7Minuscule.rep_ι_apply (x : Matrix.ToLieAlgebra ℚ (CartanMatrix.E 7)) (v : Fin 56 → ℚ) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) x)) v = (rationalSerreRepresentation x).mulVec v

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

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

The represented positive and negative simple generators at a common type-E₇ node, together with the represented Cartan generator, form an sl₂ triple.

@[simp]

theorem TauCeti.E7Minuscule.raisingMatrixRat_pow_two (i : Fin 7) : raisingMatrixRat i ^ 2 = 0

Every rational minuscule raising matrix squares to zero.

@[simp]

theorem TauCeti.E7Minuscule.loweringMatrixRat_pow_two (i : Fin 7) : loweringMatrixRat i ^ 2 = 0

Every rational minuscule lowering matrix squares to zero.

theorem TauCeti.E7Minuscule.pow_two_rep_serreRootGenerator_eq_zero (k : Fin 7 ⊕ Fin 7) : rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 7) k)) ^ 2 = 0

Every simple-root generator acts with square zero in the rational minuscule representation.

theorem TauCeti.E7Minuscule.isNilpotent_rep_serreRootGenerator (k : Fin 7 ⊕ Fin 7) : IsNilpotent (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 7) k)))

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

The admissible coordinate lattice

def TauCeti.E7Minuscule.lattice : Submodule ℤ (Fin 56 → ℚ)

The coordinate ℤ-lattice in the rational minuscule module.

Equations

• TauCeti.E7Minuscule.lattice = TauCeti.coordinateLattice (Fin 56)

@[simp]

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

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

noncomputable def TauCeti.E7Minuscule.latticeBasis : Module.Basis (Fin 56) ℤ ↥lattice

The coordinate basis of the minuscule lattice.

Equations

• TauCeti.E7Minuscule.latticeBasis = TauCeti.coordinateLatticeBasis (Fin 56)

@[simp]

theorem TauCeti.E7Minuscule.coe_latticeBasis (a : Fin 56) : ↑(latticeBasis a) = Pi.single a 1

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

theorem TauCeti.E7Minuscule.rep_serreRootGenerator_apply_mem_lattice (k : Fin 7 ⊕ Fin 7) {v : Fin 56 → ℚ} (hv : v ∈ lattice) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 7) k))) v ∈ lattice

Every simple-root generator preserves the minuscule coordinate lattice.

theorem TauCeti.E7Minuscule.isCartanWeightVector_single (a : Fin 56) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.E 7)) rep (DynkinType.e7MinusculeWeight a) (Pi.single a 1)

Each coordinate basis vector has the corresponding minuscule weight for the Cartan generators.

theorem TauCeti.E7Minuscule.isCartanWeightVector_latticeBasis (a : Fin 56) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.E 7)) rep (DynkinType.e7MinusculeWeight a) ↑(latticeBasis a)

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

theorem TauCeti.E7Minuscule.rep_serreKostantForm_apply_mem_lattice {u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 7))} (hu : u ∈ serreKostantForm (CartanMatrix.E 7)) {v : Fin 56 → ℚ} (hv : v ∈ lattice) : (rep u) v ∈ lattice

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