The full-weight doubled type-E6 minuscule carrier

This file feeds the explicit 54-dimensional type-E₆ representation V(ϖ₁) ⊕ V(ϖ₆), its admissible coordinate lattice, and its full set of weights into the Kostant toral-closure construction. The result is an explicit affine group scheme over ℤ, cut out inside GL₅₄ by the largest Hopf ideal killed by the twelve numbered simple-root subgroups and the represented rank-six split torus, together with its matrix-valued points and the scheme-level pinning equation.

The 27-dimensional carrier TauCeti.E6Minuscule.groupScheme already realizes the same root datum in the same numbering, and the branch E₆(q) of the classification list is built on it. What the doubled carrier adds is the index set. The nontrivial symmetry of the E₆ diagram exchanges V(ϖ₁) with V(ϖ₆), so it does not permute the twenty-seven minuscule weights, which is what TauCeti.DynkinType.e6MinusculeWeight_comp_graphPermE6_notMem_range records; on the fifty-four doubled weights it does, by TauCeti.DynkinType.e6DoubledMinusculeWeight_e6DoubledMinusculeGraphPerm, which is the equivariance wt (π x) i = wt x (γ i) under which a numbered permutation of the coordinates extends to an automorphism of a Kostant toral-closure carrier. This carrier is therefore the one on which the E₆ graph automorphism can be realized. That realization is not performed here, and no declaration below mentions the diagram symmetry.

The generic construction indexes its lattice basis and its weight family by Fin n, while the representation is indexed by the block set Fin 27 ⊕ Fin 27, so matrixIndexEquiv fixes the order in which the two blocks are laid out along the fifty-four matrix coordinates, and matrixBasis and matrixWeight are the basis and weight family read in that order. Every declaration below is stated in the resulting Fin 54 coordinates.

The root characters are not redefined: TauCeti.E6Minuscule.rootGeneratorWeight and TauCeti.E6Minuscule.lie_serreH_rootGenerator are statements about the type-E₆ Serre algebra alone, with no reference to a representation of it, so the pinning equation below is stated and proved against them.

No reductivity, smoothness, maximality of the torus, or identification of the carrier's root datum is asserted here. Those are subsequent steps in the pinned Chevalley--Demazure construction.

Main declarations

• TauCeti.E6DoubledMinuscule.matrixBasis and TauCeti.E6DoubledMinuscule.matrixWeight: the admissible lattice basis and the weight family in the fifty-four matrix coordinates.
• TauCeti.E6DoubledMinuscule.groupScheme: the doubled minuscule Kostant toral-closure carrier over ℤ.
• TauCeti.E6DoubledMinuscule.rootSubgroup: its twelve numbered simple-root subgroup morphisms.
• TauCeti.E6DoubledMinuscule.weightTorus: its closed rank-six split torus.
• TauCeti.E6DoubledMinuscule.points: its matrix-valued points over a commutative ring.
• TauCeti.E6DoubledMinuscule.rootSubgroupPoints: its numbered root subgroups on matrix-valued points.
• TauCeti.E6DoubledMinuscule.weightTorus_conj_rootSubgroup: the scheme-level pinning equation.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.
• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• R. W. Carter, Simple Groups of Lie Type, §12.2, for the doubled minuscule realization and the diagram symmetry it is built to carry.
• The carrier API follows the formal template of TauCeti.Algebra.Lie.E6.Minuscule.GroupScheme, specialized here to the doubled minuscule representation, lattice, and weights.

Roadmap

This is a type-E₆ instance of "The Chevalley--Demazure construction" and "Root subgroup maps" in Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md: an explicitly constructed group scheme over ℤ with its numbered root subgroup maps and the equations pinning them against a split torus. It does not close that layer on this diagram, which still owes the reductivity, the maximality of the torus, the identification of the carrier's root datum with TauCeti.DynkinType.simplyConnectedRootDatum at E₆, and the pinning datum itself.

The fifty-four matrix coordinates

def TauCeti.E6DoubledMinuscule.matrixIndexEquiv : Fin 27 ⊕ Fin 27 ≃ Fin 54

The order in which the two minuscule blocks are laid out along the matrix coordinates of the doubled carrier: finSumFinEquiv after the numeral identification 27 + 27 = 54, so that the twenty-seven coordinates of V(ϖ₁) come first and the twenty-seven coordinates of V(ϖ₆) after them.

Equations

• TauCeti.E6DoubledMinuscule.matrixIndexEquiv = finSumFinEquiv.trans (finCongr TauCeti.E6DoubledMinuscule.matrixIndexEquiv._proof_1✝)

@[simp]

theorem TauCeti.E6DoubledMinuscule.val_matrixIndexEquiv_inl (a : Fin 27) : ↑(matrixIndexEquiv (Sum.inl a)) = ↑a

The V(ϖ₁) block occupies the first twenty-seven matrix coordinates.

