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 #
restrict_total_degree σ R m
: the subspace of multivariate polynomials indexed byσ
over the commutative ringR
of total degree at mostm
.restrict_degree σ 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 ring of positive characteristic has positive characteristic.
basis_monomials
: shows that the monomials form a basis of the vector space of multivariate polynomials.
TODO #
Generalise to noncommutative (semi)rings
@[protected, instance]
def
mv_polynomial.char_p
(σ : Type u)
(R : Type v)
[comm_ring R]
(p : ℕ)
[char_p R p] :
char_p (mv_polynomial σ R) p
theorem
mv_polynomial.map_range_eq_map
(σ : Type u)
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
(p : mv_polynomial σ R)
(f : R →+* S) :
finsupp.map_range ⇑f _ p = ⇑(mv_polynomial.map f) p
def
mv_polynomial.restrict_total_degree
(σ : Type u)
(R : Type v)
[comm_ring R]
(m : ℕ) :
submodule R (mv_polynomial σ R)
The submodule of polynomials of total degree less than or equal to m
.
Equations
- mv_polynomial.restrict_total_degree σ R m = finsupp.supported R R {n : σ →₀ ℕ | n.sum (λ (n : σ) (e : ℕ), e) ≤ m}
def
mv_polynomial.restrict_degree
(σ : Type u)
(R : Type v)
[comm_ring R]
(m : ℕ) :
submodule R (mv_polynomial σ R)
The submodule of polynomials such that the degree with respect to each individual variable is
less than or equal to m
.
Equations
- mv_polynomial.restrict_degree σ R m = finsupp.supported R R {n : σ →₀ ℕ | ∀ (i : σ), ⇑n i ≤ m}
theorem
mv_polynomial.mem_restrict_total_degree
(σ : Type u)
{R : Type v}
[comm_ring R]
(m : ℕ)
(p : mv_polynomial σ R) :
p ∈ mv_polynomial.restrict_total_degree σ R m ↔ p.total_degree ≤ m
theorem
mv_polynomial.mem_restrict_degree
(σ : Type u)
{R : Type v}
[comm_ring R]
(p : mv_polynomial σ R)
(n : ℕ) :
theorem
mv_polynomial.mem_restrict_degree_iff_sup
(σ : Type u)
{R : Type v}
[comm_ring R]
(p : mv_polynomial σ R)
(n : ℕ) :
p ∈ mv_polynomial.restrict_degree σ R n ↔ ∀ (i : σ), multiset.count i p.degrees ≤ n
noncomputable
def
mv_polynomial.basis_monomials
(σ : Type u)
(R : Type v)
[comm_ring R] :
basis (σ →₀ ℕ) R (mv_polynomial σ R)
The monomials form a basis on mv_polynomial σ R
.
Equations
@[simp]
theorem
mv_polynomial.coe_basis_monomials
(σ : Type u)
(R : Type v)
[comm_ring R] :
⇑(mv_polynomial.basis_monomials σ R) = λ (s : σ →₀ ℕ), ⇑(mv_polynomial.monomial s) 1
The monomials form a basis on polynomial R
.
Equations
@[simp]
theorem
polynomial.coe_basis_monomials
(R : Type v)
[comm_ring R] :
⇑(polynomial.basis_monomials R) = λ (s : ℕ), ⇑(polynomial.monomial s) 1