Divided powers in associative algebras

For an element x of an associative algebra over ℚ, its n-th divided power is

x⁽ⁿ⁾ = xⁿ / n!.

Unlike Mathlib's DividedPowers.RatAlgebra.dpow, this definition does not require the ambient algebra to be commutative. This is the form used by the Kostant integral form of a universal enveloping algebra. The multiplication and commuting-sum formulas below show why these rational elements can generate an integral algebra and a coalgebra: their structure constants are integers.

The Chevalley--Demazure construction starts from divided powers of Chevalley root vectors in the generally noncommutative universal enveloping algebra.

Main definitions and results

• TauCeti.Associative.dividedPower: the normalized power x ^ n / n!.
• TauCeti.Associative.mul_dividedPower_eq_dividedPower_mul_add_zsmul: moving an element past a divided power of an integer-eigenvector for its commutator.
• TauCeti.Associative.mul_dividedPower: products of divided powers of one element have a binomial coefficient as structure constant.
• TauCeti.Associative.dividedPower_add: divided powers turn a sum of commuting elements into an antidiagonal sum.
• TauCeti.Associative.dividedPower_sub: the corresponding signed expansion for a difference.
• TauCeti.Associative.map_dividedPower: divided powers are natural under algebra homomorphisms.
• TauCeti.Associative.dividedPower_apply_mem_of_pow_two_eq_zero: a square-zero endomorphism preserving a set containing zero has all divided powers preserving it.
• TauCeti.Associative.dividedPower_units_conj: divided powers are equivariant for conjugation by a unit.

References

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

