The submodules of polynomials of bounded total degree

Mathlib's MvPolynomial.restrictTotalDegree σ R m is the submodule of polynomials of total degree at most m. This file records that these submodules increase with m, that a monomial of degree at most m lies in the m-th one, and that the m-th one is spanned by those monomials, so that a linear statement about polynomials of bounded degree reduces to monomials.

Main results

• MvPolynomial.restrictTotalDegree_mono: the submodules increase with the degree bound.
• MvPolynomial.monomial_mem_restrictTotalDegree: a monomial of degree at most m has total degree at most m.
• MvPolynomial.restrictTotalDegree_eq_span: the monomials of degree at most m span the polynomials of total degree at most m.
• TauCeti.MvPolynomial.apply_mem_of_basis: a bilinear map takes values in a submodule on bounded-degree polynomials if it does so on basis vectors and bounded-degree monomials.

theorem MvPolynomial.restrictTotalDegree_mono (σ : Type u_1) (R : Type u_2) [CommSemiring R] : Monotone (restrictTotalDegree σ R)

The polynomials of total degree at most m increase with m.

theorem MvPolynomial.monomial_mem_restrictTotalDegree {σ : Type u_1} {R : Type u_2} [CommSemiring R] {s : σ →₀ ℕ} {m : ℕ} (h : Finsupp.degree s ≤ m) (r : R) : (monomial s) r ∈ restrictTotalDegree σ R m

A monomial whose exponent has degree at most m has total degree at most m.

theorem MvPolynomial.restrictTotalDegree_eq_span (σ : Type u_1) (R : Type u_2) [CommSemiring R] (m : ℕ) : restrictTotalDegree σ R m = Submodule.span R ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' {s : σ →₀ ℕ | Finsupp.degree s ≤ m})

The polynomials of total degree at most m are spanned by the monomials of degree at most m.

theorem TauCeti.MvPolynomial.apply_mem_of_basis {σ : Type u_1} {κ : Type u_2} {R : Type u_3} {L : Type u_4} {M : Type u_5} [CommSemiring R] [AddCommMonoid L] [Module R L] [AddCommMonoid M] [Module R M] (b : Module.Basis κ R L) (Φ : L →ₗ[R] MvPolynomial σ R →ₗ[R] M) (N : Submodule R M) (d : ℕ) (h : ∀ (l : κ) (s : σ →₀ ℕ), Finsupp.degree s ≤ d → (Φ (b l)) ((MvPolynomial.monomial s) 1) ∈ N) (x : L) {p : MvPolynomial σ R} (hp : p ∈ MvPolynomial.restrictTotalDegree σ R d) : (Φ x) p ∈ N

A bilinear map out of a module and a polynomial algebra takes values in a submodule on polynomials of total degree at most d if it does so on basis vectors and monomials of degree at most d.