Documentation

TauCeti.RingTheory.DividedPowers.RootString.G2.Basic

Normal ordering divided powers along the type-G₂ root string #

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

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

v and s commuting with x, y commuting with z, w commuting with v, and s commuting with z, w, and v. This is the situation of the two simple roots of a root system of type G₂, α short and β long: with x and y the Chevalley root vectors of α and β, the divided powers (ad x)ᵏ y / k! of the inner derivation are the root vectors of α + β, 2α + β, and 3α + β up to sign, and s is the root vector of 3α + 2β. Every one of the four brackets above is integral.

The resulting straightening rule is again coefficient-one,

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ b + c + d + 2e ≤ n, b + 2c + 3d + 3e ≤ m,
              y⁽ⁿ⁻ᵇ⁻ᶜ⁻ᵈ⁻²ᵉ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ v⁽ᵈ⁾ s⁽ᵉ⁾ x⁽ᵐ⁻ᵇ⁻²ᶜ⁻³ᵈ⁻³ᵉ⁾,

so it holds in a Kostant integral form and, after base change, over a ring of any characteristic. The two exponents attached to a summand are the pair (i, j) of the root i α + j β it comes from: z contributes (1, 1), w contributes (2, 1), v contributes (3, 1), and s contributes (3, 2). That last root is what makes the type-G₂ case genuinely longer than the chain treated in TauCeti.RingTheory.DividedPowers.RootString.Basic: 3α + 2β is not on the α-string through β, and it enters through the bracket w * z = z * w + 3 • s rather than through ad x.

For the other nontrivial pair α, α + β, the root 3α + 2β arises instead from ⁅e_(2α + β), e_(α + β)⁆. Its divided-power straightening rule is TauCeti.Associative.dividedPower_mul_dividedPower_of_g2_short_pair in TauCeti.RingTheory.DividedPowers.RootString.G2.ShortPair.

The proof feeds TauCeti.Associative.dividedPower_mul_of_ad_dividedPower_series the sequence

d k = ∑ b + 2c + 3d + 3e = k,  y⁽ⁿ⁻ᵇ⁻ᶜ⁻ᵈ⁻²ᵉ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ v⁽ᵈ⁾ s⁽ᵉ⁾,

which is the k-th divided power of the inner derivation ad x applied to y⁽ⁿ⁾. Verifying its defining recurrence is the whole content: moving x across one normal-ordered monomial lengthens the z-power with coefficient b + 1, the w-power with coefficient 2 (c + 1), the v-power with coefficient 3 (d + 1), or the s-power with coefficient 3 (e + 1), and the four contributions to a summand of d (k + 1) add up to b + 2c + 3d + 3e = k + 1.

Main results #

References #

Moving one element across a power whose commutator is not central #

source
theorem TauCeti.Associative.mul_dividedPower_of_commutator_eq_two_nsmul {A : Type u_1} [Semiring A] [Algebra ℚ A] {x z a d : A} (hxz : x * z = z * x + a) (haz : a * z = z * a + 2 • d) (hzd : Commute z d) (b : ℕ) :
x * dividedPower b z = (dividedPower b z * x + if 0 < b then dividedPower (b - 1) z * a else 0) + if 1 < b then dividedPower (b - 2) z * d else 0

Moving one element across a divided power with a non-central commutator. Suppose x * z = z * x + a and a * z = z * a + 2 • d, with d commuting with z. Then

x z⁽ᵇ⁾ = z⁽ᵇ⁾ x + z⁽ᵇ⁻¹⁾ a + z⁽ᵇ⁻²⁾ d,

both released terms being present exactly when their exponent is defined. Every coefficient is 1: the factor 2 in the second hypothesis is exactly what the divided powers absorb, which is why d rather than a * z - z * a is the integral datum. Taking d = 0 recovers mul_dividedPower_of_commutator_eq'.

The bracket at the root 3α + 2β #

source
theorem TauCeti.Associative.commutator_eq_three_nsmul_of_commute {B : Type u_2} [Ring B] {x y z w v s : B} (hxy : x * y = y * x + z) (hxw : x * w = w * x + 3 • v) (hyw : Commute y w) (hyv : y * v = v * y + s) :
w * z = z * w + 3 • s

The fifth bracket is forced. In the type-G₂ configuration the bracket of the root vectors of α + β and 2α + β is not an independent datum: it is three times the root vector of 3α + 2β that already appears as ⁅y, v⁆. The proof is the Jacobi identity applied to ⁅x, ⁅y, w⁆⁆ = 0.

A consumer holding a Chevalley basis therefore supplies the four brackets along the α-string together with ⁅e_β, e_{3α+β}⁆, and reads off the hypothesis w * z = z * w + 3 • s of the straightening rule below.

Moving one element across a single normal-ordered monomial #

The divided-power series of the inner derivation #

Reindexing the four exponent shifts #

Each of the four ways to advance the series moves the index p of weighted degree k to an index of weighted degree k + 1 by a fixed shift of the exponents. All four are instances of one reindexing lemma, which leaves each of them only the arithmetic of its own shift.

The straightening rule #

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

The quadruples of exponents in the straightening rule for the type-G₂ root string, one coordinate for each of the roots α + β, 2α + β, 3α + β, and 3α + 2β.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.Associative.mem_chainG2Index {m n : ℕ} {p : ℕ × ℕ × ℕ × ℕ} :
    p ∈ chainG2Index m n ↔ p.1 + p.2.1 + p.2.2.1 + 2 * p.2.2.2 ≤ n ∧ p.1 + 2 * p.2.1 + 3 * p.2.2.1 + 3 * p.2.2.2 ≤ m

    Membership in chainG2Index in terms of its two mathematical inequalities.

    source
    theorem TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq_three_nsmul {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z w v s : A} (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : x * w = w * x + 3 • v) (hwz : w * z = z * w + 3 • s) (hxv : Commute x v) (hxs : Commute x s) (hyz : Commute y z) (hwv : Commute w v) (hzs : Commute z s) (hws : Commute w s) (hvs : Commute v s) (m n : ℕ) :
    dividedPower m x * dividedPower n y = ∑ p ∈ chainG2Index m n, dividedPower (n - p.1 - p.2.1 - p.2.2.1 - 2 * p.2.2.2) y * dividedPower p.1 z * dividedPower p.2.1 w * dividedPower p.2.2.1 v * dividedPower p.2.2.2 s * dividedPower (m - p.1 - 2 * p.2.1 - 3 * p.2.2.1 - 3 * p.2.2.2) x

    Coefficient-one normal ordering along the type-G₂ root string. Suppose

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

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

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

    Every coefficient in the divided-power basis is 1, so the identity survives restriction to a Kostant integral lattice and base change to a ring of arbitrary characteristic. Taking v = 0 and s = 0 and discarding the terms with d ≠ 0 or e ≠ 0 recovers the chain rule dividedPower_mul_dividedPower_of_commutator_eq_two_nsmul.