The full-weight type-E7 minuscule carrier

This file feeds the explicit 56-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 affine group scheme over ℤ, explicitly cut out inside GL₅₆ by the common kernel of the represented simple root subgroups and weight torus.

The construction exposes the positive and negative simple root subgroups, the closed rank-seven weight torus, matrix-valued points over every commutative ring, and the scheme-level pinning equation. Every ingredient is explicit data from TauCeti.Algebra.Lie.E7.Minuscule.AdmissibleLattice; no carrier is selected from an existence theorem. Nothing here asserts reductivity, identifies the root datum of the carrier, or constructs root subgroups for nonsimple roots. Those remain type-E₇ tasks in Layer 9 of the ReductiveGroups roadmap before milestone L0 of the CFSGStatement roadmap can use this carrier.

Main definitions

• TauCeti.E7Minuscule.groupScheme: the full-weight minuscule toral closure in GL₅₆.
• TauCeti.E7Minuscule.rootSubgroup: its fourteen numbered simple root subgroups.
• TauCeti.E7Minuscule.weightTorus: its rank-seven split weight torus.
• TauCeti.E7Minuscule.points: its matrix-valued points over a commutative ring.

Main results

• TauCeti.E7Minuscule.isClosedImmersion_rootSubgroup: each numbered root subgroup is a closed copy of the additive group.
• TauCeti.E7Minuscule.isClosedImmersion_weightTorus: the minuscule weights make the split torus a closed subgroup of the carrier.
• TauCeti.E7Minuscule.coe_rootSubgroupPoints_inl and TauCeti.E7Minuscule.coe_rootSubgroupPoints_inr: the positive and negative simple-root matrices in the minuscule basis.
• TauCeti.E7Minuscule.weightTorus_conj_rootSubgroup: the scheme-level pinning equation.
• TauCeti.E7Minuscule.weightTorusPoints_conj_rootSubgroupPoints: the same equation on matrix-valued points.

References

The construction is the minuscule-representation form of the Chevalley--Demazure construction; see J. E. Humphreys, Linear Algebraic Groups, §26, and R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1. The type-E₇ minuscule representation and weight conventions follow N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI, and J. C. Jantzen, Representations of Algebraic Groups, II.2. The formal interface follows the parallel type-E₆ minuscule carrier in TauCetiProject/TauCeti#5246.

theorem TauCeti.E7Minuscule.rep_kostantForm_mem_lattice (u : UniversalEnvelopingAlgebra ℚ (Matrix.ToLieAlgebra ℚ (CartanMatrix.E 7))) (hu : u ∈ UniversalEnvelopingAlgebra.kostantForm (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7))) (v : Fin 56 → ℚ) (hv : v ∈ lattice.toAddSubgroup) : (rep u) v ∈ lattice.toAddSubgroup

The minuscule lattice is stable under the generic Kostant form generated by the Serre generators. This is the form required by the toral-closure construction.

Root characters and a nonzero root step

theorem TauCeti.E7Minuscule.lie_cartanGenerator_rootGenerator (k : Fin 7 ⊕ Fin 7) (j : Fin 7) : ⁅serreH ℚ (CartanMatrix.E 7) j, serreRootGenerator (CartanMatrix.E 7) k⁆ = ↑(DynkinType.E7.rootGeneratorWeight DynkinType.valid_E7 k j) • serreRootGenerator (CartanMatrix.E 7) k

The Cartan generators act on the numbered simple root generators through their root characters.

The pinned carrier

noncomputable def TauCeti.E7Minuscule.definingIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 56)

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

Equations

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

theorem TauCeti.E7Minuscule.definingIdeal_def : definingIdeal = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight

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

@[reducible, inline]

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

The full-weight type-E₇ minuscule carrier: the smallest closed subgroup scheme of GL₅₆ containing the represented simple root subgroups and the minuscule weight torus.

Equations

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

theorem TauCeti.E7Minuscule.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 56) definingIdeal

The quotient-spectrum presentation of the full-weight type-E₇ minuscule carrier.

noncomputable def TauCeti.E7Minuscule.carrierι : groupScheme ⟶ GeneralLinear.groupScheme ℤ 56

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.E7Minuscule.carrierι_def : carrierι = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight

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

instance TauCeti.E7Minuscule.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.E7Minuscule.rootSubgroup (k : Fin 7 ⊕ Fin 7) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme

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

Equations

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

