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.instCharPMvPolynomialToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringCommSemiring
(σ : Type u)
(R : Type v)
[CommSemiring R]
(p : ℕ)
[CharP R p]
:
CharP (MvPolynomial σ R) p
instance
MvPolynomial.instCharZeroMvPolynomialToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringCommSemiring
(σ : 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)
:
Finsupp.mapRange ↑f (_ : ↑f 0 = 0) p = ↑(MvPolynomial.map f) p
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
.
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
.
Instances For
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 : σ →₀ ℕ), 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
def
MvPolynomial.basisMonomials
(σ : Type u)
(R : Type v)
[CommSemiring R]
:
Basis (σ →₀ ℕ) R (MvPolynomial σ R)
The monomials form a basis on MvPolynomial σ R
.
Instances For
@[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
The monomials form a basis on R[X]
.
Instances For
@[simp]
theorem
Polynomial.coe_basisMonomials
(R : Type v)
[CommSemiring R]
:
↑(Polynomial.basisMonomials R) = fun s => ↑(Polynomial.monomial s) 1