Divided-square pinning on the modular F4 quotient

This file compares divided-square quotient columns with the reversed first-order and second-order columns on the short-root 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.f4ShortRootQuotientToIdealEquiv_dividedSquare_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 (f4ShortRootQuotientDividedSquareColumn k a) = f4ShortRootIdealDividedSquareColumn (F4ShortRoot.isogenyReverse k) a

On the opposite long-root coordinate, the quotient divided square is exactly the target short-root divided-square column after reversing the signed simple-root label.

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

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

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_twelve (k : Fin 4 ⊕ Fin 4) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k 12) = f4ShortRootIdealDividedSquareColumn (F4ShortRoot.isogenyReverse k) 12

On zero-weight coordinate 12, the quotient and ideal divided-square columns both vanish.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_thirteen (k : Fin 4 ⊕ Fin 4) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k 13) = f4ShortRootIdealDividedSquareColumn (F4ShortRoot.isogenyReverse k) 13

On zero-weight coordinate 13, the quotient and ideal divided-square columns both vanish.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_of_long (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 2) (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k a) = f4ShortRootIdealDividedSquareColumn (F4ShortRoot.isogenyReverse k) a

Every long-source quotient divided-square column is the corresponding ideal divided-square column after reversing the signed simple-root label.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_eq_firstColumn_of_specialMap_add (k : Fin 4 ⊕ Fin 4) (β γ : Fin 48) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) (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 (f4ShortRootQuotientDividedSquareColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

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

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

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

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_eq_firstColumn_twelve_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k 12) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) 12

For a short source, the quadratic quotient column at coordinate 12 and the reversed first-order ideal column both vanish.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_eq_firstColumn_thirteen_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k 13) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) 13

For a short source, the quadratic quotient column at coordinate 13 and the reversed first-order ideal column both vanish.

theorem TauCeti.DynkinType.f4ShortRootQuotientToIdealEquiv_dividedSquare_eq_firstColumn_of_short (k : Fin 4 ⊕ Fin 4) (hk : f4Length (f4SignedSimpleRootIndex k) = 1) (a : Fin 26) : f4ShortRootQuotientToIdealEquiv (f4ShortRootQuotientDividedSquareColumn k a) = f4ShortRootIdealFirstColumn (F4ShortRoot.isogenyReverse k) a

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