theorem TauCeti.E7Minuscule.rootSubgroup_def (k : Fin 7 ⊕ Fin 7) : rootSubgroup k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight k

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

@[simp]

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

Including a numbered root subgroup into GL₅₆ recovers its represented Kostant root subgroup.

noncomputable def TauCeti.E7Minuscule.weightTorus : SplitTorus.groupScheme ℤ (Fin 7) ⟶ groupScheme

The rank-seven split weight torus in the type-E₇ minuscule carrier.

Equations

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

theorem TauCeti.E7Minuscule.weightTorus_def : weightTorus = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight

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

@[simp]

theorem TauCeti.E7Minuscule.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = GeneralLinear.weightTorus DynkinType.e7MinusculeWeight

Including the split weight torus into GL₅₆ recovers the diagonal torus of the minuscule weights.

theorem TauCeti.E7Minuscule.groupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 7 ⊕ Fin 7), 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₇ minuscule carrier agree when they agree on every numbered simple root subgroup and on the split weight torus.

theorem TauCeti.E7Minuscule.groupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec (CommRingCat.of ℤ)).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin 7 ⊕ Fin 7), 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.E7Minuscule.points (A : Type v) [CommRing A] : Subgroup (GL (Fin 56) 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.E7Minuscule.points_def (A : Type v) [CommRing A] : points A = GeneralLinear.hopfIdealPointsSubgroup 56 definingIdeal A

The points of the type-E₇ minuscule carrier are cut out by its defining Hopf ideal.

@[simp]

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

A matrix is a point of the type-E₇ minuscule carrier exactly when its associated convolution point kills the carrier's defining Hopf ideal.

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

The parametrized numbered simple root subgroup inside the type-E₇ carrier points.

Equations

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

@[simp]

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

A numbered simple-root point is the corresponding divided-power exponential matrix.

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

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

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

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

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

The split weight torus inside the type-E₇ minuscule carrier points.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.coe_weightTorusPoints (A : Type v) [CommRing A] (s : Fin 7 → Aˣ) : ↑((weightTorusPoints A) s) = (UniversalEnvelopingAlgebra.kostantTorusMatrix lattice.toAddSubgroup latticeBasis DynkinType.e7MinusculeWeight) s

A split-torus point is the diagonal matrix whose entries are the minuscule weight characters.

Closed subgroups and the pinning equation

theorem TauCeti.E7Minuscule.rootSubgroupCoordinateMap_surjective (k : Fin 7 ⊕ Fin 7) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (serreRootGenerator (CartanMatrix.E 7)) (serreH ℚ (CartanMatrix.E 7)) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.e7MinusculeWeight k))

The root-subgroup coordinate map remains surjective after adjoining the weight torus.

instance TauCeti.E7Minuscule.isClosedImmersion_rootSubgroup (k : Fin 7 ⊕ Fin 7) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (rootSubgroup k).hom.hom)

Every numbered simple root subgroup is a closed copy of the additive group.

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

The minuscule weights make the rank-seven split weight torus a closed immersion into the carrier.

@[simp]

theorem TauCeti.E7Minuscule.weightTorus_conj_rootSubgroup (k : Fin 7 ⊕ Fin 7) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec (CommRingCat.of A)).asOver (AlgebraicGeometry.Spec (CommRingCat.of ℤ)) ⟶ (SplitTorus.groupScheme ℤ (Fin 7)).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) (DynkinType.E7.rootGeneratorWeight DynkinType.valid_E7 k)) * u))) (rootSubgroup k).hom.hom

The scheme-level pinning equation: conjugation by the weight torus acts on each numbered simple root subgroup through the corresponding type-E₇ root character.

@[simp]

theorem TauCeti.E7Minuscule.weightTorusPoints_conj_rootSubgroupPoints (k : Fin 7 ⊕ Fin 7) (A : Type v) [CommRing A] (s : Fin 7 → Aˣ) (u : Multiplicative A) : (weightTorusPoints A) s * (rootSubgroupPoints k A) u * ((weightTorusPoints A) s)⁻¹ = (rootSubgroupPoints k A) (Multiplicative.ofAdd (↑(torusCharacter s (DynkinType.E7.rootGeneratorWeight DynkinType.valid_E7 k)) * Multiplicative.toAdd u))

The pinning equation on matrix-valued points: conjugation by a point s of the weight torus rescales the parameter of each numbered simple root subgroup by the corresponding type-E₇ root character evaluated at s.