Documentation

TauCeti.RingTheory.MvPolynomial.Polarization

Powers of linear forms span the homogeneous polynomials #

Over a field K of characteristic zero, the n-th powers of linear forms span the space of homogeneous polynomials of degree n in finitely many variables. This file proves the sharper statement in which the linear forms are restricted to a polynomially dense set of coefficient vectors: if S ⊆ K^σ is such that only the zero polynomial vanishes at every point of S, then the powers (∑ i, x i • X i) ^ n for x ∈ S already span the degree-n homogeneous polynomials.

The argument is by duality. A linear functional φ on the polynomial ring that vanishes on all these powers defines a polynomial Q in the coordinates x, with Q (x) = φ ((∑ i, x i • X i) ^ n) for every point x; by the multinomial theorem the coefficient of Q at an exponent d of total degree n is the multinomial coefficient of d times φ (X ^ d). Since Q vanishes on S, it is zero, and since multinomial coefficients do not vanish in characteristic zero, φ kills every monomial of degree n, hence the whole homogeneous component.

This is the classical polarization argument, used for instance to show that the restrictions of the trace polynomials of the representations of a semisimple Lie algebra span the invariant polynomials on a Cartan subalgebra, where S is the set of dominant integral weights.

Main results #

References #

theorem TauCeti.MvPolynomial.span_sum_smul_X_pow_eq_homogeneousSubmodule {σ : Type u_1} [Fintype σ] {K : Type u_2} [Field K] [CharZero K] (S : Set (σ → K)) (hS : ∀ (q : MvPolynomial σ K), (∀ x ∈ S, (MvPolynomial.eval x) q = 0) → q = 0) (n : ℕ) :
Submodule.span K ((fun (x : σ → K) => (∑ i : σ, x i • MvPolynomial.X i) ^ n) '' S) = MvPolynomial.homogeneousSubmodule σ K n

Polarization. Over a field of characteristic zero, let S be a polynomially dense set of points of K^σ, in the sense that only the zero polynomial vanishes at every point of S. Then the n-th powers of the linear forms ∑ i, x i • X i with x ∈ S span the homogeneous polynomials of degree n.