The simply connected root datum of type F4

This file constructs the pinned integral root datum of type F4 on the character and cocharacter lattices Fin 4 → ℤ. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. Thus the first four roots are the rows of the Bourbaki-numbered Cartan matrix, while their coroots are the standard basis vectors.

The forty-eight roots are ordered with the four Bourbaki simple roots at indices 0 through 3, then at indices 4 through 23 the remaining twenty positive roots in increasing lexicographic order of their tuple of simple-root coefficients — the order in which f4RootCoefficients lists those tuples — and finally at index i + 24 the negative of the root at index i. The coordinate tables make both the carrier and every reflection explicit. The first two simple roots are long and the last two are short.

Main definitions and results

• TauCeti.DynkinType.f4SimplyConnectedRootDatum is the pinned forty-eight-root datum.
• TauCeti.DynkinType.f4ReflectionIndex is its explicit action on root indices.
• The RootPairing.IsRootSystem instance for TauCeti.DynkinType.f4SimplyConnectedRootDatum says that its roots span the character lattice and its coroots span the cocharacter lattice. The latter, span_coroot_eq_top, is the simply connected condition the file is named for: the datum has cocharacter lattice equal to the coroot lattice, so no central isogeny quotient of the simply connected form is taken.
• TauCeti.DynkinType.f4SimplyConnectedBase is its Bourbaki-numbered base.
• TauCeti.DynkinType.f4SimplyConnectedRootDatum_pairing_eq_cartanMatrix_F₄ pins the numbering.
• TauCeti.DynkinType.hasCartanType_f4SimplyConnectedRootDatum identifies its Cartan type.

References

The node numbering and the Cartan matrix follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII. The coordinate tables here are not in Bourbaki's orthonormal model, in which the long roots are ±eᵢ ± eⱼ and the short roots are ±eᵢ and (±e₁ ± e₂ ± e₃ ± e₄) / 2: they are written in the fundamental-weight basis for the roots and the simple-coroot basis for the coroots. This is the F4 branch of Layer 6 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

def TauCeti.DynkinType.f4Root : Fin 48 ↪ Fin 4 → ℤ

The roots of F4 in the fundamental-weight basis, with the simple roots first and the negative roots in the second half.

Equations

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

def TauCeti.DynkinType.f4Coroot : Fin 48 ↪ Fin 4 → ℤ

The coroots of F4 in the simple-coroot basis, ordered compatibly with f4Root.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4Root_castAdd (i : Fin 4) : f4Root (Fin.castAdd 44 i) = CartanMatrix.F₄ i

The simple roots of F4 sit at the first four indices, where they are the rows of Mathlib's Bourbaki-numbered Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.f4Coroot_castAdd (i : Fin 4) : f4Coroot (Fin.castAdd 44 i) = Pi.single i 1

The simple coroots of F4 sit at the first four indices, where they are the standard basis of the cocharacter lattice.

@[simp]

theorem TauCeti.DynkinType.f4Root_addNat (i : Fin 24) : f4Root (i.addNat 24) = -f4Root (Fin.castAdd 24 i)

The root at index i + 24 is the negative of the root at index i.

@[simp]

theorem TauCeti.DynkinType.f4Coroot_addNat (i : Fin 24) : f4Coroot (i.addNat 24) = -f4Coroot (Fin.castAdd 24 i)

The coroot at index i + 24 is the negative of the coroot at index i.

def TauCeti.DynkinType.f4PositiveIndex (i : Fin 48) : Fin 24

The first-half index underlying a root, identifying a negative root with its positive opposite.

Equations

• TauCeti.DynkinType.f4PositiveIndex i = ⟨↑i % 24, ⋯⟩

@[simp]

theorem TauCeti.DynkinType.f4PositiveIndex_castAdd (i : Fin 24) : f4PositiveIndex (Fin.castAdd 24 i) = i

The first twenty-four indices are their own first-half index.

@[simp]

theorem TauCeti.DynkinType.f4PositiveIndex_addNat (i : Fin 24) : f4PositiveIndex (i.addNat 24) = i

Adding twenty-four to a first-half index leaves the first-half index unchanged.

def TauCeti.DynkinType.f4ReflectionTable : Fin 24 → Fin 48 → Fin 48

The permutation table for reflection in each of the twenty-four positive F4 roots. Reflection in the corresponding negative root is the same permutation.

Equations

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

def TauCeti.DynkinType.f4ReflectionIndex (i j : Fin 48) : Fin 48

The explicit action of the reflection in the root of index i on root indices: it sends the index j to f4ReflectionIndex i j.

Equations

• TauCeti.DynkinType.f4ReflectionIndex i j = TauCeti.DynkinType.f4ReflectionTable (TauCeti.DynkinType.f4PositiveIndex i) j

@[simp]

