A basis of the modular F4 short-root subspace

The modular short-root subspace has the twenty-four short-root vectors and the two short simple coroots as a basis. The coordinate equivalence from the short-root weight table fixes the two zero-weight coordinates as the simple coroots at zero-based Lean indices 2 and 3.

Main declarations

• TauCeti.DynkinType.f4ShortRootBasisCoordinate: the corresponding full Chevalley-basis label of each of the twenty-six short-root coordinates.
• TauCeti.DynkinType.f4ShortRootBasis: the resulting basis of f4ShortRootSubspace.
• TauCeti.DynkinType.f4ShortRootLieIdealBasis: the same basis, carried by the Lie ideal f4ShortRootLieIdeal; f4ShortRootLieIdealBasis_repr_apply identifies its coordinates with the ambient Chevalley coordinates.

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

The two short simple nodes in Bourbaki order.

Equations

• TauCeti.DynkinType.f4ShortSimpleIndex k = Fin.cast TauCeti.DynkinType.f4ShortSimpleIndex._proof_2✝ ⟨↑k + 2, ⋯⟩

@[simp]

theorem TauCeti.DynkinType.f4ShortSimpleIndex_zero : f4ShortSimpleIndex 0 = Fin.cast ⋯ 2

@[simp]

theorem TauCeti.DynkinType.f4ShortSimpleIndex_one : f4ShortSimpleIndex 1 = Fin.cast ⋯ 3

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

The full Chevalley-basis coordinate assigned to a short-root-representation coordinate. Nonzero weights use their unique short-root label; coordinates 12 and 13 use the short simple-coroot labels 2 and 3.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootBasisCoordinate_symm_inl (i : F4ShortRootIndex) : f4ShortRootBasisCoordinate (f4ShortRootWeightIndexEquiv.symm (Sum.inl i)) = Sum.inl (f4KillingRootLabel ↑i)

@[simp]

theorem TauCeti.DynkinType.f4ShortRootBasisCoordinate_symm_inr (k : Fin 2) : f4ShortRootBasisCoordinate (f4ShortRootWeightIndexEquiv.symm (Sum.inr k)) = Sum.inr ((F4.lieBasis valid_F4).baseSupportEquiv (f4ShortSimpleIndex k))

theorem TauCeti.DynkinType.f4ShortRootBasisCoordinate_injective : Function.Injective f4ShortRootBasisCoordinate

@[simp]

theorem TauCeti.DynkinType.range_f4ShortRootBasisCoordinate : Set.range f4ShortRootBasisCoordinate = f4ShortChevalleyIndices

noncomputable def TauCeti.DynkinType.f4ShortRootBasis : Module.Basis (Fin 26) (ZMod 2) ↥f4ShortRootSubspace

The coordinate basis of the modular short-root subspace. The directions other than 12 and 13 are short-root vectors; those two zero-weight directions are the short simple coroots at zero-based Lean indices 2 and 3.

Equations

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

theorem TauCeti.DynkinType.coe_f4ShortRootBasis (a : Fin 26) : ↑(f4ShortRootBasis a) = f4ModularChevalleyBasis (f4ShortRootBasisCoordinate a)

Coercing a short-root basis vector gives the ambient Chevalley basis vector selected by f4ShortRootBasisCoordinate.

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootBasis_symm_inl (i : F4ShortRootIndex) : ↑(f4ShortRootBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl i))) = f4ModularRootVector ↑i

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootBasis_symm_inr (k : Fin 2) : ↑(f4ShortRootBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inr k))) = f4ModularSimpleCoroot (f4ShortSimpleIndex k)

The two zero-weight basis coordinates are the corresponding short simple coroots.

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootBasis_twelve : ↑(f4ShortRootBasis 12) = f4ModularSimpleCoroot (Fin.cast ⋯ 2)

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootBasis_thirteen : ↑(f4ShortRootBasis 13) = f4ModularSimpleCoroot (Fin.cast ⋯ 3)

noncomputable def TauCeti.DynkinType.f4ShortRootLieIdealBasis : Module.Basis (Fin 26) (ZMod 2) ↥f4ShortRootLieIdeal

The coordinate basis of the modular short-root Lie ideal.

Equations

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

@[simp]

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis (a : Fin 26) : ↑(f4ShortRootLieIdealBasis a) = f4ModularChevalleyBasis (f4ShortRootBasisCoordinate a)

The ideal basis has the same ambient Chevalley coordinates as the short-root subspace basis.

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis_symm_inl (i : F4ShortRootIndex) : ↑(f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inl i))) = f4ModularRootVector ↑i

A nonzero-weight ideal basis vector is the corresponding modular short-root vector.

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis_symm_inr (k : Fin 2) : ↑(f4ShortRootLieIdealBasis (f4ShortRootWeightIndexEquiv.symm (Sum.inr k))) = f4ModularSimpleCoroot (f4ShortSimpleIndex k)

The two zero-weight ideal basis vectors are the corresponding short simple coroots.

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis_of_weight_eq_root (b : Fin 26) (i : Fin 48) (hi : f4Length i = 1) (h : f4ShortRootWeight b = f4Root i) : ↑(f4ShortRootLieIdealBasis b) = f4ModularRootVector i

A basis coordinate whose short-root weight is the root i has the modular root vector of i as its underlying element.

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis_twelve : ↑(f4ShortRootLieIdealBasis 12) = f4ModularSimpleCoroot (Fin.cast ⋯ 2)

Ideal coordinate twelve is the short simple coroot at index two.

theorem TauCeti.DynkinType.coe_f4ShortRootLieIdealBasis_thirteen : ↑(f4ShortRootLieIdealBasis 13) = f4ModularSimpleCoroot (Fin.cast ⋯ 3)

Ideal coordinate thirteen is the short simple coroot at index three.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootLieIdealBasis_repr_apply (y : ↥f4ShortRootLieIdeal) (i : Fin 26) : (f4ShortRootLieIdealBasis.repr y) i = (f4ModularChevalleyBasis.repr ↑y) (f4ShortRootBasisCoordinate i)

Coordinates in the ideal basis agree with the corresponding ambient Chevalley coordinates.