@[simp]

theorem TauCeti.E6DoubledMinuscule.val_matrixIndexEquiv_inr (a : Fin 27) : ↑(matrixIndexEquiv (Sum.inr a)) = 27 + ↑a

The V(ϖ₆) block occupies the last twenty-seven matrix coordinates.

noncomputable def TauCeti.E6DoubledMinuscule.matrixBasis : Module.Basis (Fin 54) ℤ ↥lattice

The admissible doubled minuscule lattice basis, read in the fifty-four matrix coordinates.

Equations

• TauCeti.E6DoubledMinuscule.matrixBasis = TauCeti.E6DoubledMinuscule.latticeBasis.reindex TauCeti.E6DoubledMinuscule.matrixIndexEquiv

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixBasis_apply (a : Fin 54) : matrixBasis a = latticeBasis (matrixIndexEquiv.symm a)

The matrix-coordinate basis vector at a is the block-coordinate one at the block index that matrixIndexEquiv places at a.

def TauCeti.E6DoubledMinuscule.matrixWeight : Fin 54 → Fin 6 → ℤ

The fifty-four weights of V(ϖ₁) ⊕ V(ϖ₆), read in the fifty-four matrix coordinates.

Equations

• TauCeti.E6DoubledMinuscule.matrixWeight = TauCeti.DynkinType.e6DoubledMinusculeWeight ∘ ⇑TauCeti.E6DoubledMinuscule.matrixIndexEquiv.symm

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixWeight_apply (a : Fin 54) : matrixWeight a = DynkinType.e6DoubledMinusculeWeight (matrixIndexEquiv.symm a)

The weight at the matrix coordinate a is the doubled minuscule weight at the block index that matrixIndexEquiv places at a.

theorem TauCeti.E6DoubledMinuscule.isCartanWeightVector_matrixBasis (a : Fin 54) : UniversalEnvelopingAlgebra.IsCartanWeightVector (serreH ℚ (CartanMatrix.E 6).transpose) rep (matrixWeight a) ↑(matrixBasis a)

Every matrix-coordinate basis vector has its named Cartan weight.

theorem TauCeti.E6DoubledMinuscule.span_range_matrixWeight_eq_top : Submodule.span ℤ (Set.range matrixWeight) = ⊤

The doubled minuscule weights span the full type-E₆ character lattice. Reordering the weight family along matrixIndexEquiv does not change its range, so this is TauCeti.DynkinType.span_range_e6DoubledMinusculeWeight_eq_top.

theorem TauCeti.E6DoubledMinuscule.rep_kostantForm_mem_lattice (u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 6).transpose)) : u ∈ UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) → ∀ v ∈ lattice.toAddSubgroup, (rep u) v ∈ lattice.toAddSubgroup

The doubled minuscule coordinate lattice is stable under the Kostant ℤ-form of the type-E₆ Serre algebra. This is TauCeti.E6DoubledMinuscule.rep_serreKostantForm_mem_lattice in the shape the generic toral-closure construction consumes it, with the Serre Kostant form unfolded to the Kostant form of the numbered root and Cartan generators.

The pinned carrier

noncomputable def TauCeti.E6DoubledMinuscule.definingIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 54)

The Hopf ideal cutting out the doubled type-E₆ minuscule carrier inside GL₅₄.

Equations

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

theorem TauCeti.E6DoubledMinuscule.definingIdeal_def : definingIdeal = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight

The defining ideal is the ideal supplied by the generic Kostant toral-closure construction.

@[reducible, inline]

noncomputable abbrev TauCeti.E6DoubledMinuscule.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec (CommRingCat.of ℤ)))

The full-weight doubled type-E₆ minuscule carrier over ℤ, obtained as the smallest closed subgroup scheme of GL₅₄ containing the represented numbered root subgroups and weight torus.

Equations

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

theorem TauCeti.E6DoubledMinuscule.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 54) definingIdeal

The quotient-spectrum presentation of the doubled type-E₆ minuscule carrier.

noncomputable def TauCeti.E6DoubledMinuscule.carrierι : groupScheme ⟶ GeneralLinear.groupScheme ℤ 54

The canonical inclusion of the doubled type-E₆ minuscule carrier into GL₅₄.

Equations

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

theorem TauCeti.E6DoubledMinuscule.carrierι_def : carrierι = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight

The carrier inclusion is the generic Kostant toral-closure inclusion.

instance TauCeti.E6DoubledMinuscule.isClosedImmersion_carrierι : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left carrierι.hom.hom)

The doubled type-E₆ minuscule carrier is a closed subgroup scheme of GL₅₄.

noncomputable def TauCeti.E6DoubledMinuscule.rootSubgroup (k : Fin 6 ⊕ Fin 6) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme

A positive or negative numbered simple-root subgroup of the doubled type-E₆ carrier.

