Evaluations of elements of a symmetric algebra

Let M be a free module over an infinite integral domain R. Every linear form f : M → R extends to the evaluation SymmetricAlgebra.lift f : S(M) →ₐ[R] R, and an element of S(M) is a polynomial function on the dual of M through these evaluations. This file shows that the function determines the element: two elements of S(M) with the same value at every linear form are equal. In a basis of M, S(M) is a polynomial algebra (SymmetricAlgebra.equivMvPolynomial) and the evaluations are the evaluations of polynomials at all points, which separate polynomials over an infinite domain (MvPolynomial.funext).

The function is polynomial in the usual sense along every affine line of linear forms, over any commutative ring and without freeness: for p : S(M) and linear forms f, g, the values SymmetricAlgebra.lift (f + t • g) p are the values at t of one polynomial in R[X], namely the image of p under the evaluation at the R[X]-valued linear form f + X • g. Over a domain, this is how an identity between two such functions known at infinitely many points of a line is extended to the whole line.

For a Cartan subalgebra H of a semisimple Lie algebra, S(H) is the algebra of polynomial functions on the weights H*, and this is how an identity in S(H) is checked one weight at a time.

Main results

• SymmetricAlgebra.exists_polynomial_eval_eq_lift_add_smul: along an affine line of linear forms, the evaluations of an element of S(M) are the values of a polynomial.
• TauCeti.SymmetricAlgebra.eq_of_forall_lift_apply_eq: two elements of S(M) on which every evaluation SymmetricAlgebra.lift f agrees are equal.

theorem SymmetricAlgebra.exists_polynomial_eval_eq_lift_add_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (p : SymmetricAlgebra R M) (f g : M →ₗ[R] R) : ∃ (q : Polynomial R), ∀ (t : R), Polynomial.eval t q = (lift (f + t • g)) p

An element of the symmetric algebra is a polynomial function along every affine line of linear forms: for p : S(M) and linear forms f, g there is a polynomial q with q.eval t = SymmetricAlgebra.lift (f + t • g) p for every t : R.

theorem TauCeti.SymmetricAlgebra.eq_of_forall_lift_apply_eq {R : Type u_1} {M : Type u_2} [CommRing R] [IsDomain R] [Infinite R] [AddCommGroup M] [Module R M] [Module.Free R M] {p q : SymmetricAlgebra R M} (h : ∀ (f : Module.Dual R M), (SymmetricAlgebra.lift f) p = (SymmetricAlgebra.lift f) q) : p = q

An element of the symmetric algebra of a free module over an infinite domain is determined by its values at all linear forms: if SymmetricAlgebra.lift f p = SymmetricAlgebra.lift f q for every f : Module.Dual R M, then p = q.