Normal ordering divided powers with a central commutator

Let x, y, and z belong to an associative algebra over ℚ, with x * y = y * x + z. When z commutes with both x and y, the divided powers admit the coefficient-one normal-ordering formula

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ k ≤ min(m,n), y⁽ⁿ⁻ᵏ⁾ z⁽ᵏ⁾ x⁽ᵐ⁻ᵏ⁾.

This is the class-two case of the straightening relations used in a Kostant integral form. For a Chevalley basis it applies whenever [x, y] is a root vector and both further brackets with x and y vanish; in particular it covers non-opposite roots α and β in a simply-laced root system when α + β is a root. The coefficient-one form is the integral content: reordering the rational divided powers introduces no rational structure constants.

The preliminary one-sided formula only needs z to commute with y. The full formula additionally needs z to commute with x, because its normal form places all powers of z between those of y and x.

Both are instances of one rule without any class-two restriction. Whenever a sequence d : ℕ → A behaves like the divided powers (ad x)ᵏ(d 0) / k! of the inner derivation, in the sense that x * d k = d k * x + (k + 1) • d (k + 1), one gets

x⁽ᵐ⁾ * d 0 = ∑ k ≤ m, d k * x⁽ᵐ⁻ᵏ⁾,

again with every coefficient equal to 1. All of the structure constants of a longer root string are carried by the sequence d, so the rule stays integral exactly when its terms are. The class-two formula is the case d k = y⁽ⁿ⁻ᵏ⁾ z⁽ᵏ⁾, truncated to zero beyond k = n.

Main results

• TauCeti.Associative.mul_dividedPower_of_commutator_eq: move one element across a divided power when its commutator with the base commutes with that base.
• TauCeti.Associative.mul_dividedPower_of_commutator_eq': the same identity for an exponent that is not syntactically a successor.
• TauCeti.Associative.mul_dividedPower_mul_dividedPower_mul_of_commutator_eq_nsmul: move one element across a monomial z⁽ᵇ⁾ w⁽ᶜ⁾ t when its commutator with z is a multiple of w.
• TauCeti.Associative.dividedPower_mul_of_ad_dividedPower_series: coefficient-one normal ordering against an arbitrary divided-power series for the inner derivation.
• TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq: the coefficient-one normal-ordering formula for two divided powers with central commutator.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

theorem TauCeti.Associative.mul_dividedPower_of_commutator_eq {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z : A} (hxy : x * y = y * x + z) (hyz : Commute y z) (n : ℕ) : x * dividedPower (n + 1) y = dividedPower (n + 1) y * x + dividedPower n y * z

First-order divided-power normal ordering. If x * y = y * x + z and z commutes with y, then

x y⁽ⁿ⁺¹⁾ = y⁽ⁿ⁺¹⁾ x + y⁽ⁿ⁾ z.

Unlike the corresponding ordinary-power identity, the divided-power identity has coefficient one. No commutation hypothesis between x and z is needed for this one-sided formula.

theorem TauCeti.Associative.mul_dividedPower_of_commutator_eq' {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z : A} (hxy : x * y = y * x + z) (hyz : Commute y z) (n : ℕ) : x * dividedPower n y = dividedPower n y * x + if 0 < n then dividedPower (n - 1) y * z else 0

The form of mul_dividedPower_of_commutator_eq for an exponent that is not syntactically a successor: the commutator term is present exactly when the exponent is positive. This is the shape needed when the exponent is a summation variable.

theorem TauCeti.Associative.mul_dividedPower_mul_dividedPower_mul_of_commutator_eq_nsmul {A : Type u_1} [Semiring A] [Algebra ℚ A] {x z w t : A} {k : ℕ} (hxz : x * z = z * x + k • w) (hxw : Commute x w) (hxt : Commute x t) (hzw : Commute z w) (b c : ℕ) : x * (dividedPower b z * (dividedPower c w * t)) = dividedPower b z * (dividedPower c w * t) * x + if 0 < b then (k * (c + 1)) • (dividedPower (b - 1) z * (dividedPower (c + 1) w * t)) else 0

Moving one element across a divided-power monomial. Suppose x * z = z * x + k • w, where w commutes with x and z, and t commutes with x. Then x passes through z⁽ᵇ⁾ w⁽ᶜ⁾ t at the cost of one term, which trades a z for a w:

x z⁽ᵇ⁾ w⁽ᶜ⁾ t = z⁽ᵇ⁾ w⁽ᶜ⁾ t x + k (c + 1) z⁽ᵇ⁻¹⁾ w⁽ᶜ⁺¹⁾ t,

the second term being present exactly when b is positive. Compared with mul_dividedPower_of_commutator_eq', the released w is already absorbed into w⁽ᶜ⁺¹⁾. The factor t stands for the part of a normal-ordered monomial that x commutes with; t = 1 covers a monomial ending in w⁽ᶜ⁾.

Normal ordering against a divided-power series for the inner derivation

theorem TauCeti.Associative.dividedPower_mul_of_ad_dividedPower_series {A : Type u_1} [Semiring A] [Algebra ℚ A] {x : A} {d : ℕ → A} (hd : ∀ (k : ℕ), x * d k = d k * x + (k + 1) • d (k + 1)) (m : ℕ) : dividedPower m x * d 0 = ∑ k ∈ Finset.range (m + 1), d k * dividedPower (m - k) x

Coefficient-one normal ordering against a divided-power series. Let d : ℕ → A satisfy

x * d k = d k * x + (k + 1) • d (k + 1)

for every k, which is what the sequence k ↦ (ad x)ᵏ (d 0) / k! does. Then

x⁽ᵐ⁾ * d 0 = ∑ k ≤ m, d k * x⁽ᵐ⁻ᵏ⁾.

Every coefficient is 1: the sequence d carries all of the structure constants, so the rule is integral precisely when its terms are. The class-two formula dividedPower_mul_dividedPower_of_commutator_eq below is derived from this one as the case d k = y⁽ⁿ⁻ᵏ⁾ z⁽ᵏ⁾, truncated to zero beyond k = n; the chain β, α + β, 2α + β needs a longer sequence and nothing else.

The class-two case

theorem TauCeti.Associative.dividedPower_mul_dividedPower_of_commutator_eq {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y z : A} (hxy : x * y = y * x + z) (hxz : Commute x z) (hyz : Commute y z) (m n : ℕ) : dividedPower m x * dividedPower n y = ∑ k ∈ Finset.range (min m n + 1), dividedPower (n - k) y * dividedPower k z * dividedPower (m - k) x

Coefficient-one normal ordering for divided powers with central commutator. Suppose x * y = y * x + z, and z commutes with both x and y. Then

x⁽ᵐ⁾ y⁽ⁿ⁾ = ∑ k ≤ min(m,n), y⁽ⁿ⁻ᵏ⁾ z⁽ᵏ⁾ x⁽ᵐ⁻ᵏ⁾.

The summation is written as range (min m n + 1), so every displayed subtraction is exact. This is the integral normal-ordering rule: every coefficient in the divided-power basis is 1.

This is the classTwoSeries case of dividedPower_mul_of_ad_dividedPower_series, truncated at min m n because that sequence vanishes beyond k = n.