Polarization for multilinear maps

The diagonal values of a multilinear map of ι arguments already determine its symmetrizations. This file proves the classical polarization identity, an inclusion-exclusion over the subsets of ι: for a multilinear map f of ι arguments and a family m of arguments, ∑_{S ⊆ ι} (-1)^{#S} f (∑_{i ∉ S} m i, …, ∑_{i ∉ S} m i) = ∑_{σ} f (m (σ ·)). Only the diagonal values of f appear on the left, and the right side is the full symmetrization of f at m.

Expanding each argument by multilinearity turns the left side into a sum over all functions g : ι → ι, weighted by ∑_{S ⊆ (range g)ᶜ} (-1)^{#S}, which vanishes unless g is onto; the surviving terms are the permutations. Nothing is inverted along the way, so the identity holds over an arbitrary ring, commutative or not.

The instance for the tensor power ⨂[R] (_ : ι), M is recorded here too: there the diagonal values are the pure powers ⨂ₜ i, x, the tensors with the same vector in every slot.

Main results

• MultilinearMap.sum_neg_one_pow_card_smul_apply_sum_compl: the polarization identity for a multilinear map.
• PiTensorProduct.sum_neg_one_pow_card_smul_tprod_sum_compl: its tensor-power instance, writing the full symmetrization of a pure tensor as an alternating sum of pure powers.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix B.1, for the polarization argument.

theorem MultilinearMap.sum_neg_one_pow_card_smul_apply_sum_compl {R : Type u} {M : Type v} {N : Type z} {ι : Type w} [Ring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Fintype ι] [DecidableEq ι] (f : (ι → M) →ₘₗ[R] N) (m : ι → M) : (∑ S : Finset ι, (-1) ^ S.card • f fun (x : ι) => ∑ i ∈ Sᶜ, m i) = ∑ σ : Equiv.Perm ι, f fun (i : ι) => m (σ i)

Polarization. For a multilinear map of ι arguments, the alternating sum over the subsets S ⊆ ι of its value on the constant family ∑_{i ∉ S} m i is the full symmetrization of its value on m. Only the diagonal values of f appear on the left, so they already determine every symmetrization; over a ring in which (#ι)! is invertible they therefore determine f on all symmetric arguments.

theorem PiTensorProduct.sum_neg_one_pow_card_smul_tprod_sum_compl {R : Type u} {M : Type v} {ι : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (m : ι → M) : (∑ S : Finset ι, (-1) ^ S.card • (tprod R) fun (x : ι) => ∑ i ∈ Sᶜ, m i) = ∑ σ : Equiv.Perm ι, (tprod R) fun (i : ι) => m (σ i)

Polarization for tensor powers. The full symmetrization of a pure tensor is an alternating sum of pure powers ⨂ₜ i, x.