Closed generators of the type-E7 minuscule carrier after base change

The integral type-E₇ minuscule carrier comes with fourteen numbered simple-root subgroups and a rank-seven weight torus. This file proves that their transported coordinate maps remain surjective after base change from ℤ to an arbitrary commutative ring. Contravariantly, the transported root subgroups and weight torus are closed immersions into the specialized carrier.

The resulting morphisms are the scheme-theoretic base changes of the integral pinning generators, not newly chosen subgroups in each fibre. No assertion is made that the carrier is smooth, reductive, or geometrically connected, nor that its weight torus is maximal.

Main declarations

• TauCeti.E7Minuscule.rootSubgroupToBaseChangeCoordinateMap_surjective: every transported numbered root-subgroup coordinate map is surjective.
• TauCeti.E7Minuscule.weightTorusToBaseChangeCoordinateMap_surjective: the transported weight-torus coordinate map is surjective.
• TauCeti.E7Minuscule.baseChangeRootSubgroup and TauCeti.E7Minuscule.baseChangeWeightTorus: the corresponding morphisms into the specialized carrier.
• TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroup: each numbered root subgroup as a bundled closed subgroup scheme.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1.
• J. C. Jantzen, Representations of Algebraic Groups, II.2.

Surjectivity of the transported coordinate maps

theorem TauCeti.E7Minuscule.rootSubgroupToBaseChangeCoordinateMap_surjective (A : Type u) [CommRing A] (k : Fin 7 ⊕ Fin 7) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupToBaseChangeCoordinateMap A k))

Every transported numbered type-E₇ root-subgroup coordinate map is surjective. Thus the simple-root copy of 𝔾ₐ remains scheme-theoretically closed after arbitrary base change from ℤ.

theorem TauCeti.E7Minuscule.weightTorusToBaseChangeCoordinateMap_surjective (A : Type u) [CommRing A] : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (weightTorusToBaseChangeCoordinateMap A))

The transported rank-seven weight-torus coordinate map is surjective. Thus the weight torus remains a closed split torus in every specialized carrier.

Scheme-theoretic closed generators

The current hopfSpec bridge requires the base ring and all coordinate rings to inhabit the same universe. The concrete pinning uses the finite index types Fin 7 and Fin 56, so its scheme-level packaging is correspondingly stated in the base universe.

@[reducible, inline]

noncomputable abbrev TauCeti.E7Minuscule.baseChangeGroupScheme (A : Type) [CommRing A] : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧A))

The type-E₇ minuscule carrier specialized to the commutative ring A, in its transported quotient presentation inside GL₅₆/A.

Equations

• TauCeti.E7Minuscule.baseChangeGroupScheme A = TauCeti.CommHopfAlgCat.quotientSpec (TauCeti.GeneralLinear.coordinateHopfAlgebra A 56) (TauCeti.E7Minuscule.baseChangeDefiningIdeal A)

noncomputable def TauCeti.E7Minuscule.baseChangeRootSubgroup (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : AdditiveGroup.groupScheme A ⟶ baseChangeGroupScheme A

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

Equations

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

instance TauCeti.E7Minuscule.isClosedImmersion_baseChangeRootSubgroup (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (baseChangeRootSubgroup A k).hom.hom)

Every transported numbered simple root subgroup is a closed immersion into the specialized type-E₇ minuscule carrier.

noncomputable def TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroup (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : ClosedSubgroupScheme (baseChangeGroupScheme A)

A transported numbered simple root subgroup as a closed subgroup scheme of the specialized type-E₇ minuscule carrier.

Equations

• TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroup A k = TauCeti.ClosedSubgroupScheme.mk (TauCeti.E7Minuscule.baseChangeRootSubgroup A k)

@[simp]

theorem TauCeti.E7Minuscule.coe_baseChangeRootSubgroupClosedSubgroup (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : ↑(baseChangeRootSubgroupClosedSubgroup A k) = CategoryTheory.Subobject.mk (baseChangeRootSubgroup A k)

The bundled closed root subgroup is represented by the transported root-subgroup morphism.

noncomputable def TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroupIso (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : CategoryTheory.Subobject.underlying.obj ↑(baseChangeRootSubgroupClosedSubgroup A k) ≅ AdditiveGroup.groupScheme A

The bundled transported root subgroup is canonically isomorphic to the additive group scheme.

Equations

• TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroupIso A k = TauCeti.ClosedSubgroupScheme.mkIso (TauCeti.E7Minuscule.baseChangeRootSubgroup A k)

@[simp]

theorem TauCeti.E7Minuscule.baseChangeRootSubgroupClosedSubgroupIso_inv_comp_arrow (A : Type) [CommRing A] (k : Fin 7 ⊕ Fin 7) : CategoryTheory.CategoryStruct.comp (baseChangeRootSubgroupClosedSubgroupIso A k).inv (↑(baseChangeRootSubgroupClosedSubgroup A k)).arrow = baseChangeRootSubgroup A k

The canonical parametrization of the bundled closed subgroup followed by its inclusion is the transported root-subgroup map.

noncomputable def TauCeti.E7Minuscule.baseChangeWeightTorus (A : Type) [CommRing A] : SplitTorus.groupScheme A (Fin 7) ⟶ baseChangeGroupScheme A

The transported rank-seven weight torus of the specialized type-E₇ minuscule carrier.

Equations

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

instance TauCeti.E7Minuscule.isClosedImmersion_baseChangeWeightTorus (A : Type) [CommRing A] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (baseChangeWeightTorus A).hom.hom)

The transported weight-torus morphism is a closed immersion into the specialized carrier.