The tripled type-D4 carrier

This file feeds the explicit 24-dimensional type-D₄ representation V(ϖ₁) ⊕ V(ϖ₃) ⊕ V(ϖ₄), its admissible coordinate lattice, and its full set of weights into the Kostant toral-closure construction. The result is an explicit affine group scheme over ℤ, cut out inside GL₂₄ by the largest Hopf ideal killed by the eight numbered simple-root subgroups and the represented rank-four split torus, together with its matrix-valued points and the pinning equation on both.

The type-D₄ diagram carries three families of finite groups of Lie type, and the full-weight spin carrier TauCeti.TypeDSpinCarrier.groupScheme at rank four serves the untwisted and the graph-twisted ones. It cannot serve the triality-twisted family: triality permutes the three eight-dimensional representations of D₄, so neither the natural representation nor the full spin module is stable under it, while the tripled module is a full-weight module that is. On the twenty-four tripled weights triality acts by TauCeti.DynkinType.d4TripledWeight_d4TripledTrialityPerm_apply, the equivariance wt (π x) (σ i) = wt x i. That equivariance is the weight-level hypothesis of the numbered-symmetry construction on a Kostant toral-closure carrier; its remaining inputs, a linear automorphism of the module intertwining the Serre root generators along the permutation and acting monomially on the lattice basis, are supplied in TauCeti.Algebra.Lie.D4.Tripled.Triality, which builds the triality automorphism of the carrier.

The character by which the split torus rescales a numbered root subgroup is TauCeti.TypeDStd.rootGeneratorWeight, a row of the type-D₄ Cartan matrix, identified with the simple roots of TauCeti.DynkinType.simplyConnectedRootDatum at D 4 by TauCeti.TypeDStd.rootGeneratorWeight_inl_eq_root_simpleIndex; the Cartan action on the numbered root generators is TauCeti.TypeDStd.lie_serreH_serreRootGenerator, and the pinning equation below is stated against them.

No reductivity, smoothness, maximality of the torus, or identification of the carrier with the pinned simply connected group scheme of type D₄ is asserted here. Constructions on this carrier transfer to that pinned group only along such an identification.

Main declarations

• TauCeti.D4Tripled.groupScheme: the tripled Kostant toral-closure carrier over ℤ.
• TauCeti.D4Tripled.rootSubgroup: its eight numbered simple-root subgroup morphisms.
• TauCeti.D4Tripled.weightTorus: its closed rank-four split torus.
• TauCeti.D4Tripled.points: its matrix-valued points over a commutative ring.
• TauCeti.D4Tripled.rootSubgroupPoints and TauCeti.D4Tripled.weightTorusPoints: its numbered root subgroups and weight torus on matrix-valued points.
• TauCeti.D4Tripled.coe_rootSubgroupPoints_inl and TauCeti.D4Tripled.coe_rootSubgroupPoints_inr: a simple-root point of parameter u is the matrix 1 + uEᵢ or 1 + uFᵢ.
• TauCeti.D4Tripled.weightTorus_conj_rootSubgroup and TauCeti.D4Tripled.weightTorusPoints_conj_rootSubgroupPoints: the pinning equation on scheme points and on matrix-valued points.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• J. E. Humphreys, Linear Algebraic Groups, §26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1--2.
• R. W. Carter, Simple Groups of Lie Type, §12.2, for triality and the family it defines.
• The carrier API follows the formal template of TauCeti.Algebra.Lie.E6.Minuscule.GroupScheme, specialized here to the tripled type-D₄ representation, lattice, and weights.
• The symmetry-carrying full-weight design follows TauCeti.Algebra.Lie.E6.DoubledMinuscule.GroupScheme and its GraphAutomorphism module.
• The pinning section follows TauCeti.Algebra.Lie.Orthogonal.TypeD.SpinCarrier.Basic, and its named-simple-root equations follow TauCeti.Algebra.Lie.Symplectic.StandardCarrier.RootDatum.

The pinned carrier

noncomputable def TauCeti.D4Tripled.definingIdeal : HopfIdeal ℤ ↑(GeneralLinear.coordinateHopfAlgebra ℤ 24)

The Hopf ideal cutting out the tripled type-D₄ carrier inside GL₂₄.

Equations

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

theorem TauCeti.D4Tripled.definingIdeal_def : definingIdeal = UniversalEnvelopingAlgebra.kostantToralDefiningIdeal (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight

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

@[reducible, inline]

noncomputable abbrev TauCeti.D4Tripled.groupScheme : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧ℤ))

The tripled type-D₄ carrier over ℤ, obtained as the smallest closed subgroup scheme of GL₂₄ containing the represented numbered root subgroups and weight torus.

Equations

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

theorem TauCeti.D4Tripled.groupScheme_def : groupScheme = CommHopfAlgCat.quotientSpec (GeneralLinear.coordinateHopfAlgebra ℤ 24) definingIdeal

The quotient-spectrum presentation of the tripled type-D₄ carrier.

noncomputable def TauCeti.D4Tripled.carrierι : groupScheme ⟶ GeneralLinear.groupScheme ℤ 24

The canonical inclusion of the tripled type-D₄ carrier into GL₂₄.

Equations

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

theorem TauCeti.D4Tripled.carrierι_def : carrierι = UniversalEnvelopingAlgebra.kostantToralGroupSchemeι (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight

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

instance TauCeti.D4Tripled.isClosedImmersion_carrierι : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left carrierι.hom.hom)

