Normal ordering divided powers for the short pair in type G₂

Let x, y, z, w, and s belong to an associative algebra over ℚ, with

x * y = y * x + 2 • z,   x * z = z * x + 3 • w,   z * y = y * z + 3 • s,

w and s commuting with x, s commuting with y, and z, w, s commuting pairwise. This is the second configuration of positive roots in type G₂: if x and y are the root vectors of α and α + β, respectively, then z, w, and s belong to the root spaces of 2α + β, 3α + β, and 3α + 2β. The last root has coordinates (1, 2) relative to the pair α, α + β, and enters through the bracket of z with y.

For these canonically normalized Chevalley root vectors, the resulting straightening rule is

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ b + c + 2d ≤ n, b + 2c + d ≤ m,
              2ᵇ 3ᶜ⁺ᵈ • y⁽ⁿ⁻ᵇ⁻ᶜ⁻²ᵈ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ s⁽ᵈ⁾ x⁽ᵐ⁻ᵇ⁻²ᶜ⁻ᵈ⁾.

Its displayed coefficients are natural numbers. Together with TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq_three_nsmul, this covers the two nontrivial normal-ordering configurations needed for type G₂.

Main results

• TauCeti.Associative.dividedPower_mul_dividedPower_of_g2_short_pair_scaled: the coefficient-one straightening rule for scaled short-pair root vectors.
• TauCeti.Associative.dividedPower_mul_dividedPower_of_g2_short_pair: the Chevalley-basis straightening rule for the pair α, α + β in type G₂.

References

• R. W. Carter, Simple Groups of Lie Type, §4.2 and Theorem 5.2.2.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

Moving one element across a normal-ordered monomial

The divided-power series of the inner derivation

The straightening rule

def TauCeti.Associative.g2ShortPairIndex (m n : ℕ) : Finset (ℕ × ℕ × ℕ)

The triples of exponents in the short-pair straightening rule for type G₂, corresponding to the roots 2α + β, 3α + β, and 3α + 2β.

Equations

• TauCeti.Associative.g2ShortPairIndex m n = {p ∈ Finset.range (n + 1) ×ˢ Finset.range (n + 1) ×ˢ Finset.range (n + 1) | p.1 + p.2.1 + 2 * p.2.2 ≤ n ∧ p.1 + 2 * p.2.1 + p.2.2 ≤ m}

@[simp]

theorem TauCeti.Associative.mem_g2ShortPairIndex {m n : ℕ} {p : ℕ × ℕ × ℕ} : p ∈ g2ShortPairIndex m n ↔ p.1 + p.2.1 + 2 * p.2.2 ≤ n ∧ p.1 + 2 * p.2.1 + p.2.2 ≤ m

Membership in g2ShortPairIndex in terms of its two mathematical inequalities.

theorem TauCeti.Associative.dividedPower_mul_dividedPower_of_g2_short_pair_scaled {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z w s : A} (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hzy : z * y = y * z + 2 • 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) (m n : ℕ) : dividedPower m x * dividedPower n y = ∑ p ∈ g2ShortPairIndex m n, dividedPower (n - p.1 - p.2.1 - 2 * p.2.2) y * dividedPower p.1 z * dividedPower p.2.1 w * dividedPower p.2.2 s * dividedPower (m - p.1 - 2 * p.2.1 - p.2.2) x

Coefficient-one normal ordering for scaled short-pair root vectors in type G₂. The bracket constants are 1, 2, 2: x * y = y * x + z, x * z = z * x + 2 • w, and z * y = y * z + 2 • s. Assume also that w and s commute with x, that s commutes with y, and that z, w, s commute pairwise. Then every coefficient in the displayed divided-power expansion is 1.

For Chevalley root vectors with bracket constants 2, 3, 3, apply this identity to 2 • z, 3 • w, and 3 • s; see dividedPower_mul_dividedPower_of_g2_short_pair.

theorem TauCeti.Associative.dividedPower_mul_dividedPower_of_g2_short_pair {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z w s : A} (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) (m n : ℕ) : dividedPower m x * dividedPower n y = ∑ p ∈ g2ShortPairIndex m n, (2 ^ p.1 * 3 ^ (p.2.1 + p.2.2)) • (dividedPower (n - p.1 - p.2.1 - 2 * p.2.2) y * dividedPower p.1 z * dividedPower p.2.1 w * dividedPower p.2.2 s * dividedPower (m - p.1 - 2 * p.2.1 - p.2.2) x)

Chevalley-basis normal ordering for the short pair in type G₂. Suppose

x * y = y * x + 2 • z,   x * z = z * x + 3 • w,   z * y = y * z + 3 • s,

that w and s commute with x, s commutes with y, and z, w, s commute pairwise. Then

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ b + c + 2d ≤ n, b + 2c + d ≤ m,
              2ᵇ 3ᶜ⁺ᵈ • y⁽ⁿ⁻ᵇ⁻ᶜ⁻²ᵈ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ s⁽ᵈ⁾ x⁽ᵐ⁻ᵇ⁻²ᶜ⁻ᵈ⁾.

Here x, y, z, w, and s model Chevalley root vectors for α, α + β, 2α + β, 3α + β, and 3α + 2β, respectively. The powers of 2 and 3 are the structure constants introduced by passing from the scaled vectors 2 • z, 3 • w, and 3 • s back to the Chevalley basis. In particular, every displayed coefficient is a natural number.