Multivariate polynomials over commutative rings

This file contains basic facts about multivariate polynomials over commutative rings, for example that the monomials form a basis.

Main definitions

• restrictTotalDegree σ R m: the subspace of multivariate polynomials indexed by σ over the commutative ring R of total degree at most m.
• restrictDegree σ R m: the subspace of multivariate polynomials indexed by σ over the commutative ring R such that the degree in each individual variable is at most m.

Main statements

• The multivariate polynomial ring over a commutative semiring of characteristic p has characteristic p, and similarly for CharZero.
• basisMonomials: shows that the monomials form a basis of the vector space of multivariate polynomials.

TODO

Generalise to noncommutative (semi)rings

instance MvPolynomial.instCharPMvPolynomialToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringCommSemiring (σ : Type u) (R : Type v) [CommSemiring R] (p : ℕ) [CharP R p] : CharP (MvPolynomial σ R) p

instance MvPolynomial.instCharZeroMvPolynomialToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringCommSemiring (σ : Type u) (R : Type v) [CommSemiring R] [CharZero R] : CharZero (MvPolynomial σ R)

theorem MvPolynomial.mapRange_eq_map (σ : Type u) {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) : Finsupp.mapRange ↑f (_ : ↑f 0 = 0) p = ↑(MvPolynomial.map f) p

def MvPolynomial.restrictTotalDegree (σ : Type u) (R : Type v) [CommSemiring R] (m : ℕ) : Submodule R (MvPolynomial σ R)

The submodule of polynomials of total degree less than or equal to m.

def MvPolynomial.restrictDegree (σ : Type u) (R : Type v) [CommSemiring R] (m : ℕ) : Submodule R (MvPolynomial σ R)

The submodule of polynomials such that the degree with respect to each individual variable is less than or equal to m.

theorem MvPolynomial.mem_restrictTotalDegree (σ : Type u) {R : Type v} [CommSemiring R] (m : ℕ) (p : MvPolynomial σ R) : p ∈ MvPolynomial.restrictTotalDegree σ R m ↔ MvPolynomial.totalDegree p ≤ m

theorem MvPolynomial.mem_restrictDegree (σ : Type u) {R : Type v} [CommSemiring R] (p : MvPolynomial σ R) (n : ℕ) : p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ (s : σ →₀ ℕ), s ∈ MvPolynomial.support p → ∀ (i : σ), ↑s i ≤ n

theorem MvPolynomial.mem_restrictDegree_iff_sup (σ : Type u) {R : Type v} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (n : ℕ) : p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i (MvPolynomial.degrees p) ≤ n

def MvPolynomial.basisMonomials (σ : Type u) (R : Type v) [CommSemiring R] : Basis (σ →₀ ℕ) R (MvPolynomial σ R)

The monomials form a basis on MvPolynomial σ R.

@[simp]

theorem MvPolynomial.coe_basisMonomials (σ : Type u) (R : Type v) [CommSemiring R] : ↑(MvPolynomial.basisMonomials σ R) = fun s => ↑(MvPolynomial.monomial s) 1

theorem MvPolynomial.linearIndependent_X (σ : Type u) (R : Type v) [CommSemiring R] : LinearIndependent R MvPolynomial.X

noncomputable def Polynomial.basisMonomials (R : Type v) [CommSemiring R] : Basis ℕ R (Polynomial R)

The monomials form a basis on R[X].

@[simp]

theorem Polynomial.coe_basisMonomials (R : Type v) [CommSemiring R] : ↑(Polynomial.basisMonomials R) = fun s => ↑(Polynomial.monomial s) 1