Closed root subgroups of the tripled type-D4 carrier

Each of the eight numbered root-subgroup maps into the tripled type-D₄ carrier is a closed immersion over ℤ. Its image is therefore a closed subgroup scheme canonically isomorphic to the additive group scheme, as required for the root subgroups in a pinning.

For each simple root, a tripled weight has simple-coroot coordinate -1. The raising operator sends its basis vector to the reflected basis vector with coefficient one, and the lowering operator reverses this edge. The represented generators square to zero, so one matrix coordinate of each root subgroup recovers its additive parameter. The generic Kostant root-step criterion then gives surjectivity of the coordinate maps. This also proves surjectivity of the transported root-subgroup coordinate maps over every commutative base ring.

Main declarations

• TauCeti.D4Tripled.rootSubgroupIntegralCoordinateMap_surjective: surjectivity over ℤ.
• TauCeti.D4Tripled.rootSubgroupToBaseChangeCoordinateMap_surjective: surjectivity after arbitrary base change.
• TauCeti.D4Tripled.isClosedImmersion_rootSubgroup: every numbered root map is closed.
• TauCeti.D4Tripled.rootSubgroupClosedSubgroupIso: its closed image is the additive group.

References

• J. E. Humphreys, Linear Algebraic Groups, §26.
• R. W. Carter, Simple Groups of Lie Type, §§4.4 and 12.2.
• The root-step argument and closed-subgroup packaging follow TauCeti.Algebra.Lie.E6.DoubledMinuscule.ClosedRootSubgroup, using the generic minuscule representation API for the tripled weight table.

theorem TauCeti.D4Tripled.rootSubgroupIntegralCoordinateMap_surjective (k : Fin 4 ⊕ Fin 4) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupIntegralCoordinateMap k))

Every numbered root-subgroup coordinate map of the tripled carrier is surjective over ℤ. Thus the additive parameter is a regular function on its scheme-theoretic image.

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

Every numbered root-subgroup map into the tripled type-D₄ carrier is a closed immersion.

theorem TauCeti.D4Tripled.mono_rootSubgroup (k : Fin 4 ⊕ Fin 4) : CategoryTheory.Mono (rootSubgroup k)

Every numbered root-subgroup map into the tripled type-D₄ carrier is a monomorphism.

theorem TauCeti.D4Tripled.rootSubgroupToBaseChangeCoordinateMap_surjective (A : Type u_1) [CommRing A] (k : Fin 4 ⊕ Fin 4) : Function.Surjective ⇑(CommHopfAlgCat.Hom.hom (rootSubgroupToBaseChangeCoordinateMap A k))

Surjectivity of the numbered root-subgroup coordinate maps persists over every commutative base ring, in the transported quotient presentation of the carrier.

noncomputable def TauCeti.D4Tripled.rootSubgroupClosedSubgroup (k : Fin 4 ⊕ Fin 4) : ClosedSubgroupScheme groupScheme

A numbered root subgroup as a closed subgroup scheme of the tripled type-D₄ carrier.

Equations

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

@[simp]

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

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

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

Each closed root subgroup is canonically isomorphic to the additive group scheme over ℤ.

Equations

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

@[simp]

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

The parametrization of the closed image followed by its inclusion recovers the root map.