Closed root subgroups of the type-E6 minuscule carrier

The twelve numbered raising and lowering maps into TauCeti.E6Minuscule.groupScheme are closed copies of the additive group scheme. For every Bourbaki node, one explicit edge in the minuscule weight graph recovers the root-subgroup parameter as a matrix coordinate. The raising operator carries the basis vector at the negative end of this edge to the basis vector at its positive end with coefficient one; the lowering operator traverses the same edge in reverse.

The generic Kostant root-subgroup construction turns this unit-coefficient basis step into a surjective map from the carrier's coordinate Hopf algebra to the coordinate algebra of 𝔾ₐ. Consequently each numbered root-subgroup morphism is a closed immersion. Its scheme-theoretic image is bundled below as a closed subgroup canonically isomorphic to 𝔾ₐ.

This supplies the closed-root-subgroup component of a pinning for the explicit full-weight type-E₆ carrier in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. That carrier is consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md. No reductivity, Borel, finiteness, or simplicity statement is made here.

Main declarations

• TauCeti.E6Minuscule.rootSubgroupCoordinateMap_surjective: every numbered root-subgroup coordinate map is surjective.
• TauCeti.E6Minuscule.isClosedImmersion_rootSubgroup: every numbered root-subgroup morphism is a closed immersion.
• TauCeti.E6Minuscule.rootSubgroupClosedSubgroup: its image as a closed subgroup scheme.
• TauCeti.E6Minuscule.rootSubgroupClosedSubgroupIso: the canonical isomorphism of that image with the additive group 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.

A unit-coefficient edge at every simple root

Closed root-subgroup morphisms

theorem TauCeti.E6Minuscule.rootSubgroupCoordinateMap_surjective (k : Fin 6 ⊕ Fin 6) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) weightTable.rep (coordinateLattice (Fin 27)).toAddSubgroup ⋯ ⋯ (coordinateLatticeBasis (Fin 27)) weightTable.weight k))

The coordinate morphism of every numbered type-E₆ minuscule root subgroup is surjective. The selected minuscule-weight edge has coefficient one, so one matrix coordinate recovers the additive parameter.

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

Every numbered root-subgroup map into the type-E₆ minuscule carrier is a closed immersion. Thus its scheme-theoretic image is a closed copy of 𝔾ₐ, as required of the root subgroups in a pinning.

theorem TauCeti.E6Minuscule.mono_rootSubgroup (k : Fin 6 ⊕ Fin 6) : CategoryTheory.Mono (rootSubgroup k)

Every numbered root-subgroup map into the type-E₆ minuscule carrier is a monomorphism.

noncomputable def TauCeti.E6Minuscule.rootSubgroupClosedSubgroup (k : Fin 6 ⊕ Fin 6) : ClosedSubgroupScheme groupScheme

A numbered type-E₆ minuscule root subgroup as a closed subgroup scheme of the carrier.

Equations

• TauCeti.E6Minuscule.rootSubgroupClosedSubgroup k = TauCeti.ClosedSubgroupScheme.mk (TauCeti.E6Minuscule.rootSubgroup k)

@[simp]

theorem TauCeti.E6Minuscule.coe_rootSubgroupClosedSubgroup (k : Fin 6 ⊕ Fin 6) : ↑(rootSubgroupClosedSubgroup k) = CategoryTheory.Subobject.mk (rootSubgroup k)

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

noncomputable def TauCeti.E6Minuscule.rootSubgroupClosedSubgroupIso (k : Fin 6 ⊕ Fin 6) : CategoryTheory.Subobject.underlying.obj ↑(rootSubgroupClosedSubgroup k) ≅ AdditiveGroup.groupScheme ℤ

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

Equations

• TauCeti.E6Minuscule.rootSubgroupClosedSubgroupIso k = TauCeti.ClosedSubgroupScheme.mkIso (TauCeti.E6Minuscule.rootSubgroup k)

@[simp]

theorem TauCeti.E6Minuscule.rootSubgroupClosedSubgroupIso_inv_comp_arrow (k : Fin 6 ⊕ Fin 6) : CategoryTheory.CategoryStruct.comp (rootSubgroupClosedSubgroupIso k).inv (↑(rootSubgroupClosedSubgroup k)).arrow = rootSubgroup k

The canonical parametrization of the bundled closed subgroup followed by its inclusion is the numbered type-E₆ root-subgroup map.