Torus characters of the type-G₂ short-root carrier in its named root datum

TauCeti.G2ShortRoot.IntegralToralClosure.groupScheme is the integral toral closure of the seven-dimensional short-root representation of the type-G₂ Serre presentation. Its four numbered simple root subgroups and rank-two split weight torus are explicit. Its conjugation equation describes the root character as DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2, hence as a Cartan-matrix row.

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

(G2.simplyConnectedRootDatum ht).root (G2.simpleIndex ht i)

and the lowering character with its negative. The results below substitute those identities into the carrier's integral scheme-level conjugation equation. They therefore certify that the explicit short-root carrier and DynkinType.simplyConnectedRootDatum use the same Bourbaki numbering and the same 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

• weightTorus_conj_rootSubgroup_root_simpleIndex: the positive simple-root equation in the uniform simply connected G₂ datum.
• weightTorus_conj_rootSubgroup_neg_root_simpleIndex: the negative simple-root equation.
• weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex and its negative-root counterpart: the equations on matrix-valued points.

References

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

Torus conjugation equations against the named simple roots

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_conj_rootSubgroup_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 2)).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.G2.simplyConnectedRootDatum ht).root (DynkinType.G2.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-G₂ datum.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type) [CommRing A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧ℤ) ⟶ (SplitTorus.groupScheme ℤ (Fin 2)).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.G2.simplyConnectedRootDatum ht).root (DynkinType.G2.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.G2ShortRoot.IntegralToralClosure.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type v) [CommRing A] (s : Fin 2 → 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.G2.simplyConnectedRootDatum ht).root (DynkinType.G2.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, where αᵢ is the corresponding root of the uniform simply connected type-G₂ datum.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type v) [CommRing A] (s : Fin 2 → 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.G2.simplyConnectedRootDatum ht).root (DynkinType.G2.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.