Equations

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

theorem TauCeti.E6DoubledMinuscule.rootSubgroup_def (k : Fin 6 ⊕ Fin 6) : rootSubgroup k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight k

The root subgroup is the one supplied by the generic Kostant toral-closure construction.

@[simp]

theorem TauCeti.E6DoubledMinuscule.rootSubgroup_comp_carrierι (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) carrierι = UniversalEnvelopingAlgebra.kostantRootSubgroup (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ matrixBasis

Including a numbered root subgroup into GL₅₄ recovers its represented divided-power exponential subgroup.

noncomputable def TauCeti.E6DoubledMinuscule.weightTorus : SplitTorus.groupScheme ℤ (Fin 6) ⟶ groupScheme

The represented rank-six split weight torus in the doubled type-E₆ carrier.

Equations

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

theorem TauCeti.E6DoubledMinuscule.weightTorus_def : weightTorus = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight

The weight torus is the one supplied by the generic Kostant toral-closure construction.

@[simp]

theorem TauCeti.E6DoubledMinuscule.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = GeneralLinear.weightTorus matrixWeight

Including the weight torus into GL₅₄ recovers the diagonal torus of the doubled minuscule weights.

instance TauCeti.E6DoubledMinuscule.isClosedImmersion_weightTorus : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left weightTorus.hom.hom)

The doubled minuscule weights make the represented split torus a closed subgroup scheme of the carrier.

theorem TauCeti.E6DoubledMinuscule.groupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 6 ⊕ Fin 6), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) (htorus : CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g) : f = g

Two morphisms out of the doubled type-E₆ carrier agree when they agree on its numbered root subgroups and represented split torus.

theorem TauCeti.E6DoubledMinuscule.groupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin 6 ⊕ Fin 6), CategoryTheory.CategoryStruct.comp (rootSubgroup k) f = CategoryTheory.CategoryStruct.comp (rootSubgroup k) g) ∧ CategoryTheory.CategoryStruct.comp weightTorus f = CategoryTheory.CategoryStruct.comp weightTorus g

Matrix-valued points

noncomputable def TauCeti.E6DoubledMinuscule.points (A : Type v) [CommRing A] : Subgroup (GL (Fin 54) A)

The matrix-valued points of the doubled type-E₆ minuscule carrier.

Equations

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

theorem TauCeti.E6DoubledMinuscule.points_def (A : Type v) [CommRing A] : points A = GeneralLinear.hopfIdealPointsSubgroup 54 definingIdeal A

The carrier points are exactly the invertible matrices cut out by the defining Hopf ideal.

@[simp]

theorem TauCeti.E6DoubledMinuscule.mem_points_iff (A : Type v) [CommRing A] (g : GL (Fin 54) A) : g ∈ points A ↔ ∀ x ∈ definingIdeal, ((GeneralLinear.pointsMulEquiv 54).symm g).ofConv x = 0

A matrix is a carrier point exactly when its associated convolution point kills the defining Hopf ideal.

noncomputable def TauCeti.E6DoubledMinuscule.rootSubgroupPoints (k : Fin 6 ⊕ Fin 6) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points A)

The parametrized numbered root subgroup inside the doubled type-E₆ carrier points.

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.coe_rootSubgroupPoints (k : Fin 6 ⊕ Fin 6) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints k A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ matrixBasis) (AdditiveGroup.gaPointsMulEquiv.symm u)

A numbered root-subgroup point is its represented divided-power exponential matrix.

noncomputable def TauCeti.E6DoubledMinuscule.weightTorusPoints (A : Type v) [CommRing A] : (Fin 6 → Aˣ) →* ↥(points A)

The split weight torus on matrix-valued points of the doubled type-E₆ carrier.

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.coe_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 6 → Aˣ) : ↑((weightTorusPoints A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix lattice.toAddSubgroup matrixBasis matrixWeight) s

A doubled minuscule weight-torus point is the diagonal matrix obtained by evaluating each weight.

The pinning equation

@[simp]

theorem TauCeti.E6DoubledMinuscule.weightTorus_conj_rootSubgroup (k : Fin 6 ⊕ Fin 6) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of ℤ)) ⟶ (SplitTorus.groupScheme ℤ (Fin 6)).X) (u : A) : CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.groupSchemePointMulEquiv A) (AdditiveGroup.gaPointsMulEquiv.symm (Multiplicative.ofAdd u))) (rootSubgroup k).hom.hom * (CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (E6Minuscule.rootGeneratorWeight k)) * u))) (rootSubgroup k).hom.hom

Conjugation by the doubled minuscule weight torus acts on each numbered root subgroup through its positive or negative pinned simple-root character. The character is TauCeti.E6Minuscule.rootGeneratorWeight, which reads a row of the type-E₆ Cartan matrix and mentions no representation, so it is the same one the 27-dimensional carrier is pinned by.