Documentation

TauCeti.Algebra.Lie.G2.ShortRoot.CrossProduct.Diagonal

Diagonal automorphisms of the type-G₂ cross product #

When multiplication by two is injective, an invertible diagonal matrix preserves the seven-dimensional cross product exactly when its diagonal entries are the characters of the short-root weight diagram. Thus tensor invariance identifies diagonal elements with the rank-two weight torus, rather than the full diagonal torus of GL₇. This is the diagonal part of the centralizer calculation for the short-root carrier.

The cross-product normalization is that of TauCeti.Algebra.Lie.G2.ShortRoot.CrossProduct.Basic; the weight coordinates follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX.

theorem TauCeti.G2ShortRoot.preservesG2Cross_diagonal_iff {R : Type u_1} [CommRing R] (h2 : IsRegular 2) (d : Fin 7 → Rˣ) :
(Matrix.diagonal fun (i : Fin 7) => ↑(d i)).PreservesG2Cross ↔ ∃ (s : Fin 2 → Rˣ), ∀ (i : Fin 7), d i = torusCharacter s (weight i)

An invertible diagonal matrix preserves the type-G₂ cross product exactly when its entries come from the rank-two weight torus, provided two is regular.