A basis of the modular F4 quotient by the short-root subspace

The complement of the short-root coordinates consists of the twenty-four long-root vectors and simple coroots at zero-based Lean indices 0 and 1. The special F4 root permutation indexes these coordinates by the same Fin 26 labels as the short-root basis. Their images in the quotient form a basis with the normalization required by the special isogeny.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11, for the special isogeny of type F₄ in characteristic two.
• 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.

def TauCeti.DynkinType.f4LongSimpleIndex (k : Fin 2) : Fin F4.rank

The long simple nodes, in the order exchanged with the two short nodes by the isogeny.

Equations

• TauCeti.DynkinType.f4LongSimpleIndex k = Fin.cast TauCeti.DynkinType.f4LongSimpleIndex._proof_1✝ (![1, 0] k)

@[simp]

theorem TauCeti.DynkinType.f4LongSimpleIndex_zero : f4LongSimpleIndex 0 = Fin.cast ⋯ 1

The first complementary simple-coroot coordinate is numbered one.

@[simp]

theorem TauCeti.DynkinType.f4LongSimpleIndex_one : f4LongSimpleIndex 1 = Fin.cast ⋯ 0

The second complementary simple-coroot coordinate is numbered zero.

noncomputable def TauCeti.DynkinType.f4LongRootBasisCoordinate (a : Fin 26) : f4ChevalleyIndex

The full Chevalley-basis coordinate complementary to a short-root-representation coordinate. A short-root label is sent through the special root permutation to its long-root partner; zero coordinates 12, 13 are sent to simple-coroot labels 1, 0, respectively.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.f4LongRootBasisCoordinate_symm_inl (i : F4ShortRootIndex) : f4LongRootBasisCoordinate (f4ShortRootWeightIndexEquiv.symm (Sum.inl i)) = Sum.inl (f4KillingRootLabel (f4SpecialIsogenyIndexEquiv ↑i))

A nonzero short-root coordinate is sent to the Chevalley coordinate of its long-root partner under the special root permutation.

@[simp]

theorem TauCeti.DynkinType.f4LongRootBasisCoordinate_symm_inr (j : Fin 2) : f4LongRootBasisCoordinate (f4ShortRootWeightIndexEquiv.symm (Sum.inr j)) = Sum.inr ((F4.lieBasis valid_F4).baseSupportEquiv (f4LongSimpleIndex j))

The zero-weight quotient coordinates are the two long simple-coroot coordinates.

theorem TauCeti.DynkinType.f4LongRootBasisCoordinate_injective : Function.Injective f4LongRootBasisCoordinate

Distinct short-root labels name distinct complementary Chevalley coordinates.

@[simp]

theorem TauCeti.DynkinType.range_f4LongRootBasisCoordinate : Set.range f4LongRootBasisCoordinate = f4ShortChevalleyIndicesᶜ

The complementary coordinates exhaust exactly the Chevalley coordinates that are not short: the twenty-four long roots and the two long simple coroots.

noncomputable def TauCeti.DynkinType.f4LongRootComplement : Submodule (ZMod 2) f4ModularChevalleyLieAlgebra

The coordinate complement to the modular short-root subspace.

Equations

• TauCeti.DynkinType.f4LongRootComplement = Submodule.span (ZMod 2) (⇑TauCeti.DynkinType.f4ModularChevalleyBasis '' TauCeti.DynkinType.f4ShortChevalleyIndicesᶜ)

theorem TauCeti.DynkinType.isCompl_f4ShortRootSubspace_f4LongRootComplement : IsCompl f4ShortRootSubspace f4LongRootComplement

The short-root subspace and its coordinate complement decompose the reduced Chevalley Lie algebra. This is what makes the complementary coordinates a basis of the quotient.

noncomputable def TauCeti.DynkinType.f4LongRootComplementBasis : Module.Basis (Fin 26) (ZMod 2) ↥f4LongRootComplement

The long-root and long-simple-coroot coordinate basis complementary to f4ShortRootSubspace.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DynkinType.coe_f4LongRootComplementBasis (a : Fin 26) : ↑(f4LongRootComplementBasis a) = f4ModularChevalleyBasis (f4LongRootBasisCoordinate a)

The complement basis vector embeds as its matching modular Chevalley vector.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_longRootBasisCoordinate_twelve : f4ModularChevalleyBasis (f4LongRootBasisCoordinate 12) = f4ModularSimpleCoroot (Fin.cast ⋯ 1)

Complement coordinate twelve is the surviving simple coroot at index one.

@[simp]

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_longRootBasisCoordinate_thirteen : f4ModularChevalleyBasis (f4LongRootBasisCoordinate 13) = f4ModularSimpleCoroot (Fin.cast ⋯ 0)

Complement coordinate thirteen is the surviving simple coroot at index zero.

noncomputable def TauCeti.DynkinType.f4ShortRootQuotientBasis : Module.Basis (Fin 26) (ZMod 2) (f4ModularChevalleyLieAlgebra ⧸ f4ShortRootSubspace)

The special-isogeny-indexed basis of the modular quotient by the short-root subspace.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DynkinType.f4ShortRootQuotientBasis_apply (a : Fin 26) : f4ShortRootQuotientBasis a = Submodule.Quotient.mk (f4ModularChevalleyBasis (f4LongRootBasisCoordinate a))

Each quotient basis vector is the class of its complementary Chevalley basis vector.

theorem TauCeti.DynkinType.f4ShortRootQuotientBasis_symm_inl (i : F4ShortRootIndex) : f4ShortRootQuotientBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl i)) = Submodule.Quotient.mk (f4ModularRootVector (f4SpecialIsogenyIndexEquiv ↑i))

A nonzero-weight quotient coordinate is the corresponding special-map long-root class.

theorem TauCeti.DynkinType.f4ShortRootQuotientBasis_twelve : f4ShortRootQuotientBasis 12 = Submodule.Quotient.mk (f4ModularSimpleCoroot (Fin.cast ⋯ 1))

Quotient coordinate twelve is the class of the first surviving simple coroot.

theorem TauCeti.DynkinType.f4ShortRootQuotientBasis_thirteen : f4ShortRootQuotientBasis 13 = Submodule.Quotient.mk (f4ModularSimpleCoroot (Fin.cast ⋯ 0))

Quotient coordinate thirteen is the class of the other surviving simple coroot.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSubspace_mkQ_rootVector_eq_quotientBasis (γ : Fin 48) (hγ : f4Length γ = 2) : Submodule.Quotient.mk (f4ModularRootVector γ) = f4ShortRootQuotientBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl ⟨f4SpecialIsogenyIndexEquiv γ, ⋯⟩))

A long-root lift is the quotient basis vector indexed by its short special-map image.