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.instCharP (σ : Type u) (R : Type v) [CommSemiring R] (p : ℕ) [CharP R p] : CharP (MvPolynomial σ R) p

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 ⋯ p = (MvPolynomial.map f) p

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 = Finsupp.supported R R s

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

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

Equations

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

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

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}

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 ∈ MvPolynomial.restrictTotalDegree σ R m ↔ p.totalDegree ≤ m

theorem MvPolynomial.mem_restrictDegree (σ : Type u) {R : Type v} [CommSemiring R] (p : MvPolynomial σ R) (n : ℕ) : p ∈ MvPolynomial.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 ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i p.degrees ≤ n

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

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

The monomials form a basis on MvPolynomial σ R.

Equations

• MvPolynomial.basisMonomials σ R = Finsupp.basisSingleOne

@[simp]

theorem MvPolynomial.coe_basisMonomials (σ : Type u) (R : Type v) [CommSemiring R] : ⇑(MvPolynomial.basisMonomials σ R) = fun (s : σ →₀ ℕ) => (MvPolynomial.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.

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

noncomputable def MvPolynomial.algebraMvPolynomial {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra (MvPolynomial σ R) (MvPolynomial σ S)

If S is an R-algebra, then MvPolynomial σ S is a MvPolynomial σ R algebra.

Warning: This produces a diamond for Algebra (MvPolynomial σ R) (MvPolynomial σ (MvPolynomial σ S)). That's why it is not a global instance.

Equations

• MvPolynomial.algebraMvPolynomial = (MvPolynomial.map (algebraMap R S)).toAlgebra

@[simp]

theorem MvPolynomial.algebraMap_def {R : Type u_1} {S : Type u_2} {σ : Type u_3} [CommSemiring R] [CommSemiring S] [Algebra R S] : algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S)

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

The monomials form a basis on R[X].

Equations

• Polynomial.basisMonomials R = { repr := (Polynomial.toFinsuppIsoAlg R).toLinearEquiv }

@[simp]

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