# 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

source
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)
source
instance MvPolynomial.instCharP (σ : Type u) (R : Type v) [CommSemiring R] (p : ℕ) [CharP R p] :
CharP (MvPolynomial σ R) p
source
instance MvPolynomial.instCharZero (σ : Type u) (R : Type v) [CommSemiring R] [CharZero R] :
CharZero (MvPolynomial σ R)
source
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 = (map f) p
source
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

Instances For

source
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 := Finsupp.supportedEquivFinsupp s }

Instances For

source
theorem MvPolynomial.restrictSupport_mono {σ : Type u} (R : Type v) [CommSemiring R] {s t : Set (σ →₀ ℕ)} (h : s ⊆ t) :
restrictSupport R s ≤ restrictSupport R t
source
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}

Instances For

source
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}

Instances For

source
theorem MvPolynomial.mem_restrictTotalDegree (σ : Type u) {R : Type v} [CommSemiring R] (m : ℕ) (p : MvPolynomial σ R) :
p ∈ restrictTotalDegree σ R m ↔ p.totalDegree ≤ m
source
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
source
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
source
theorem MvPolynomial.restrictTotalDegree_le_restrictDegree (σ : Type u) (R : Type v) [CommSemiring R] (m : ℕ) :
restrictTotalDegree σ R m ≤ restrictDegree σ R m
source
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 = Finsupp.basisSingleOne

Instances For

source
@[simp]
theorem MvPolynomial.coe_basisMonomials (σ : Type u) (R : Type v) [CommSemiring R] :
⇑(basisMonomials σ R) = fun (s : σ →₀ ℕ) => (monomial s) 1
source
instance MvPolynomial.instFree (σ : Type u) (R : Type v) [CommSemiring R] :
Module.Free R (MvPolynomial σ R)

The `R`-module `MvPolynomial σ R` is free.

source
theorem MvPolynomial.linearIndependent_X (σ : Type u) (R : Type v) [CommSemiring R] :
LinearIndependent R X
source
instance MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite (σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) :
Module.Finite R ↥(restrictDegree σ R N)
source
instance MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite (σ : Type u) (R : Type v) [CommSemiring R] [Finite σ] (N : ℕ) :
Module.Finite R ↥(restrictTotalDegree σ R N)