noncomputable def TauCeti.Associative.dividedPower {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : A

The n-th divided power xⁿ / n! of an element of an associative ℚ-algebra.

The scalar is placed through the ℚ-algebra structure, so this definition applies to noncommutative algebras such as universal enveloping algebras.

Equations

• TauCeti.Associative.dividedPower n x = (↑n.factorial)⁻¹ • x ^ n

theorem TauCeti.Associative.dividedPower_def {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : dividedPower n x = (↑n.factorial)⁻¹ • x ^ n

The defining equation of dividedPower, for consumers that need to normalize it.

@[simp]

theorem TauCeti.Associative.dividedPower_zero {A : Type u_1} [Semiring A] [Algebra ℚ A] (x : A) : dividedPower 0 x = 1

@[simp]

theorem TauCeti.Associative.dividedPower_one {A : Type u_1} [Semiring A] [Algebra ℚ A] (x : A) : dividedPower 1 x = x

@[simp]

theorem TauCeti.Associative.dividedPower_eval_zero {A : Type u_1} [Semiring A] [Algebra ℚ A] {n : ℕ} (hn : n ≠ 0) : dividedPower n 0 = 0

theorem TauCeti.Associative.dividedPower_apply {V : Type u_2} [AddCommGroup V] [Module ℚ V] (f : Module.End ℚ V) (n : ℕ) (v : V) : dividedPower n f • v = (↑n.factorial)⁻¹ • (f ^ n) v

Evaluate a divided power of a rational endomorphism on a vector.

theorem TauCeti.Associative.dividedPower_apply_eq_zero_iff {V : Type u_2} [AddCommGroup V] [Module ℚ V] (f : Module.End ℚ V) (n : ℕ) (v : V) : dividedPower n f • v = 0 ↔ (f ^ n) v = 0

A divided power vanishes on a vector exactly when the ordinary power does.

theorem TauCeti.Associative.pow_succ_apply_eq_zero_of_dividedPower_apply_eq_zero {V : Type u_2} [AddCommGroup V] [Module ℚ V] (f : Module.End ℚ V) (n : ℕ) (v : V) (h : dividedPower n f • v = 0) : (f ^ (n + 1)) v = 0

If a divided power annihilates a vector, so does the next ordinary power.

theorem TauCeti.Associative.dividedPower_apply_mem_of_pow_eq_zero {V : Type u_2} [AddCommGroup V] [Module ℚ V] (f : Module.End ℚ V) (N : Set V) (hzero : 0 ∈ N) (d : ℕ) (hf : f ^ d = 0) (hN : ∀ k < d, ∀ {v : V}, v ∈ N → (dividedPower k f) v ∈ N) (n : ℕ) {v : V} (hv : v ∈ N) : (dividedPower n f) v ∈ N

Divided powers of a nilpotent endomorphism preserve a set containing zero if all terms below the nilpotency bound preserve it.

theorem TauCeti.Associative.dividedPower_apply_mem_of_pow_two_eq_zero {V : Type u_2} [AddCommGroup V] [Module ℚ V] (f : Module.End ℚ V) (N : Set V) (hzero : 0 ∈ N) (hf : f ^ 2 = 0) (hN : ∀ {v : V}, v ∈ N → f v ∈ N) (n : ℕ) {v : V} (hv : v ∈ N) : (dividedPower n f) v ∈ N

Every divided power of a square-zero endomorphism preserves a set containing zero once the endomorphism itself does.

theorem TauCeti.Associative.factorial_smul_dividedPower_eq_pow {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : ↑n.factorial • dividedPower n x = x ^ n

Multiplying a divided power by its factorial recovers the ordinary power.

@[simp]

theorem TauCeti.Associative.map_dividedPower {A : Type u_1} [Semiring A] [Algebra ℚ A] {B : Type u_2} [Semiring B] [Algebra ℚ B] {F : Type u_3} [FunLike F A B] [AlgHomClass F ℚ A B] (f : F) (n : ℕ) (x : A) : f (dividedPower n x) = dividedPower n (f x)

Divided powers are preserved by homomorphisms of associative ℚ-algebras.

theorem TauCeti.Associative.dividedPower_mul_left {A : Type u_1} [Semiring A] [Algebra ℚ A] {a x : A} (hax : Commute a x) (n : ℕ) : dividedPower n (a * x) = a ^ n * dividedPower n x

Multiplying an element on the left by a commuting element multiplies its n-th divided power by the n-th power of that element.

@[simp]

theorem TauCeti.Associative.dividedPower_smul {A : Type u_1} [Semiring A] [Algebra ℚ A] (q : ℚ) (n : ℕ) (x : A) : dividedPower n (q • x) = q ^ n • dividedPower n x

Scaling an element scales its n-th divided power by the n-th power of the scalar.

@[simp]

theorem TauCeti.Associative.dividedPower_units_conj {A : Type u_1} [Semiring A] [Algebra ℚ A] (u : Aˣ) (n : ℕ) (x : A) : dividedPower n (↑u * x * ↑u⁻¹) = ↑u * dividedPower n x * ↑u⁻¹

Divided powers are equivariant for conjugation by a unit.

Conjugation is an algebra automorphism, so it commutes with the rational scalar as well as with the power. This is what lets a Chevalley group element move past a root subgroup.

theorem TauCeti.Associative.commute_dividedPower_dividedPower {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y : A} (hxy : Commute x y) (m n : ℕ) : Commute (dividedPower m x) (dividedPower n y)

Divided powers preserve commutation of their underlying elements.

@[simp]

theorem Commute.dividedPower_right {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y : A} (hxy : Commute x y) (n : ℕ) : Commute x (TauCeti.Associative.dividedPower n y)

An element commuting with y commutes with every divided power of y. This is the case m = 1 of commute_dividedPower_dividedPower.

theorem TauCeti.Associative.mul_dividedPower {A : Type u_1} [Semiring A] [Algebra ℚ A] (m n : ℕ) (x : A) : dividedPower m x * dividedPower n x = (m + n).choose m • dividedPower (m + n) x

Products of divided powers of the same element have integral structure constants: x⁽ᵐ⁾ x⁽ⁿ⁾ = choose (m + n) m • x⁽ᵐ⁺ⁿ⁾.

theorem TauCeti.Associative.dividedPower_mul_self {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : dividedPower n x * x = (n + 1) • dividedPower (n + 1) x

The right-handed first-order recurrence for divided powers.

theorem TauCeti.Associative.self_mul_dividedPower {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : x * dividedPower n x = (n + 1) • dividedPower (n + 1) x

The left-handed first-order recurrence for divided powers.

theorem TauCeti.Associative.succ_nsmul_dividedPower_succ_mul {A : Type u_1} [Semiring A] [Algebra ℚ A] (m : ℕ) (x z : A) : (m + 1) • (dividedPower (m + 1) x * z) = x * (dividedPower m x * z)

Raising the left divided power, scaled. Multiplying by x on the left turns x^[m] · z into m + 1 copies of x^[m+1] · z, for any z.

theorem TauCeti.Associative.dividedPower_succ {A : Type u_1} [Semiring A] [Algebra ℚ A] (n : ℕ) (x : A) : dividedPower (n + 1) x = (↑(n + 1))⁻¹ • (dividedPower n x * x)

The first-order recurrence solved for the successor divided power.

theorem TauCeti.Associative.dividedPower_comp {A : Type u_1} [Semiring A] [Algebra ℚ A] (m n : ℕ) (hn : n ≠ 0) (x : A) : dividedPower m (dividedPower n x) = m.uniformBell n • dividedPower (m * n) x

Iterating divided powers has the integral uniform-Bell-number structure constant.

theorem TauCeti.Associative.dividedPower_add {A : Type u_1} [Semiring A] [Algebra ℚ A] {x y : A} (hxy : Commute x y) (n : ℕ) : dividedPower n (x + y) = ∑ ij ∈ Finset.antidiagonal n, dividedPower ij.1 x * dividedPower ij.2 y

The divided-power binomial formula for commuting elements of an associative algebra: (x + y)⁽ⁿ⁾ = ∑ i+j=n x⁽ⁱ⁾ y⁽ʲ⁾.

This is the coalgebra formula used for primitive elements: after applying a comultiplication with Δ(x) = x ⊗ 1 + 1 ⊗ x, the two summands commute.

theorem TauCeti.Associative.mul_dividedPower_eq_dividedPower_mul_add_zsmul {A : Type u_1} [Ring A] [Algebra ℚ A] {x y : A} {c : ℤ} (hxy : x * y - y * x = c • y) (n : ℕ) : x * dividedPower n y = dividedPower n y * x + (↑n * c) • dividedPower n y

Moving an element past a divided power of an integer-eigenvector for its commutator adds the same integral multiple of that divided power.

theorem TauCeti.Associative.mul_dividedPower_eq_dividedPower_mul_add_intCast {A : Type u_1} [Ring A] [Algebra ℚ A] {x y : A} {c : ℤ} (hxy : x * y - y * x = c • y) (n : ℕ) : x * dividedPower n y = dividedPower n y * (x + ↑c * ↑n)

The shifted-factor form of mul_dividedPower_eq_dividedPower_mul_add_zsmul.

theorem TauCeti.Associative.dividedPower_zsmul {A : Type u_1} [Ring A] [Algebra ℚ A] (d : ℤ) (n : ℕ) (x : A) : dividedPower n (d • x) = d ^ n • dividedPower n x

Scaling an element by an integer scales its n-th divided power by the n-th power of that integer. This is the integral companion of dividedPower_smul, and is what lets a Chevalley structure constant be moved from a root vector to the parameter of its exponential.

This is deliberately not a simp lemma: zsmul_eq_mul rewrites the argument d • x of the left-hand side to ↑d * x, so the statement is not in simp-normal form.

@[simp]

theorem TauCeti.Associative.dividedPower_neg {A : Type u_1} [Ring A] [Algebra ℚ A] (n : ℕ) (x : A) : dividedPower n (-x) = (-1) ^ n • dividedPower n x

Divided powers of a negated element acquire the expected sign.

theorem TauCeti.Associative.dividedPower_sub {A : Type u_1} [Ring A] [Algebra ℚ A] {x y : A} (hxy : Commute x y) (n : ℕ) : dividedPower n (x - y) = ∑ ij ∈ Finset.antidiagonal n, (-1) ^ ij.2 • (dividedPower ij.1 x * dividedPower ij.2 y)

The signed divided-power binomial formula for commuting elements of an associative algebra.

theorem TauCeti.Associative.dividedPower_eq_dpow {R : Type u_1} [CommSemiring R] [Algebra ℚ R] {I : Ideal R} (hI : DividedPowers I) (n : ℕ) {x : R} (hx : x ∈ I) : dividedPower n x = hI.dpow n x

In a commutative ℚ-algebra, dividedPower agrees with every Mathlib divided-power structure on each element of its ideal.