The prime-field F₄ carrier and its named simple roots

The short-root carrier over 𝔽₂ has numbered positive and negative simple-root subgroups and a split weight torus. Their conjugation law in PrimeField.PointsFunctor uses the Cartan-matrix weights of the Serre generators. Here the positive weight is identified with the corresponding root of DynkinType.F4.simplyConnectedRootDatum, and the negative weight with its negative. The resulting equations hold on points over every commutative 𝔽₂-algebra, including nonreduced ones, and on the corresponding scheme-valued points. They identify the numbering and torus characters that a pinned-group comparison must preserve.

The carrier and the pinned Chevalley--Demazure group are not identified here.

The root conventions are those of N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII; the construction of the carrier follows R. W. Carter, Simple Groups of Lie Type, §§4.4 and 7.1. The corresponding integral construction is TauCeti.Algebra.Lie.F4.ShortRoot.RootDatum.

theorem TauCeti.F4ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints_root_simpleIndex (ht : DynkinType.F4.Valid) (i : Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) 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.F4.simplyConnectedRootDatum ht).root (DynkinType.F4.simpleIndex ht i))) * Multiplicative.toAdd u))

The weight-torus character of a positive numbered simple-root subgroup of the prime-field carrier is the matching simple root of the simply connected type-F₄ datum.

theorem TauCeti.F4ShortRoot.PrimeField.weightTorusPoints_conj_rootSubgroupPoints_neg_root_simpleIndex (ht : DynkinType.F4.Valid) (i : Fin 4) (A : Type v) [CommRing A] [Algebra (ZMod 2) 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.F4.simplyConnectedRootDatum ht).root (DynkinType.F4.simpleIndex ht i))) * Multiplicative.toAdd u))

The weight-torus character of a negative numbered simple-root subgroup of the prime-field carrier is the negative of the matching simple root of the simply connected type-F₄ datum.

theorem TauCeti.F4ShortRoot.PrimeField.weightTorus_conj_rootSubgroup_root_simpleIndex (ht : DynkinType.F4.Valid) (i : Fin 4) (A : Type) [CommRing A] [Algebra (ZMod 2) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ (SplitTorus.groupScheme (ZMod 2) (Fin 4)).X) (u : A) : CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).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.F4.simplyConnectedRootDatum ht).root (DynkinType.F4.simpleIndex ht i))) * u))) (rootSubgroup (Sum.inl i)).hom.hom

Conjugation by the weight torus rescales a positive numbered simple-root subgroup by the matching root of the simply connected F₄ datum, on scheme-valued points.

theorem TauCeti.F4ShortRoot.PrimeField.weightTorus_conj_rootSubgroup_neg_root_simpleIndex (ht : DynkinType.F4.Valid) (i : Fin 4) (A : Type) [CommRing A] [Algebra (ZMod 2) A] (s : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧(ZMod 2)) ⟶ (SplitTorus.groupScheme (ZMod 2) (Fin 4)).X) (u : A) : CategoryTheory.CategoryStruct.comp s weightTorus.hom.hom * CategoryTheory.CategoryStruct.comp ((AdditiveGroup.schemePointsMulEquiv A).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.F4.simplyConnectedRootDatum ht).root (DynkinType.F4.simpleIndex ht i))) * u))) (rootSubgroup (Sum.inr i)).hom.hom

Conjugation by the weight torus rescales a negative numbered simple-root subgroup by the negative of the matching root of the simply connected F₄ datum, on scheme-valued points.