First-order pinning on the modular F4 quotient

This file compares the first adjoint columns of long signed-simple roots on the quotient by the short-root ideal with the corresponding columns for the reversed short roots on the ideal.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §12.3.

theorem TauCeti.DynkinType.f4_pairing_specialIsogenyIndexEquiv_eq_of_length_eq (α β : Fin 48) (hαβ : f4Length α = f4Length β) : RootPairing.pairing f4SimplyConnectedRootDatum (f4SpecialIsogenyIndexEquiv α) (f4SpecialIsogenyIndexEquiv β) = RootPairing.pairing f4SimplyConnectedRootDatum α β

The special root permutation preserves Cartan integers between roots of equal length.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_mkQ_rootVector (γ : Fin 48) (hγ : f4Length γ = 2) : f4ShortRootQuotientToIdealEquiv (f4ShortRootSubspace.mkQ (f4ModularRootVector γ)) = f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl ⟨f4SpecialIsogenyIndexEquiv γ, ⋯⟩))

Evaluation of the quotient-to-ideal equivalence on a long root vector.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_eq_firstColumn_of_specialMap_add (k : Fin 4 ⊕ Fin 4) (β γ : Fin 48) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) (hadd : f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv (f4SignedSimpleRootIndex k))) : have iβ := ⟨f4SpecialIsogenyIndexEquiv β, ⋯⟩; have a := f4ShortRootWeightIndexEquiv.symm (Sum.inl iβ); f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

A surviving long-source first-order quotient edge is the matching first-order edge for the reversed short source on the short-root ideal.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_opposite_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) : have i := ⟨f4SpecialIsogenyIndexEquiv (f4OppositeRootIndex (f4SignedSimpleRootIndex k)), ⋯⟩; have a := f4ShortRootWeightIndexEquiv.symm (Sum.inl i); f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

On the opposite long-root coordinate, the first-order quotient column agrees with the opposite-root column for the reversed short source.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_rootColumn_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (i : F4ShortRootIndex) : have a := f4ShortRootWeightIndexEquiv.symm (Sum.inl i); f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

For a long signed-simple source, every root-coordinate quotient first-order column agrees with the reversed short-source first-order column on the short-root ideal.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_twelve_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k 12) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) 12

A long source has matching first-order quotient and ideal columns at coordinate 12.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_thirteen_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k 13) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) 13

A long source has matching first-order quotient and ideal columns at coordinate 13.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_firstColumn_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientFirstColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

Every long-source quotient first-order column is the matching first-order column for the reversed short source on the short-root ideal.