Documentation

TauCeti.RingTheory.DividedPowers.RootString.Basic

Normal ordering divided powers along the chain β, α + β, 2α + β #

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

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

w commuting with x, y commuting with z, and z commuting with w. This is the situation of two roots α, β for which α + β and 2α + β are roots while 3α + β and α + 2β are not: with x and y the root vectors of α and β in a Chevalley basis, z is N_{α β} times the root vector of α + β, and the second divided power (ad x)² y / 2 of the inner derivation is again an integral multiple w of the root vector of 2α + β.

The resulting straightening rule is again coefficient-one,

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ b + c ≤ n, b + 2c ≤ m,  y⁽ⁿ⁻ᵇ⁻ᶜ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ x⁽ᵐ⁻ᵇ⁻²ᶜ⁾,

so it holds in a Kostant integral form and, after base change, over a ring of any characteristic. The class-two rule TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq is the degenerate case w = 0, and covers every pair of non-proportional roots in a simply-laced root system; the rule proved here covers the additional chains in types B, C, and F₄. Type G₂ also needs the longer chain containing 3α + β and 3α + 2β, which is TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq_three_nsmul in TauCeti.RingTheory.DividedPowers.RootString.G2.Basic.

The proof feeds TauCeti.Associative.dividedPower_mul_of_ad_dividedPower_series the sequence

d k = ∑ b + 2c = k,  y⁽ⁿ⁻ᵇ⁻ᶜ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾,

which is the k-th divided power of the inner derivation ad x applied to y⁽ⁿ⁾. Verifying the defining recurrence of that sequence is the whole content: moving x across one summand either lengthens the z-power, with coefficient b + 1, or lengthens the w-power, with coefficient 2 (c + 1), and the two contributions to a summand of d (k + 1) add up to b + 2c = k + 1.

Main results #

References #

Moving one element across a single normal-ordered monomial #

The divided-power series of the inner derivation #

The straightening rule #

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

The pairs of exponents in the straightening rule for the chain β, α + β, 2α + β.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Associative.mem_chainLeTwoIndex {m n : ℕ} {p : ℕ × ℕ} :
    p ∈ chainLeTwoIndex m n ↔ p.1 + p.2 ≤ n ∧ p.1 + 2 * p.2 ≤ m

    Membership in chainLeTwoIndex in terms of its two mathematical inequalities.

    source
    theorem TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq_two_nsmul {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z w : A} (hxy : x * y = y * x + z) (hxz : x * z = z * x + 2 • w) (hxw : Commute x w) (hyz : Commute y z) (hzw : Commute z w) (m n : ℕ) :
    dividedPower m x * dividedPower n y = ∑ p ∈ chainLeTwoIndex m n, dividedPower (n - p.1 - p.2) y * dividedPower p.1 z * dividedPower p.2 w * dividedPower (m - p.1 - 2 * p.2) x

    Coefficient-one normal ordering along the chain β, α + β, 2α + β. Suppose

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

    that w commutes with x, y commutes with z, and z commutes with w. Then

    x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ b + c ≤ n, b + 2c ≤ m,  y⁽ⁿ⁻ᵇ⁻ᶜ⁾ z⁽ᵇ⁾ w⁽ᶜ⁾ 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 w = 0 and discarding the terms with c ≠ 0 recovers the class-two rule dividedPower_mul_dividedPower_of_commutator_eq.