The full-weight type-E6 minuscule carrier

This file feeds the explicit 27-dimensional type-E₆ minuscule representation, 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.

The root-subgroup characters are identified with the positive and negative simple roots of TauCeti.DynkinType.e6SimplyConnectedRootDatum. Since the minuscule weights span the entire character lattice, the represented split torus is a closed immersion. The scheme-level pinning equation records its conjugation action on every numbered root subgroup.

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.E6Minuscule.groupScheme: the minuscule Kostant toral-closure carrier over ℤ.
• TauCeti.E6Minuscule.rootSubgroup: its twelve numbered simple-root subgroup morphisms.
• TauCeti.E6Minuscule.weightTorus: its closed rank-six split torus.
• TauCeti.E6Minuscule.points: its matrix-valued points over a commutative ring.
• TauCeti.E6Minuscule.rootSubgroupPoints: its numbered root subgroups on matrix-valued points.
• TauCeti.E6Minuscule.coe_rootSubgroupPoints_inl and TauCeti.E6Minuscule.coe_rootSubgroupPoints_inr: their positive and negative simple-root matrices in the minuscule basis.
• TauCeti.E6Minuscule.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.
• The carrier API follows the formal templates in TauCeti.Algebra.Lie.SpecialLinear.StandardCarrier.Basic and TauCeti.Algebra.Lie.Symplectic.StandardCarrier.Scheme, specialized here using the type-E₆ minuscule representation, lattice, weights, and root characters.
• The simple-root matrix formulas follow the parallel calculation in TauCeti.Algebra.Lie.E7.Minuscule.Carrier.

The pinned carrier

noncomputable def TauCeti.E6Minuscule.definingIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 27)

The Hopf ideal cutting out the type-E₆ minuscule carrier inside GL₂₇.

Equations

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

theorem TauCeti.E6Minuscule.definingIdeal_def : definingIdeal = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight

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

@[reducible, inline]

noncomputable abbrev TauCeti.E6Minuscule.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The full-weight 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.E6Minuscule.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 27) definingIdeal

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

noncomputable def TauCeti.E6Minuscule.carrierι : groupScheme ⟶ GeneralLinear.groupScheme ℤ 27

The canonical inclusion of the type-E₆ minuscule carrier into GL₂₇.

Equations

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

theorem TauCeti.E6Minuscule.carrierι_def : carrierι = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight

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

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

The type-E₆ minuscule carrier is a closed subgroup scheme of GL₂₇.

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

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

Equations

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

theorem TauCeti.E6Minuscule.rootSubgroup_def (k : Fin 6 ⊕ Fin 6) : rootSubgroup k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight k

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

@[simp]

theorem TauCeti.E6Minuscule.rootSubgroup_comp_carrierι (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) carrierι = UniversalEnvelopingAlgebra.kostantRootSubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ k ⋯ (coordinateLatticeBasis (Fin 27))

Including a numbered root subgroup into GL₂₇ recovers its represented divided-power exponential subgroup.

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

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

Equations

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

theorem TauCeti.E6Minuscule.weightTorus_def : weightTorus = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight

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

@[simp]

theorem TauCeti.E6Minuscule.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = GeneralLinear.weightTorus weightTable.weight

Including the weight torus into GL₂₇ recovers the diagonal torus of the minuscule weights.

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

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

theorem TauCeti.E6Minuscule.groupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).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 type-E₆ carrier agree when they agree on its numbered root subgroups and represented split torus.

theorem TauCeti.E6Minuscule.groupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).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.E6Minuscule.points (A : Type v) [CommRing A] : Subgroup (GL (Fin 27) A)

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

Equations

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

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

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

@[simp]

theorem TauCeti.E6Minuscule.mem_points_iff (A : Type v) [CommRing A] (g : GL (Fin 27) A) : g ∈ points A ↔ ∀ x ∈ definingIdeal, ((GeneralLinear.pointsMulEquiv 27).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.E6Minuscule.rootSubgroupPoints (k : Fin 6 ⊕ Fin 6) (A : Type v) [CommRing A] : Multiplicative A →* ↥(points A)

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

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.coe_rootSubgroupPoints (k : Fin 6 ⊕ Fin 6) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑((rootSubgroupPoints k A) u) = (UniversalEnvelopingAlgebra.kostantRootSubgroupMatrix (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ k ⋯ (coordinateLatticeBasis (Fin 27))) (AdditiveGroup.gaPointsMulEquiv.symm u)

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

theorem TauCeti.E6Minuscule.coe_rootSubgroupPoints_inl (i : Fin 6) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints (Sum.inl i) A) u) = 1 + Multiplicative.toAdd u • (weightTable.raisingMatrix i).map Int.cast

A positive simple-root point has matrix 1 + uEᵢ in the minuscule basis.

theorem TauCeti.E6Minuscule.coe_rootSubgroupPoints_inr (i : Fin 6) (A : Type v) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints (Sum.inr i) A) u) = 1 + Multiplicative.toAdd u • (weightTable.loweringMatrix i).map Int.cast

A negative simple-root point has matrix 1 + uFᵢ in the minuscule basis.

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

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

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.coe_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 6 → Aˣ) : ↑((weightTorusPoints A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix (coordinateLattice (Fin 27)).toAddSubgroup (coordinateLatticeBasis (Fin 27)) weightTable.weight) s

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

The pinning equation

@[simp]

theorem TauCeti.E6Minuscule.weightTorus_conj_rootSubgroup (k : Fin 6 ⊕ Fin 6) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (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) (E6.rootGeneratorWeight k)) * u))) (rootSubgroup k).hom.hom

Conjugation by the minuscule weight torus acts on each numbered root subgroup through its positive or negative pinned simple-root character.