theorem TauCeti.DynkinType.f4ReflectionIndex_castAdd (i : Fin 24) (j : Fin 48) : f4ReflectionIndex (Fin.castAdd 24 i) j = f4ReflectionTable i j

Reflection in one of the first twenty-four roots permutes root indices by the corresponding row of f4ReflectionTable.

@[simp]

theorem TauCeti.DynkinType.f4ReflectionIndex_addNat (i : Fin 24) (j : Fin 48) : f4ReflectionIndex (i.addNat 24) j = f4ReflectionIndex (Fin.castAdd 24 i) j

Reflection in a negative root is the same permutation of root indices as reflection in its positive opposite.

noncomputable def TauCeti.DynkinType.f4SimplyConnectedRootDatum : RootDatum (Fin 48) (Fin 4 → ℤ) (Fin 4 → ℤ)

The pinned simply connected root datum of type F4.

Both lattices use Fin 4 → ℤ: fundamental weights on the root side and simple coroots on the coroot side. Root indices 0 through 3 are the Bourbaki simple roots.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_root : f4SimplyConnectedRootDatum.root = f4Root

The root embedding of the pinned F4 datum is the explicit table f4Root.

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_coroot : f4SimplyConnectedRootDatum.coroot = f4Coroot

The coroot embedding of the pinned F4 datum is the explicit table f4Coroot.

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_toLinearMap_apply_apply (x y : Fin 4 → ℤ) : (f4SimplyConnectedRootDatum.toLinearMap x) y = x ⬝ᵥ y

The perfect pairing of the pinned F4 datum is the standard dot product.

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_pairing (i j : Fin 48) : RootPairing.pairing f4SimplyConnectedRootDatum i j = f4Root i ⬝ᵥ f4Coroot j

Pairing a pinned F4 root with a coroot computes as their coordinate dot product.

theorem TauCeti.DynkinType.abs_pairing_f4SimplyConnectedRootDatum_le_two (i j : Fin 48) : |RootPairing.pairing f4SimplyConnectedRootDatum i j| ≤ 2

Every Cartan integer between roots of the pinned type F₄ datum has absolute value at most two.

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_reflectionPerm (i j : Fin 48) : (f4SimplyConnectedRootDatum.reflectionPerm i) j = f4ReflectionIndex i j

Reflection in the root of index i permutes the root indices of the pinned F4 datum by the explicit table f4ReflectionIndex i.

theorem TauCeti.DynkinType.span_root_f4SimplyConnectedRootDatum_eq_top : Submodule.span ℤ (Set.range ⇑f4SimplyConnectedRootDatum.root) = ⊤

The roots of the pinned type F₄ datum span the character lattice.

instance TauCeti.DynkinType.instIsRootSystemFinOfNatNatIntForallF4SimplyConnectedRootDatum : RootPairing.IsRootSystem f4SimplyConnectedRootDatum

The pinned F4 datum is a root system: its roots and coroots span the character and cocharacter lattices. Coroot spanning is the simply connected lattice condition.

def TauCeti.DynkinType.f4Support : Finset (Fin 48)

The support of the Bourbaki-numbered base of the pinned F4 datum: the first four root indices, which carry the simple roots.

Equations

• TauCeti.DynkinType.f4Support = TauCeti.simpleSupport TauCeti.DynkinType.f4Support._proof_1✝

@[simp]

theorem TauCeti.DynkinType.mem_f4Support {i : Fin 48} : i ∈ f4Support ↔ ↑i < 4

The support of the base consists exactly of the four indices below 4.

def TauCeti.DynkinType.f4SimplyConnectedBase : RootPairing.Base f4SimplyConnectedRootDatum

The Bourbaki-numbered base of the pinned simply connected F4 datum. Its support is the first four root indices, with the two long simple roots followed by the two short simple roots.

Equations

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

@[simp]

theorem TauCeti.DynkinType.f4SimplyConnectedBase_support : f4SimplyConnectedBase.support = f4Support

theorem TauCeti.DynkinType.f4SimplyConnectedRootDatum_pairing_eq_cartanMatrix_F₄ (i j : Fin 4) : RootPairing.pairing f4SimplyConnectedRootDatum (Fin.castAdd 44 i) (Fin.castAdd 44 j) = CartanMatrix.F₄ i j

The Cartan integers of the pinned datum at the first four root indices are Mathlib's Bourbaki-numbered F4 matrix. This pins the node order independently of the existential relabelling in HasCartanType.

theorem TauCeti.DynkinType.hasCartanType_f4SimplyConnectedRootDatum : HasCartanType f4SimplyConnectedRootDatum f4SimplyConnectedBase F4

The pinned simply connected F4 datum has Cartan type F4. Its Bourbaki-numbered base realizes the standard Cartan matrix CartanMatrix.F₄, with the node numbering of TauCeti.DynkinType.