Multivariate polynomials over commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ring R of total degree at most m.
restrict_degree σ 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 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

source

@[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

source

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

source

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}

source

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}

source

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

source

theorem mv_polynomial.mem_restrict_degree (σ : Type u) {R : Type v} [comm_ring R] (p : mv_polynomial σ R) (n : ℕ) :

p ∈ mv_polynomial.restrict_degree σ R n ↔ ∀ (s : σ →₀ ℕ), s ∈ p.support → ∀ (i : σ), ⇑s i ≤ n

source

theorem mv_polynomial.mem_restrict_degree_iff_sup (σ : Type u) {R : Type v} [comm_ring R] [decidable_eq σ] (p : mv_polynomial σ R) (n : ℕ) :

p ∈ mv_polynomial.restrict_degree σ R n ↔ ∀ (i : σ), multiset.count i p.degrees ≤ n

source

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

mv_polynomial.basis_monomials σ R = finsupp.basis_single_one

source

@[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

source

theorem mv_polynomial.linear_independent_X (σ : Type u) (R : Type v) [comm_ring R] :

linear_independent R mv_polynomial.X

source

noncomputable def polynomial.basis_monomials (R : Type v) [comm_ring R] :

basis ℕ R (polynomial R)

The monomials form a basis on R[X].

Equations

polynomial.basis_monomials R = {repr := (polynomial.to_finsupp_iso_alg R).to_linear_equiv}

source

@[simp]

theorem polynomial.coe_basis_monomials (R : Type v) [comm_ring R] :

⇑(polynomial.basis_monomials R) = λ (s : ℕ), ⇑(polynomial.monomial s) 1