Squared lengths of the pinned F₄ roots

TauCeti.DynkinType.f4SimplyConnectedRootDatum tabulates its forty-eight roots in the fundamental-weight basis and its forty-eight coroots in the simple-coroot basis. Neither table displays how long a root is, and a consumer that has to distinguish long roots from short ones needs that: a characteristic-two special isogeny of type F₄ attaches one field exponent to the long root subgroups and another to the short ones.

This file supplies the missing table. TauCeti.DynkinType.f4Length is normalised as TauCeti.DynkinType.rootLength normalises the simple roots, so it is 1 on the twenty-four short roots and 2 on the twenty-four long ones. Mathlib's RootPairing.RootPositiveForm.rootLength is not that table: it is the value of a chosen invariant form, so it carries whatever scale that form has, whereas the exponent convention of a special isogeny is stated against the normalisation in which a shortest root has length 1.

The normalisation is not a stipulation. Because the invariant form is symmetric, ℓ(α) ⟨β, α∨⟩ = 2 (β, α) = 2 (α, β) = ℓ(β) ⟨α, β∨⟩ for every pair of roots, and TauCeti.DynkinType.f4Length_mul_pairing_comm records exactly that identity for the tabulated values. Together with the value on the four simple roots those equations pin the whole table, which is TauCeti.DynkinType.eq_f4Length_of_mul_pairing.

Main definitions

• TauCeti.DynkinType.f4Length: the squared length of each of the forty-eight pinned roots.

Main results

• TauCeti.DynkinType.f4Length_mul_pairing_comm and TauCeti.DynkinType.eq_f4Length_of_mul_pairing: the table symmetrises the Cartan integers, and it is the only table doing so with the prescribed values on the simple roots.
• TauCeti.DynkinType.f4Length_castAdd: on the four simple roots it is TauCeti.DynkinType.rootLength.
• TauCeti.DynkinType.isLongSimpleRoot_iff_f4Length_eq_two and TauCeti.DynkinType.f4Length_castAdd_eq_one_iff: the two long simple roots are the ones of length two and the two short ones the ones of length one.

References

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII. The table is the type F₄ input asked for by the "special isogenies in characteristics two and three" bullet of Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, matching the rank-two type B table of TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/B/RankTwo.lean.

def TauCeti.DynkinType.f4Length : Fin 48 → ℤ

The squared lengths of the forty-eight roots of the pinned F₄ datum, in the index order of TauCeti.DynkinType.f4Root and normalised as TauCeti.DynkinType.rootLength normalises the simple ones: 1 on a short root and 2 on a long one.

Equations

• TauCeti.DynkinType.f4Length = ![2, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 2, 2]

theorem TauCeti.DynkinType.f4Length_def : f4Length = ![2, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 2, 2, 2, 2, 1, 1, 1, 1, 1, 2, 1, 2, 2, 1, 1, 2, 1, 2, 2, 1, 2, 1, 1, 2, 2, 2]

The explicit squared lengths of the roots in the pinned F₄ table.

@[simp]

theorem TauCeti.DynkinType.f4Length_castAdd (i : Fin 4) : f4Length (Fin.castAdd 44 i) = F4.rootLength i

On the four simple roots the length table is TauCeti.DynkinType.rootLength: the first two Bourbaki nodes of F₄ are long and the last two are short.

@[simp]

theorem TauCeti.DynkinType.f4Length_add_twentyFour (i : Fin 48) : f4Length (i + 24) = f4Length i

A root and its negative have the same squared length.

theorem TauCeti.DynkinType.f4Length_eq_one_or_eq_two (i : Fin 48) : f4Length i = 1 ∨ f4Length i = 2

Every root of the pinned F₄ datum is short or long, of squared length 1 or 2.

theorem TauCeti.DynkinType.f4Length_pos (i : Fin 48) : 0 < f4Length i

Every root of the pinned F₄ datum has positive squared length.

theorem TauCeti.DynkinType.f4Length_mul_pairing_comm (i j : Fin 48) : f4Length i * RootPairing.pairing f4SimplyConnectedRootDatum j i = f4Length j * RootPairing.pairing f4SimplyConnectedRootDatum i j

The length table symmetrises the Cartan integers. Expanding α∨ = 2 α / (α, α) on both sides, the identity ℓ(α) ⟨β, α∨⟩ = ℓ(β) ⟨α, β∨⟩ is the symmetry of the invariant form.

theorem TauCeti.DynkinType.eq_f4Length_of_mul_pairing {k : Fin 48} {c : ℤ} (h : ∀ (i : Fin 4), c * RootPairing.pairing f4SimplyConnectedRootDatum (Fin.castAdd 44 i) k = F4.rootLength i * RootPairing.pairing f4SimplyConnectedRootDatum k (Fin.castAdd 44 i)) : c = f4Length k

The symmetry equations against the simple roots determine the length table. No root is orthogonal to every simple root, so the value at an arbitrary index is forced by the four values TauCeti.DynkinType.f4Length_castAdd prescribes.

theorem TauCeti.DynkinType.isLongSimpleRoot_iff_f4Length_eq_two (i : Fin 4) : F4.IsLongSimpleRoot i ↔ f4Length (Fin.castAdd 44 i) = 2

A simple root of the pinned F₄ datum is long exactly when its squared length is two, which is the convention TauCeti.DynkinType.rootLength fixes and the one a length-exchanging map is pinned against.

theorem TauCeti.DynkinType.f4Length_castAdd_eq_one_iff (i : Fin 4) : f4Length (Fin.castAdd 44 i) = 1 ↔ ¬F4.IsLongSimpleRoot i

A simple root of the pinned F₄ datum is short exactly when its squared length is one. This is the form in which a characteristic-two special isogeny states which of its two rescaling exponents it attaches to which node.