Root-action columns on the modular F4 quotient

This file records structural first- and second-divided-power columns after quotienting the modular Chevalley lattice by its short-root ideal. These formulas are stated on concrete lifts; they do not package quotient endomorphisms or exponentials.

References

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_lie_rootVector_eq_zero_of_short (α : Fin 48) (hα : f4Length α = 1) (x : f4ModularChevalleyLieAlgebra) : Submodule.Quotient.mk ⁅f4ModularRootVector α, x⁆ = 0

The first adjoint action of a short root vanishes after quotienting by the short-root ideal.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_lie_rootVector_of_specialMap_add (α β γ : Fin 48) (hα : f4Length α = 2) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) (hmap : f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv α)) : f4ShortRootSubspace.mkQ ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = f4ShortRootSubspace.mkQ (f4ModularRootVector γ)

Transport a target root edge to a long-source first-order quotient column.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_lie_rootVector_opposite (α : Fin 48) : f4ShortRootSubspace.mkQ ⁅f4ModularRootVector α, f4ModularRootVector (f4OppositeRootIndex α)⁆ = f4ShortRootSubspace.mkQ (f4ModularCoroot α)

The opposite-root first-order quotient column is the corresponding coroot lift.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_lie_rootVector_simpleCoroot (α : Fin 48) (i : Fin F4.rank) : f4ShortRootSubspace.mkQ ⁅f4ModularRootVector α, f4ModularSimpleCoroot i⁆ = -↑(RootPairing.pairing f4SimplyConnectedRootDatum α (Fin.castAdd 44 (Fin.cast rank_F4 i))) • f4ShortRootSubspace.mkQ (f4ModularRootVector α)

The simple-coroot first-order column has the signed reduced Cartan coefficient.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_lie_rootVector_eq_zero_of_no_specialMap_edge (α β : Fin 48) (hα : f4Length α = 2) (hβ : f4Length β = 2) (hopp : β ≠ f4OppositeRootIndex α) (hno : ∀ (δ : Fin 48), f4Length δ = 1 → f4SimplyConnectedRootDatum.root δ ≠ f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv α)) : f4ShortRootSubspace.mkQ ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = 0

A non-opposite long-root column vanishes when its transported target edge is absent.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_dividedSquare_rootVector_eq_zero_of_long (k : Fin 4 ⊕ Fin 4) (β : Fin 48) (hα : f4Length (f4SignedSimpleRootIndex k) = 2) (hβ : f4Length β = 2) (hopp : β ≠ f4OppositeRootIndex (f4SignedSimpleRootIndex k)) : f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ModularRootVector β)) = 0

A long-source divided-square column on a non-opposite long-root lift vanishes.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_dividedSquare_rootVector_opposite (k : Fin 4 ⊕ Fin 4) : f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ModularRootVector (f4OppositeRootIndex (f4SignedSimpleRootIndex k)))) = f4ShortRootSubspace.mkQ (f4ModularRootVector (f4SignedSimpleRootIndex k))

The exceptional divided-square quotient column is the source root-vector lift.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_dividedSquare_simpleCoroot_eq_zero (k : Fin 4 ⊕ Fin 4) (i : Fin F4.rank) : f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ModularSimpleCoroot i)) = 0

Every simple-coroot divided-square quotient column vanishes.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_dividedSquare_rootVector_eq_zero_of_no_specialMap_edge (k : Fin 4 ⊕ Fin 4) (β : Fin 48) (hα : f4Length (f4SignedSimpleRootIndex k) = 1) (hβ : f4Length β = 2) (hno : ∀ (δ : Fin 48), f4Length δ = 1 → f4SimplyConnectedRootDatum.root δ ≠ f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv (f4SignedSimpleRootIndex k))) : f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ModularRootVector β)) = 0

A short-source divided-square column vanishes without a transported target edge.

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_dividedSquare_rootVector_of_specialMap_add (k : Fin 4 ⊕ Fin 4) (β γ : Fin 48) (hα : f4Length (f4SignedSimpleRootIndex k) = 1) (hβ : f4Length β = 2) (hγ : f4Length γ = 2) (hmap : f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv γ) = f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv β) + f4SimplyConnectedRootDatum.root (f4SpecialIsogenyIndexEquiv (f4SignedSimpleRootIndex k))) : f4ShortRootSubspace.mkQ ((f4ModularDividedAdjointSquare k) (f4ModularRootVector β)) = f4ShortRootSubspace.mkQ (f4ModularRootVector γ)

Transport a target root edge to a short-source divided-square quotient column.