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.instSmall {σ : Type u_1} {R : Type u_2} [CommSemiring R] [Small.{u, u_2} R] [Small.{u, u_1} σ] : Small.{u, max u_2 u_1} (MvPolynomial σ R)

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

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

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

theorem MvPolynomial.map_eq_map (σ : Type u) {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) (f : R →+* S) : AddMonoidAlgebra.map (↑f) p = (map f) p

@[deprecated MvPolynomial.map_eq_map (since := "2026-06-18")]

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) : AddMonoidAlgebra.map (↑f) p = (map f) p

Alias of MvPolynomial.map_eq_map.

noncomputable def MvPolynomial.restrictSupport {σ : Type u} (R : Type v) [CommSemiring R] (s : Set (σ →₀ ℕ)) : Submodule R (MvPolynomial σ R)

The submodule of polynomials that are sum of monomials in the set s.

Equations

• MvPolynomial.restrictSupport R s = AddMonoidAlgebra.supported R R s

noncomputable def MvPolynomial.basisRestrictSupport {σ : Type u} (R : Type v) [CommSemiring R] (s : Set (σ →₀ ℕ)) : Module.Basis (↑s) R ↥(restrictSupport R s)

restrictSupport R s has a canonical R-basis indexed by s.

Equations

• MvPolynomial.basisRestrictSupport R s = { repr := AddMonoidAlgebra.supportedEquivFinsupp s }

theorem MvPolynomial.restrictSupport_mono {σ : Type u} (R : Type v) [CommSemiring R] {s t : Set (σ →₀ ℕ)} (h : s ⊆ t) : restrictSupport R s ≤ restrictSupport R t

theorem MvPolynomial.restrictSupport_eq_span {σ : Type u} (R : Type v) [CommSemiring R] (s : Set (σ →₀ ℕ)) : restrictSupport R s = Submodule.span R ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s)

theorem MvPolynomial.mem_restrictSupport_iff {σ : Type u} (R : Type v) [CommSemiring R] {s : Set (σ →₀ ℕ)} {r : MvPolynomial σ R} : r ∈ restrictSupport R s ↔ ↑r.support ⊆ s

@[simp]

theorem MvPolynomial.monomial_mem_restrictSupport {σ : Type u} (R : Type v) [CommSemiring R] {s : Set (σ →₀ ℕ)} {m : σ →₀ ℕ} {r : R} : (monomial m) r ∈ restrictSupport R s ↔ m ∈ s ∨ r = 0

theorem MvPolynomial.restrictSupport_add {σ : Type u} (R : Type v) [CommSemiring R] (s t : Set (σ →₀ ℕ)) : restrictSupport R (s + t) = restrictSupport R s * restrictSupport R t

@[simp]

theorem MvPolynomial.restrictSupport_zero {σ : Type u} (R : Type v) [CommSemiring R] : restrictSupport R 0 = 1

@[simp]

theorem MvPolynomial.restrictSupport_univ {σ : Type u} (R : Type v) [CommSemiring R] : restrictSupport R Set.univ = ⊤

theorem MvPolynomial.restrictSupport_nsmul {σ : Type u} (R : Type v) [CommSemiring R] (n : ℕ) (s : Set (σ →₀ ℕ)) : restrictSupport R (n • s) = restrictSupport R s ^ n

noncomputable def MvPolynomial.restrictSupportIdeal {σ : Type u} (R : Type v) [CommSemiring R] (s : Set (σ →₀ ℕ)) (hs : IsUpperSet s) : Ideal (MvPolynomial σ R)

The ideal defined by restrictSupport R s when s is an upper set.

Equations

• MvPolynomial.restrictSupportIdeal R s hs = { toAddSubmonoid := (MvPolynomial.restrictSupport R s).toAddSubmonoid, smul_mem' := ⋯ }

@[simp]

theorem MvPolynomial.restrictScalars_restrictSupportIdeal {σ : Type u} (R : Type v) [CommSemiring R] (s : Set (σ →₀ ℕ)) (hs : IsUpperSet s) : Submodule.restrictScalars R (restrictSupportIdeal R s hs) = restrictSupport R s

noncomputable 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.

Equations

• MvPolynomial.restrictTotalDegree σ R m = MvPolynomial.restrictSupport R {n : σ →₀ ℕ | (n.sum fun (x : σ) (e : ℕ) => e) ≤ m}

noncomputable 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.

Equations

• MvPolynomial.restrictDegree σ R m = MvPolynomial.restrictSupport R {n : σ →₀ ℕ | ∀ (i : σ), n i ≤ m}

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

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

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

theorem MvPolynomial.restrictTotalDegree_le_restrictDegree (σ : Type u) (R : Type v) [CommSemiring R] (m : ℕ) : restrictTotalDegree σ R m ≤ restrictDegree σ R m

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

The monomials form a basis on MvPolynomial σ R.

Equations

• MvPolynomial.basisMonomials σ R = { repr := AddMonoidAlgebra.coeffLinearEquiv R }

@[simp]

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

instance MvPolynomial.instFree (σ : Type u) (R : Type v) [CommSemiring R] : Module.Free R (MvPolynomial σ R)

The R-module MvPolynomial σ R is free.

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

instance MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite (σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) : Module.Finite R ↥(restrictDegree σ R N)

instance MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite (σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) : Module.Finite R ↥(restrictTotalDegree σ R N)