Indexing the short-root representation of type F4

The twenty-six coordinates of the short-root representation consist of the twenty-four short-root weight spaces and two zero-weight coordinates. This file identifies their index type with the sum of the short-root indices in the explicit type-F₄ root table and Fin 2.

Main declaration

• TauCeti.DynkinType.f4ShortRootWeightIndexEquiv: the equivalence between Fin 26 and the twenty-four short-root labels together with two zero-weight labels.

@[reducible, inline]

abbrev TauCeti.DynkinType.F4ShortRootIndex : Type

The indices of the short roots in the explicit type-F₄ root table.

Equations

• TauCeti.DynkinType.F4ShortRootIndex = { i : Fin 48 // TauCeti.DynkinType.f4Length i = 1 }

noncomputable def TauCeti.DynkinType.f4ShortRootWeightIndexEquiv : Fin 26 ≃ F4ShortRootIndex ⊕ Fin 2

The twenty-six short-root-representation coordinates are the twenty-four short roots and two zero-weight coordinates. The zero-weight coordinates 12 and 13 are sent to 0 and 1 in the Fin 2 summand, respectively.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_apply_twelve : f4ShortRootWeightIndexEquiv 12 = Sum.inr 0

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_apply_thirteen : f4ShortRootWeightIndexEquiv 13 = Sum.inr 1

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeight_f4ShortRootWeightIndexEquiv_symm_inl (i : F4ShortRootIndex) : f4ShortRootWeight (f4ShortRootWeightIndexEquiv.symm (Sum.inl i)) = f4Root ↑i

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_apply_eq_inl_iff (a : Fin 26) (i : F4ShortRootIndex) : f4ShortRootWeightIndexEquiv a = Sum.inl i ↔ f4ShortRootWeight a = f4Root ↑i

A coordinate index maps to a given short-root label exactly when its weight is that root.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_symm_apply_inr_zero : f4ShortRootWeightIndexEquiv.symm (Sum.inr 0) = 12

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_symm_apply_inr_one : f4ShortRootWeightIndexEquiv.symm (Sum.inr 1) = 13

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeight_f4ShortRootWeightIndexEquiv_symm_inr (k : Fin 2) : f4ShortRootWeight (f4ShortRootWeightIndexEquiv.symm (Sum.inr k)) = 0

Both coordinates in the Fin 2 summand carry the zero weight.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_apply_eq_inr_zero_iff (a : Fin 26) : f4ShortRootWeightIndexEquiv a = Sum.inr 0 ↔ a = 12

The first zero-weight coordinate is the first Fin 2 summand coordinate.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootWeightIndexEquiv_apply_eq_inr_one_iff (a : Fin 26) : f4ShortRootWeightIndexEquiv a = Sum.inr 1 ↔ a = 13

The second zero-weight coordinate is the second Fin 2 summand coordinate.