Documentation

TauCeti.RingTheory.Nilpotent.RootString.G2.ShortPair

The exponential relation for the short pair in type G₂ #

For Chevalley root vectors x, y, z, w, s at the roots α, α + β, 2α + β, 3α + β, 3α + 2β, choose signs such that

[x, y] = 2z,  [x, z] = 3w,  [z, y] = 3s.

If x, y, and z are nilpotent, then on any additive subgroup stable under all five families of divided powers the integral exponentials satisfy

E_x(t) E_y(u) = E_y(u) E_z(2tu) E_w(3t²u) E_s(3tu²) E_x(t).

The parameter ring is an arbitrary commutative ring: the factors 2 and 3 are multiplied, never inverted. This supplies the second nontrivial root-pair configuration in type G₂, complementing the relation for its two simple roots. The conjugation form is also recorded.

References #

theorem TauCeti.integralDividedPower_mul_integralDividedPower_of_g2_short_pair {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {x y z w s : A} (M : S) (hxy : x * y = y * x + 2 • z) (hxz : x * z = z * x + 3 • w) (hzy : z * y = y * z + 3 • s) (hxw : Commute x w) (hxs : Commute x s) (hys : Commute y s) (hzw : Commute z w) (hzs : Commute z s) (hws : Commute w s) (hMx : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n x • a ∈ M) (hMy : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n y • a ∈ M) (hMz : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n z • a ∈ M) (hMw : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n w • a ∈ M) (hMs : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n s • a ∈ M) (m n : ℕ) :
integralDividedPower x M m ⋯ * integralDividedPower y M n ⋯ = ∑ p ∈ Associative.g2ShortPairIndex m n, (2 ^ p.1 * 3 ^ (p.2.1 + p.2.2)) • (integralDividedPower y M (n - p.1 - p.2.1 - 2 * p.2.2) ⋯ * integralDividedPower z M p.1 ⋯ * integralDividedPower w M p.2.1 ⋯ * integralDividedPower s M p.2.2 ⋯ * integralDividedPower x M (m - p.1 - 2 * p.2.1 - p.2.2) ⋯)

The short-pair straightening rule on a subgroup stable under divided powers, with the Chevalley coefficients 2ᵇ 3ᶜ⁺ᵈ retained as natural-number scalar multiples.

theorem TauCeti.baseChangeExp_mul_baseChangeExp_of_g2_short_pair {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] {x y z w s : A} (M : S) (hxy : x * y = y * x + 2 • z) (hxz : x * z = z * x + 3 • w) (hzy : z * y = y * z + 3 • s) (hxw : Commute x w) (hxs : Commute x s) (hys : Commute y s) (hzw : Commute z w) (hzs : Commute z s) (hws : Commute w s) (hx : IsNilpotent x) (hy : IsNilpotent y) (hz : IsNilpotent z) (hMx : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n x • a ∈ M) (hMy : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n y • a ∈ M) (hMz : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n z • a ∈ M) (hMw : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n w • a ∈ M) (hMs : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n s • a ∈ M) (t u : R) :
baseChangeExp x M hMx t * baseChangeExp y M hMy u = baseChangeExp y M hMy u * baseChangeExp z M hMz (2 * t * u) * baseChangeExp w M hMw (3 * t ^ 2 * u) * baseChangeExp s M hMs (3 * t * u ^ 2) * baseChangeExp x M hMx t

The Chevalley exponential relation for α, α + β in type G₂, over any commutative parameter ring. Only x, y, and z need explicit nilpotency hypotheses: the central commutator relations force nilpotency of w and s.

theorem TauCeti.baseChangeExp_conj_of_g2_short_pair {A : Type u_1} [Ring A] [Algebra ℚ A] {V : Type u} [AddCommGroup V] [Module A V] {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] {R : Type v} [CommRing R] [Algebra ℤ R] {x y z w s : A} (M : S) (hxy : x * y = y * x + 2 • z) (hxz : x * z = z * x + 3 • w) (hzy : z * y = y * z + 3 • s) (hxw : Commute x w) (hxs : Commute x s) (hys : Commute y s) (hzw : Commute z w) (hzs : Commute z s) (hws : Commute w s) (hx : IsNilpotent x) (hy : IsNilpotent y) (hz : IsNilpotent z) (hMx : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n x • a ∈ M) (hMy : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n y • a ∈ M) (hMz : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n z • a ∈ M) (hMw : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n w • a ∈ M) (hMs : ∀ (n : ℕ), ∀ a ∈ M, Associative.dividedPower n s • a ∈ M) (t u : R) :
baseChangeExp x M hMx t * baseChangeExp y M hMy u * baseChangeExp x M hMx (-t) = baseChangeExp y M hMy u * baseChangeExp z M hMz (2 * t * u) * baseChangeExp w M hMw (3 * t ^ 2 * u) * baseChangeExp s M hMs (3 * t * u ^ 2)

Conjugating the short-pair root subgroup of y by that of x produces the three additional root factors with parameters 2tu, 3t²u, and 3tu².