Powers of a sum of commuting square-zero elements

Let x i be pairwise commuting elements of a semiring with x i * x i = 0. In the multinomial expansion of (∑ i ∈ s, x i) ^ n every monomial with a repeated factor vanishes, and each product of n distinct factors occurs n ! times, once for each ordering. Hence

(∑ i ∈ s, x i) ^ n = n ! • ∑_{t ⊆ s, #t = n} ∏_{i ∈ t} x i,

so (∑ i ∈ s, x i) ^ n is n ! times an explicit element with no denominators: the elementary symmetric sum is a divided power (∑ i ∈ s, x i) ^ n / n ! over any base, including ℤ.

These elementary symmetric sums e k = ∑_{t ⊆ s, #t = k} ∏_{i ∈ t} x i multiply like divided powers, e m * e n = (m + n).choose m • e (m + n), again with no division by factorials.

Main results

• Finset.sum_pow_of_commute_of_mul_self_eq_zero: the displayed formula, with the product over t the noncommutative product Finset.noncommProd of the pairwise commuting family.
• Finset.sum_pow_of_pairwise_commute_of_mul_self_eq_zero: the same formula as a sum over s.powersetCard n, for a family commuting pairwise everywhere.
• Finset.sum_noncommProd_powersetCard_mul_of_commute_of_mul_self_eq_zero: e m * e n = (m + n).choose m • e (m + n), and Finset.sum_noncommProd_powersetCard_mul_of_pairwise_commute_of_mul_self_eq_zero, the same identity as sums over powersetCard for a family commuting pairwise everywhere.

theorem Finset.sum_pow_of_pairwise_commute_of_mul_self_eq_zero {R : Type u_1} [Semiring R] {ι : Type u_2} (s : Finset ι) (x : ι → R) (hc : Pairwise (Function.onFun Commute x)) (hx : ∀ i ∈ s, x i * x i = 0) (n : ℕ) : (∑ i ∈ s, x i) ^ n = n.factorial • ∑ t ∈ powersetCard n s, t.noncommProd x ⋯

The multinomial theorem for square-zero elements, for a family commuting pairwise everywhere: (∑ i ∈ s, x i) ^ n is n ! times the sum, over the n-element subsets t of s, of the products of the x i with i ∈ t.

theorem Finset.sum_pow_of_commute_of_mul_self_eq_zero {R : Type u_1} [Semiring R] {ι : Type u_2} (s : Finset ι) (x : ι → R) (hc : (↑s).Pairwise (Function.onFun Commute x)) (hx : ∀ i ∈ s, x i * x i = 0) (n : ℕ) : (∑ i ∈ s, x i) ^ n = n.factorial • ∑ t : ↥(powersetCard n s), (↑t).noncommProd x ⋯

Multinomial theorem for square-zero elements. If the x i commute pairwise and square to zero on s, then (∑ i ∈ s, x i) ^ n is n ! times the sum, over the n-element subsets t of s, of the products of the x i with i ∈ t.

theorem Finset.sum_noncommProd_powersetCard_mul_of_pairwise_commute_of_mul_self_eq_zero {R : Type u_1} [Semiring R] {ι : Type u_2} (s : Finset ι) (x : ι → R) (hc : Pairwise (Function.onFun Commute x)) (hx : ∀ i ∈ s, x i * x i = 0) (m n : ℕ) : (∑ t ∈ powersetCard m s, t.noncommProd x ⋯) * ∑ t ∈ powersetCard n s, t.noncommProd x ⋯ = (m + n).choose m • ∑ t ∈ powersetCard (m + n) s, t.noncommProd x ⋯

Multiplication of elementary symmetric sums of square-zero elements, for a family commuting pairwise everywhere: if the x i square to zero on s, then the sums e k of the products over the k-element subsets of s satisfy e m * e n = (m + n).choose m • e (m + n).

theorem Finset.sum_noncommProd_powersetCard_mul_of_commute_of_mul_self_eq_zero {R : Type u_1} [Semiring R] {ι : Type u_2} (s : Finset ι) (x : ι → R) (hc : (↑s).Pairwise (Function.onFun Commute x)) (hx : ∀ i ∈ s, x i * x i = 0) (m n : ℕ) : (∑ t : ↥(powersetCard m s), (↑t).noncommProd x ⋯) * ∑ t : ↥(powersetCard n s), (↑t).noncommProd x ⋯ = (m + n).choose m • ∑ t : ↥(powersetCard (m + n) s), (↑t).noncommProd x ⋯

Multiplication of elementary symmetric sums of square-zero elements. If the x i commute pairwise and square to zero on s, then the sums e k of the products over the k-element subsets of s satisfy e m * e n = (m + n).choose m • e (m + n): they are the divided powers of e 1 = ∑ i ∈ s, x i, with no division by factorials.