Closed root subgroups of the doubled type-E6 minuscule carrier

The twelve numbered raising and lowering maps into TauCeti.E6DoubledMinuscule.groupScheme are closed copies of the additive group scheme. For every Bourbaki node one explicit edge of 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 the edge to the basis vector at its positive end with coefficient one, and the lowering operator traverses the same edge in reverse.

The edge is chosen inside the first of the two blocks. The doubled carrier is built from V(ϖ₁) ⊕ V(ϖ₆), and TauCeti.E6DoubledMinuscule.summandSign records that the structure constants of the second block are the negatives of those of the first, so an edge there would carry the coefficient -1. Both coefficients are units, so either block would do; taking the first keeps the selected edge the one the 27-dimensional carrier already uses in TauCeti/Algebra/Lie/E6/Minuscule/ClosedRootSubgroup.lean, and the surjectivity a closed immersion needs only asks for one unit-coefficient edge per node.

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

Nothing here asserts reductivity, that the carrier's weight torus is maximal, that the carrier is a pinned Chevalley--Demazure group scheme, or that the E₆ diagram symmetry acts on it.

Main declarations

• TauCeti.E6DoubledMinuscule.rootSubgroupCoordinateMap_surjective: every numbered root-subgroup coordinate map is surjective.
• TauCeti.E6DoubledMinuscule.isClosedImmersion_rootSubgroup: every numbered root-subgroup morphism is a closed immersion.
• TauCeti.E6DoubledMinuscule.rootSubgroupClosedSubgroup: its image as a closed subgroup scheme.
• TauCeti.E6DoubledMinuscule.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 12.2.
• J. C. Jantzen, Representations of Algebraic Groups, II.2.
• The declaration order and proof organization follow TauCeti/Algebra/Lie/E6/Minuscule/ClosedRootSubgroup.lean, the same argument on the 27-dimensional minuscule carrier.

Roadmap

This supplies the closed-root-subgroup component of a pinning for the explicit full-weight doubled type-E₆ carrier, in the "Pinnings" and "Root subgroup maps" targets of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. That carrier is the one the graph-twisted family ²E₆(q) of milestone L0 of TauCetiRoadmap/CFSGStatement/README.md needs, the E₆ diagram symmetry not acting on the 27-dimensional one.

A unit-coefficient edge at every simple root

Closed root-subgroup morphisms

theorem TauCeti.E6DoubledMinuscule.rootSubgroupCoordinateMap_surjective (k : Fin 6 ⊕ Fin 6) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (UniversalEnvelopingAlgebra.kostantRootSubgroupToralCoordinateMap (serreRootGenerator (CartanMatrix.E 6).transpose) (serreH ℚ (CartanMatrix.E 6).transpose) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator matrixBasis matrixWeight k))

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

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

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

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

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

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

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

Equations

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

@[simp]

theorem TauCeti.E6DoubledMinuscule.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.E6DoubledMinuscule.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.E6DoubledMinuscule.rootSubgroupClosedSubgroupIso k = TauCeti.ClosedSubgroupScheme.mkIso (TauCeti.E6DoubledMinuscule.rootSubgroup k)

@[simp]

theorem TauCeti.E6DoubledMinuscule.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 doubled type-E₆ root-subgroup map.