Simple-root weights of the prime-field short-root type-G2 carrier

TauCeti.G2ShortRoot.PrimeField.groupScheme is the type-G₂ carrier over 𝔽₃ generated by the reductions of the four numbered simple root subgroups and the rank-two weight torus. The carrier's matrix-valued torus-conjugation equation is initially expressed through DynkinType.G2.rootGeneratorWeight DynkinType.valid_G2, the Cartan-row character attached to a signed simple-root index.

This file rewrites the scheme-point and matrix-point equations against DynkinType.G2.simplyConnectedRootDatum, identifying the carrier's generator weights with the named positive and negative simple roots in Bourbaki numbering. The corresponding integral equations live in TauCeti.Algebra.Lie.G2.ShortRoot.IntegralToralClosure.RootDatum; the results here concern the separately generated carrier over 𝔽₃, whose defining ideal can be strictly larger than the reduction of the integral defining ideal.

No reductivity, maximality of the torus, or identification with an independently constructed pinned group scheme is asserted.

Main results

• TauCeti.G2ShortRoot.PrimeField.weightTorus_conj_rootSubgroup: the torus-conjugation equation on scheme-valued points of the prime-field carrier.
• TauCeti.G2ShortRoot.PrimeField.weightTorus_conj_rootSubgroup_root_simpleIndex and its negative-root counterpart: the scheme-point equations against the named root datum.
• TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex and its negative-root counterpart: the same 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 organization follows TauCeti.Algebra.Lie.G2.ShortRoot.IntegralToralClosure.RootDatum.

The named simply connected root datum

theorem TauCeti.G2ShortRoot.PrimeField.weightTorus_conj_rootSubgroup_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type) [CommRing A] [Algebra (ZMod 3) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ (SplitTorus.groupScheme (ZMod 3) (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 scheme-valued point of the prime-field weight torus conjugates the raising-subgroup element at node i through the corresponding root of the uniform simply connected type-G₂ datum.

theorem TauCeti.G2ShortRoot.PrimeField.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type) [CommRing A] [Algebra (ZMod 3) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 3)) ⟶ (SplitTorus.groupScheme (ZMod 3) (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 scheme-valued point of the prime-field weight torus conjugates the lowering-subgroup element at node i through the negative of the corresponding root of the uniform simply connected type-G₂ datum.

The named equations on matrix-valued points

theorem TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) 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 prime-field torus-conjugation equation at a named positive simple root, on matrix-valued points. The root character is the corresponding root of the uniform simply connected type-G₂ datum.

theorem TauCeti.G2ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex (ht : DynkinType.G2.Valid) (i : Fin 2) (A : Type v) [CommRing A] [Algebra (ZMod 3) 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 prime-field torus-conjugation equation at a named negative simple root, on matrix-valued points. The root character is the negative of the corresponding root of the uniform simply connected type-G₂ datum.