Torus pinning for the modular F4 quotient #
The special character-lattice map sends a torus point s to
(s₃², s₂², s₁, s₀). This file proves the corresponding character identity
and specializes it to the quotient basis: its long-root weight has the same
character as the associated short-root weight after applying the special torus
map. The two Cartan coordinates have weight zero on both sides.
References #
- R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11, for the
special isogeny of type
F₄and its effect on the character lattice. - R. W. Carter, Simple Groups of Lie Type, §12.3.
- N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII, for the root coordinates and the simple-root numbering.
The quotient-basis weight: the long root paired with a nonzero short-root weight, and zero on the two Cartan coordinates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.DynkinType.coe_torusCharacter_f4ShortRootQuotientWeight
{A : Type u_1}
[CommRing A]
(s : Fin 4 → Aˣ)
(a : Fin 26)
:
↑(torusCharacter s (f4ShortRootQuotientWeight a)) = ↑(torusCharacter (f4SpecialIsogenyTorusMap s) (f4ShortRootWeight a))
The quotient-basis character identity after coercing units to the scalar ring.