The tripled type-D₄ carrier is a closed subgroup scheme of GL₂₄.

noncomputable def TauCeti.D4Tripled.rootSubgroup (k : Fin 4 ⊕ Fin 4) : AdditiveGroup.groupScheme ℤ ⟶ groupScheme

A positive or negative numbered simple-root subgroup of the tripled type-D₄ carrier.

Equations

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

theorem TauCeti.D4Tripled.rootSubgroup_def (k : Fin 4 ⊕ Fin 4) : rootSubgroup k = UniversalEnvelopingAlgebra.kostantRootSubgroupToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight k

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

@[simp]

theorem TauCeti.D4Tripled.rootSubgroup_comp_carrierι (k : Fin 4 ⊕ Fin 4) : CategoryTheory.CategoryStruct.comp (rootSubgroup k) carrierι = UniversalEnvelopingAlgebra.kostantRootSubgroup (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice k ⋯ latticeBasis

Including a numbered root subgroup into GL₂₄ recovers its represented divided-power exponential subgroup.

noncomputable def TauCeti.D4Tripled.weightTorus : SplitTorus.groupScheme ℤ (Fin 4) ⟶ groupScheme

The represented rank-four split weight torus in the tripled type-D₄ carrier.

Equations

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

theorem TauCeti.D4Tripled.weightTorus_def : weightTorus = UniversalEnvelopingAlgebra.kostantWeightTorusToToral (serreRootGenerator weightTable.cartanMatrix) (serreH ℚ weightTable.cartanMatrix) rep lattice.toAddSubgroup rep_kostantForm_mem_lattice isNilpotent_rep_serreRootGenerator latticeBasis DynkinType.d4TripledWeight

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

@[simp]

theorem TauCeti.D4Tripled.weightTorus_comp_carrierι : CategoryTheory.CategoryStruct.comp weightTorus carrierι = GeneralLinear.weightTorus DynkinType.d4TripledWeight

Including the weight torus into GL₂₄ recovers the diagonal torus of the tripled weights.

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

The tripled weights make the represented split torus a closed subgroup scheme of the carrier.

theorem TauCeti.D4Tripled.groupScheme_hom_ext {Y : CommHopfAlgCat ℤ} (f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)) (hroot : ∀ (k : Fin 4 ⊕ Fin 4), 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 tripled type-D₄ carrier agree when they agree on its numbered root subgroups and represented split torus.

theorem TauCeti.D4Tripled.groupScheme_hom_ext_iff {Y : CommHopfAlgCat ℤ} {f g : groupScheme ⟶ (AlgebraicGeometry.hopfSpec ↧ℤ).obj (Opposite.op Y)} : f = g ↔ (∀ (k : Fin 4 ⊕ Fin 4), 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.D4Tripled.points (A : Type v) [CommRing A] : Subgroup (GL (Fin 24) A)

The matrix-valued points of the tripled type-D₄ carrier.

Equations

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

theorem TauCeti.D4Tripled.points_def (A : Type v) [CommRing A] : points A = GeneralLinear.hopfIdealPointsSubgroup 24 definingIdeal A

The carrier points are exactly the invertible matrices cut out by the defining Hopf ideal.

@[simp]

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

A matrix is a carrier point exactly when its associated convolution point kills the defining Hopf ideal.

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

The parametrized numbered root subgroup inside the tripled type-D₄ carrier points.

Equations

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

@[simp]

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

A numbered root-subgroup point is its represented divided-power exponential matrix.

theorem TauCeti.D4Tripled.coe_rootSubgroupPoints_inl (i : Fin 4) (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 tripled weight basis.

theorem TauCeti.D4Tripled.coe_rootSubgroupPoints_inr (i : Fin 4) (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 tripled weight basis.

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

The split weight torus on matrix-valued points of the tripled type-D₄ carrier.

Equations

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

@[simp]

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

A tripled weight-torus point is the diagonal matrix obtained by evaluating each weight.

The pinning equation

theorem TauCeti.D4Tripled.lie_serreH_serreRootGenerator (k : Fin 4 ⊕ Fin 4) (j : Fin 4) : ⁅serreH ℚ weightTable.cartanMatrix j, serreRootGenerator weightTable.cartanMatrix k⁆ = ↑(TypeDStd.rootGeneratorWeight 4 k j) • serreRootGenerator weightTable.cartanMatrix k

The numbered Serre root generators of the tripled type-D₄ presentation are Cartan weight vectors with weight TauCeti.TypeDStd.rootGeneratorWeight: the Cartan matrix of the tripled weight table is the type-D₄ Cartan matrix.

@[simp]

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

Conjugation by the tripled weight torus acts on each numbered root subgroup through its positive or negative simple-root character, on matrix-valued points. A torus point s carries the root-subgroup point of parameter u to the one of parameter α_k(s) u, where the character α_k is TauCeti.TypeDStd.rootGeneratorWeight, the positive or negative k-th simple root of TauCeti.DynkinType.simplyConnectedRootDatum at D 4.

@[simp]

theorem TauCeti.D4Tripled.weightTorus_conj_rootSubgroup (k : Fin 4 ⊕ Fin 4) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 4)).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) (TypeDStd.rootGeneratorWeight 4 k)) * u))) (rootSubgroup k).hom.hom

Conjugation by the tripled weight torus acts on each numbered root subgroup through its positive or negative simple-root character, on scheme points.