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

Equations

• (_ : CharP (MvPolynomial σ R) p) = (_ : CharP (MvPolynomial σ R) p)

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

Equations

• (_ : CharZero (MvPolynomial σ 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.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 : σ →₀ ℕ | (Finsupp.sum n 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 ↔ 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 ∈ 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

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

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

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

Equations

• (_ : Module.Finite R ↥(MvPolynomial.restrictDegree σ R N)) = (_ : Module.Finite R ↥(MvPolynomial.restrictDegree σ R N))

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

Equations

• (_ : Module.Finite R ↥(MvPolynomial.restrictTotalDegree σ R N)) = (_ : Module.Finite R ↥(MvPolynomial.restrictTotalDegree σ R N))

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 := AlgEquiv.toLinearEquiv (Polynomial.toFinsuppIsoAlg R) }

@[simp]

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