Torus characters of the tripled type-D4 carrier in its named root datum

TauCeti.D4Tripled.groupScheme is the full-weight Chevalley carrier obtained from the twenty-four-dimensional representation V(ϖ₁) ⊕ V(ϖ₃) ⊕ V(ϖ₄) of the type-D₄ Serre presentation. Its eight numbered simple-root subgroups and rank-four split weight torus are explicit. The carrier's conjugation equation initially describes the root character as TauCeti.TypeDStd.rootGeneratorWeight 4, hence as a row of the type-D₄ Cartan matrix.

This file rewrites that equation against the uniform simply connected root datum used by downstream consumers. The identities TauCeti.TypeDStd.rootGeneratorWeight_inl_eq_root_simpleIndex and TauCeti.TypeDStd.rootGeneratorWeight_inr_eq_neg_root_simpleIndex identify the character of the i-th raising subgroup with

((DynkinType.D 4).simplyConnectedRootDatum ht).root
  ((DynkinType.D 4).simpleIndex ht i)

and the lowering character with its negative. The results below substitute these identities into the carrier's conjugation equations. They therefore certify that the tripled carrier and DynkinType.simplyConnectedRootDatum use the same Bourbaki numbering and character lattice.

This file does not assert reductivity, maximality of the weight torus, existence of all root subgroups, or an identification of the carrier with an independently defined algebraic group. It packages only the named simple-root pinning equations already justified by the construction.

Main results

• TauCeti.D4Tripled.weightTorus_conj_rootSubgroup_root_simpleIndex: conjugation by the weight torus on a positive simple-root subgroup is governed by the corresponding root of the uniform simply connected type-D₄ datum.
• TauCeti.D4Tripled.weightTorus_conj_rootSubgroup_neg_root_simpleIndex: the analogous equation for a negative simple root.
• TauCeti.D4Tripled.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex and TauCeti.D4Tripled.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex: the same equations on matrix-valued points.

References

• R. W. Carter, Simple Groups of Lie Type, Sections 4.4, 7.1, and 12.2.
• J. E. Humphreys, Linear Algebraic Groups, Sections 26--27.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IV.
• The interface follows TauCeti.Algebra.Lie.F4.ShortRoot.RootDatum and TauCeti.Algebra.Lie.E7.Minuscule.RootDatum.

Torus conjugation equations against the named simple roots

theorem TauCeti.D4Tripled.weightTorus_conj_rootSubgroup_root_simpleIndex (ht : (DynkinType.D 4).Valid) (i : 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 (Sum.inl i)).hom.hom * (CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (((DynkinType.D 4).simplyConnectedRootDatum ht).root ((DynkinType.D 4).simpleIndex ht i))) * u))) (rootSubgroup (Sum.inl i)).hom.hom

The torus conjugation equation at a named positive simple root. A point s of the split weight torus conjugates the raising-subgroup element of parameter u at node i to the same subgroup with parameter αᵢ(s)u, where αᵢ is the corresponding root of the uniform simply connected type-D₄ datum.

theorem TauCeti.D4Tripled.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (ht : (DynkinType.D 4).Valid) (i : 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 (Sum.inr i)).hom.hom * (CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom)⁻¹ = CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).symm (Multiplicative.ofAdd (↑(torusCharacter (SplitTorus.schemePointsMulEquiv s) (-((DynkinType.D 4).simplyConnectedRootDatum ht).root ((DynkinType.D 4).simpleIndex ht i))) * u))) (rootSubgroup (Sum.inr i)).hom.hom

The torus conjugation equation at a named negative simple root. A point s of the split weight torus conjugates the lowering-subgroup element of parameter u at node i to the same subgroup with parameter (-αᵢ)(s)u.

Torus conjugation equations on matrix-valued points

theorem TauCeti.D4Tripled.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex (ht : (DynkinType.D 4).Valid) (i : Fin 4) (A : Type v) [CommRing A] (s : Fin 4 → Aˣ) (u : Multiplicative A) : (weightTorusPoints A) s * (rootSubgroupPoints (Sum.inl i) A) u * ((weightTorusPoints A) s)⁻¹ = (rootSubgroupPoints (Sum.inl i) A) (Multiplicative.ofAdd (↑(torusCharacter s (((DynkinType.D 4).simplyConnectedRootDatum ht).root ((DynkinType.D 4).simpleIndex ht i))) * Multiplicative.toAdd u))

The pinning equation at a named positive simple root, on matrix-valued points. A point s of the split weight torus conjugates the raising-subgroup element of parameter u at node i to the same subgroup with parameter αᵢ(s)u.

theorem TauCeti.D4Tripled.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex (ht : (DynkinType.D 4).Valid) (i : Fin 4) (A : Type v) [CommRing A] (s : Fin 4 → Aˣ) (u : Multiplicative A) : (weightTorusPoints A) s * (rootSubgroupPoints (Sum.inr i) A) u * ((weightTorusPoints A) s)⁻¹ = (rootSubgroupPoints (Sum.inr i) A) (Multiplicative.ofAdd (↑(torusCharacter s (-((DynkinType.D 4).simplyConnectedRootDatum ht).root ((DynkinType.D 4).simpleIndex ht i))) * Multiplicative.toAdd u))

The pinning equation at a named negative simple root, on matrix-valued points. A point s of the split weight torus conjugates the lowering-subgroup element of parameter u at node i to the same subgroup with parameter (-αᵢ)(s)u.