Homogeneous symmetric polynomials in a basis

A basis identifies a symmetric algebra with a multivariate polynomial ring. This file records that the equivalence sends a generator to the linear form with the same coordinates, and that it carries each homogeneous submodule of the symmetric algebra to the corresponding total-degree submodule of the polynomial ring.

Main results

• SymmetricAlgebra.equivMvPolynomial_ι: the basis-induced equivalence sends the generator of x to the linear form ∑ᵢ (b.repr x i) Xᵢ.
• map_homogeneousSubmodule_equivMvPolynomial: the basis-induced equivalence carries the degree n part of a symmetric algebra to the degree n part of a multivariate polynomial ring.
• SymmetricAlgebra.equivMvPolynomial_isHomogeneous_iff: the degreewise form of that comparison.

@[simp]

theorem SymmetricAlgebra.equivMvPolynomial_ι {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type w} (b : Module.Basis ι R M) (x : M) : (equivMvPolynomial b) ((SymmetricAlgebra.ι R M) x) = ((b.constr R) MvPolynomial.X) x

The algebra equivalence induced by a basis sends the generator of x to the linear form with the coordinates of x.

@[simp]

theorem TauCeti.SymmetricAlgebra.map_homogeneousSubmodule_equivMvPolynomial (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type w} (b : Module.Basis ι R M) (n : ℕ) : Submodule.map (SymmetricAlgebra.equivMvPolynomial b).toLinearMap (homogeneousSubmodule R M n) = MvPolynomial.homogeneousSubmodule ι R n

The algebra equivalence induced by a basis preserves homogeneous degree.

@[simp]

theorem SymmetricAlgebra.equivMvPolynomial_isHomogeneous_iff (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type w} (b : Module.Basis ι R M) (n : ℕ) (p : SymmetricAlgebra R M) : ((equivMvPolynomial b) p).IsHomogeneous n ↔ p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n

An element of a symmetric algebra is homogeneous of degree n exactly when its image under the polynomial equivalence induced by a basis is.