Detecting Cartan coordinates with the short-root weights of type F4

The type-F₄ short-root weights span the integral character lattice. Consequently, their pairings detect any four-tuple in an additive commutative group. This packages that consequence without extending scalars or choosing a basis after reduction.

Main declaration

• TauCeti.DynkinType.eq_zero_of_f4ShortRootWeight_smul_eq_zero: a four-tuple is zero if every short-root weight gives the zero integral linear combination of its entries.

theorem TauCeti.DynkinType.eq_zero_of_f4ShortRootWeight_smul_eq_zero {A : Type u_1} [AddCommGroup A] (h : Fin 4 → A) (hweights : ∀ (a : Fin 26), ∑ j : Fin 4, f4ShortRootWeight a j • h j = 0) : h = 0

The type-F₄ short-root weights detect four Cartan coordinates.

This works in any additive commutative group, using its canonical ℤ-module structure. In particular, it applies after reduction to characteristic two without a separate base-change spanning argument.

theorem TauCeti.DynkinType.eq_zero_of_f4Root_smul_eq_zero_on_short {A : Type u_1} [AddCommGroup A] (c : Fin 4 → A) (hc : ∀ (β : Fin 48), f4Length β = 1 → ∑ i : Fin 4, f4Root β i • c i = 0) : c = 0

The short pinned F₄ roots detect every Cartan coordinate in an additive commutative group.