Positive-root collection in the seven-dimensional G₂ carrier

commutatorElement_positive_simple_eq_root_product collects the commutator of the two positive simple-root points into four root-subgroup factors, ordered by increasing height. The nonsimple root parameters are normalized by actual opposite-root words, not by an independent choice of root vectors. With nᵢ = xᵢ(1)x₋ᵢ(-1)xᵢ(1), the conjugating words are n₂, n₁n₂, n₁, and n₂n₁; the corresponding roots are α₁+α₂, 2α₁+α₂, 3α₁+α₂, and 3α₁+2α₂. Their parameters are respectively -ab, a²b, a³b, and 2a³b².

The formula holds over arbitrary commutative rings, with the divided-square terms retained. It supplies the triple-bond collection relation for the explicit carrier. It does not identify that carrier with an independently constructed pinned simply connected group scheme.

The calculation uses the integral root matrices of G2ShortRoot.AdmissibleLattice and their faithful point realization in IntegralToralClosure.Basic.

References

• R. W. Carter, Simple Groups of Lie Type, Theorem 5.2.2.
• R. Steinberg, Lectures on Chevalley Groups, §§3 and 6.

theorem TauCeti.G2ShortRoot.IntegralToralClosure.commutatorElement_positive_simple_eq_root_product (A : Type v) [CommRing A] (a b : A) : have x := fun (i : Fin 2) (t : A) => (rootSubgroupPoints (Sum.inl i) A) (Multiplicative.ofAdd t); have n := fun (i : Fin 2) => x i 1 * (rootSubgroupPoints (Sum.inr i) A) (Multiplicative.ofAdd (-1)) * x i 1; ⁅x 0 a, x 1 b⁆ = n 1 * x 0 (-a * b) * (n 1)⁻¹ * (n 0 * n 1 * x 0 (a ^ 2 * b) * (n 0 * n 1)⁻¹) * (n 0 * x 1 (a ^ 3 * b) * (n 0)⁻¹) * (n 1 * n 0 * x 1 (2 * a ^ 3 * b ^ 2) * (n 1 * n 0)⁻¹)

The positive-simple-root Chevalley collection formula in type G₂. The four factors are normalized by the displayed Weyl words and ordered as α₁+α₂, 2α₁+α₂, 3α₁+α₂, 3α₁+2α₂. No invertibility, characteristic or reducedness condition on the coefficients is needed.