Polarization in a symmetric algebra

Let V be a finite-dimensional vector space over a field K of characteristic zero. The symmetric algebra S(V*) of its dual is the algebra of polynomial functions on V: a vector v evaluates p : S(V*) through SymmetricAlgebra.lift (Module.Dual.eval K V v). Call a set S ⊆ V polynomially dense when the only polynomial function vanishing at every point of S is zero.

The n-th powers v ^ n of the vectors of a polynomially dense set span the whole degree-n component of S(V). This is the coordinate-free form of TauCeti.MvPolynomial.span_sum_smul_X_pow_eq_homogeneousSubmodule, to which it is reduced by a basis of V and its dual basis: the first identifies S(V) with a polynomial ring in which v ^ n becomes the n-th power of the linear form with the coordinates of v, and the second identifies the polynomial functions on V with polynomials in those coordinates.

Main results

• TauCeti.SymmetricAlgebra.span_pow_eq_homogeneous_of_polynomial_vanishing: the n-th powers of the vectors of a polynomially dense set span the degree-n component of S(V).
• TauCeti.SymmetricAlgebra.span_pow_eq_homogeneousSubmodule: the n-th powers of all vectors span it, for a space V of any dimension.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §23.1.

theorem TauCeti.SymmetricAlgebra.span_pow_eq_homogeneous_of_polynomial_vanishing {K : Type u_1} {V : Type u_2} [Field K] [CharZero K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (S : Set V) (hS : ∀ (p : SymmetricAlgebra K (Module.Dual K V)), (∀ v ∈ S, (SymmetricAlgebra.lift ((Module.Dual.eval K V) v)) p = 0) → p = 0) (n : ℕ) : Submodule.span K ((fun (v : V) => (SymmetricAlgebra.ι K V) v ^ n) '' S) = homogeneousSubmodule K V n

Polarization. Over a field of characteristic zero, let S be a polynomially dense subset of a finite-dimensional space V: the only polynomial function p : S(V*) vanishing at every point of S is zero. Then the n-th powers of the vectors of S span the degree-n component of the symmetric algebra S(V).

theorem TauCeti.SymmetricAlgebra.span_pow_eq_homogeneousSubmodule {K : Type u_1} {V : Type u_2} [Field K] [CharZero K] [AddCommGroup V] [Module K V] (n : ℕ) : Submodule.span K (Set.range fun (v : V) => (SymmetricAlgebra.ι K V) v ^ n) = homogeneousSubmodule K V n

The n-th powers span Sⁿ(V). Over a field of characteristic zero, the n-th powers of all vectors of V span the degree-n component of S(V). A product of n vectors lies in the symmetric algebra of their finite-dimensional span, where the whole space is polynomially dense.