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 ringR
of total degree at mostm
.restrictDegree σ R m
: the subspace of multivariate polynomials indexed byσ
over the commutative ringR
such that the degree in each individual variable is at mostm
.
Main statements #
- The multivariate polynomial ring over a commutative semiring of characteristic
p
has characteristicp
, and similarly forCharZero
. 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} σ]
:
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)
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)
:
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
def
MvPolynomial.basisRestrictSupport
{σ : Type u}
(R : Type v)
[CommSemiring R]
(s : Set (σ →₀ ℕ))
:
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
theorem
MvPolynomial.restrictSupport_mono
{σ : Type u}
(R : Type v)
[CommSemiring R]
{s t : Set (σ →₀ ℕ)}
(h : s ⊆ 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
Instances For
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
theorem
MvPolynomial.mem_restrictTotalDegree
(σ : Type u)
{R : Type v}
[CommSemiring R]
(m : ℕ)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.mem_restrictDegree
(σ : Type u)
{R : Type v}
[CommSemiring R]
(p : MvPolynomial σ R)
(n : ℕ)
:
theorem
MvPolynomial.mem_restrictDegree_iff_sup
(σ : Type u)
{R : Type v}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
(n : ℕ)
:
theorem
MvPolynomial.restrictTotalDegree_le_restrictDegree
(σ : Type u)
(R : Type v)
[CommSemiring 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
Instances For
@[simp]
instance
MvPolynomial.instFree
(σ : Type u)
(R : Type v)
[CommSemiring R]
:
Module.Free R (MvPolynomial σ R)
The R
-module MvPolynomial σ R
is free.
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)