The modular short-root coordinate space in type F₄

In the full integral F₄ Chevalley lattice reduced modulo two, the distinguished coordinate subspace is spanned by the twenty-four short-root vectors and the two short simple coroots.

The subspace is defined only after reduction modulo two. Its integral coordinate span is not a Lie ideal: a short--short bracket can be twice a long-root vector.

This is the full integral Chevalley lattice reduced modulo two. In this characteristic it must not be replaced by the Lie algebra generated by the reductions of the simple generators: taking the generated image and reducing the full integral lattice need not commute.

Main declaration

• TauCeti.DynkinType.f4ShortRootLieIdeal: the characteristic-two short-root ideal of the reduced integral Chevalley algebra, used in the construction of the F₄ special isogeny.

References

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

def TauCeti.DynkinType.F4ChevalleyIndexIsShort : f4ChevalleyIndex → Prop

A Chevalley coordinate is short when it is labelled by a short root or by one of the two short simple coroots.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ChevalleyIndexIsShort_inl_iff (α : ↥LieSubalgebra.root) : F4ChevalleyIndexIsShort (Sum.inl α) ↔ f4Length (f4PinnedRootIndex α) = 1

@[simp]

theorem TauCeti.DynkinType.f4ChevalleyIndexIsShort_inr_iff (j : ↥f4KillingBase.support) : F4ChevalleyIndexIsShort (Sum.inr j) ↔ f4PinnedSimpleIndexEquiv j = 2 ∨ f4PinnedSimpleIndexEquiv j = 3

def TauCeti.DynkinType.f4ShortChevalleyIndices : Set f4ChevalleyIndex

The coordinate labels spanning the modular short-root space.

Equations

• TauCeti.DynkinType.f4ShortChevalleyIndices = {i : TauCeti.DynkinType.f4ChevalleyIndex | TauCeti.DynkinType.F4ChevalleyIndexIsShort i}

@[simp]

theorem TauCeti.DynkinType.mem_f4ShortChevalleyIndices_iff (i : f4ChevalleyIndex) : i ∈ f4ShortChevalleyIndices ↔ F4ChevalleyIndexIsShort i

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

The modular coordinate subspace spanned by short root vectors and the two short simple coroots. It is a Lie ideal; see f4ShortRootLieIdeal.

Equations

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

theorem TauCeti.DynkinType.f4ShortRootSubspace_eq_span : f4ShortRootSubspace = Submodule.span (ZMod 2) (⇑f4ModularChevalleyBasis '' f4ShortChevalleyIndices)

The short-root subspace is the span of the Chevalley basis vectors with short indices.

theorem TauCeti.DynkinType.f4ModularChevalleyBasis_mem_shortRootSubspace {i : f4ChevalleyIndex} (hi : F4ChevalleyIndexIsShort i) : f4ModularChevalleyBasis i ∈ f4ShortRootSubspace

theorem TauCeti.DynkinType.f4ModularRootVector_mem_shortRootSubspace (β : Fin 48) (hβ : f4Length β = 1) : f4ModularRootVector β ∈ f4ShortRootSubspace

theorem TauCeti.DynkinType.f4ModularSimpleCoroot_mem_shortRootSubspace (i : Fin F4.rank) (hi : Fin.cast rank_F4 i = 2 ∨ Fin.cast rank_F4 i = 3) : f4ModularSimpleCoroot i ∈ f4ShortRootSubspace

theorem TauCeti.DynkinType.f4ModularCoroot_mem_shortRootSubspace (β : Fin 48) (hβ : f4Length β = 1) : f4ModularCoroot β ∈ f4ShortRootSubspace

Every short-root coroot reduces to the span of the two short simple coroots modulo two.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_eq_zero_of_short_add_short_eq_long (α β γ : Fin 48) (hα : f4Length α = 1) (hβ : f4Length β = 1) (hγ : f4Length γ = 2) (h : f4SimplyConnectedRootDatum.root γ = f4SimplyConnectedRootDatum.root β + f4SimplyConnectedRootDatum.root α) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ = 0

A short--short Chevalley bracket with long-root target vanishes in the modular lattice.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_mem_shortRootSubspace (α β : Fin 48) (hβ : f4Length β = 1) : ⁅f4ModularRootVector α, f4ModularRootVector β⁆ ∈ f4ShortRootSubspace

Bracketing an arbitrary modular root vector with a short-root vector stays in the modular short-root coordinate space.

theorem TauCeti.DynkinType.f4Modular_lie_rootVector_simpleCoroot_mem_shortRootSubspace (α : Fin 48) (i : Fin F4.rank) (hi : Fin.cast rank_F4 i = 2 ∨ Fin.cast rank_F4 i = 3) : ⁅f4ModularRootVector α, f4ModularSimpleCoroot i⁆ ∈ f4ShortRootSubspace

Bracketing an arbitrary modular root vector with either short simple coroot stays in the modular short-root coordinate space. Long-root coefficients vanish by length symmetry modulo two.

theorem TauCeti.DynkinType.f4Modular_lie_simpleCoroot_rootVector_mem_shortRootSubspace (i : Fin F4.rank) (α : Fin 48) (hα : f4Length α = 1) : ⁅f4ModularSimpleCoroot i, f4ModularRootVector α⁆ ∈ f4ShortRootSubspace

theorem TauCeti.DynkinType.f4Modular_lie_basis_mem_shortRootSubspace (i j : f4ChevalleyIndex) (hj : F4ChevalleyIndexIsShort j) : ⁅f4ModularChevalleyBasis i, f4ModularChevalleyBasis j⁆ ∈ f4ShortRootSubspace

A Chevalley basis vector brackets every distinguished short Chevalley basis vector back into the short coordinate space.

theorem TauCeti.DynkinType.f4ShortRootSubspace_lie_mem (x : f4ModularChevalleyLieAlgebra) {y : f4ModularChevalleyLieAlgebra} (hy : y ∈ f4ShortRootSubspace) : ⁅x, y⁆ ∈ f4ShortRootSubspace

The modular short-root coordinate space is stable under the bracket with every element of the reduced Chevalley Lie algebra.

noncomputable def TauCeti.DynkinType.f4ShortRootLieIdeal : LieIdeal (ZMod 2) f4ModularChevalleyLieAlgebra

The characteristic-two short-root coordinate space as a Lie ideal in the reduced integral Chevalley algebra.

Equations

• TauCeti.DynkinType.f4ShortRootLieIdeal = { toSubmodule := TauCeti.DynkinType.f4ShortRootSubspace, lie_mem := ⋯ }

@[simp]

theorem TauCeti.DynkinType.f4ShortRootLieIdeal_toSubmodule : ↑f4ShortRootLieIdeal = f4ShortRootSubspace

@[simp]

theorem TauCeti.DynkinType.mem_f4ShortRootLieIdeal_iff {x : f4ModularChevalleyLieAlgebra} : x ∈ f4ShortRootLieIdeal ↔ x ∈ f4ShortRootSubspace

theorem TauCeti.DynkinType.mem_f4ShortRootSubspace_of_repr_eq_zero (X : f4ModularChevalleyLieAlgebra) (hX : ∀ (i : f4ChevalleyIndex), ¬F4ChevalleyIndexIsShort i → (f4ModularChevalleyBasis.repr X) i = 0) : X ∈ f4ShortRootSubspace

A modular Chevalley vector whose coordinates outside the distinguished short labels vanish belongs to the short-root coordinate subspace.