mathlib docs: ring_theory.polynomial.basic

source

@[instance]

def polynomial.char_p {R : Type u} [semiring R] (p : ℕ) [h : char_p R p] :

char_p (polynomial R) p

source

def polynomial.degree_le (R : Type u) [comm_ring R] (n : with_bot ℕ) :

submodule R (polynomial R)

The R-submodule of R[X] consisting of polynomials of degree ≤ n.

Equations

polynomial.degree_le R n = ⨅ (k : ℕ) (h : ↑k > n), (polynomial.lcoeff R k).ker

source

def polynomial.degree_lt (R : Type u) [comm_ring R] (n : ℕ) :

submodule R (polynomial R)

The R-submodule of R[X] consisting of polynomials of degree < n.

Equations

polynomial.degree_lt R n = ⨅ (k : ℕ) (h : k ≥ n), (polynomial.lcoeff R k).ker

source

theorem polynomial.mem_degree_le {R : Type u} [comm_ring R] {n : with_bot ℕ} {f : polynomial R} :

f ∈ polynomial.degree_le R n ↔ f.degree ≤ n

source

theorem polynomial.degree_le_mono {R : Type u} [comm_ring R] {m n : with_bot ℕ} (H : m ≤ n) :

polynomial.degree_le R m ≤ polynomial.degree_le R n

source

theorem polynomial.degree_le_eq_span_X_pow {R : Type u} [comm_ring R] {n : ℕ} :

polynomial.degree_le R ↑n = submodule.span R ↑(finset.image (λ (n : ℕ), polynomial.X ^ n) (finset.range (n + 1)))

source

theorem polynomial.mem_degree_lt {R : Type u} [comm_ring R] {n : ℕ} {f : polynomial R} :

f ∈ polynomial.degree_lt R n ↔ f.degree < ↑n

source

theorem polynomial.degree_lt_mono {R : Type u} [comm_ring R] {m n : ℕ} (H : m ≤ n) :

polynomial.degree_lt R m ≤ polynomial.degree_lt R n

source

theorem polynomial.degree_lt_eq_span_X_pow {R : Type u} [comm_ring R] {n : ℕ} :

polynomial.degree_lt R n = submodule.span R ↑(finset.image (λ (n : ℕ), polynomial.X ^ n) (finset.range n))

source

def polynomial.restriction {R : Type u} [comm_ring R] (p : polynomial R) :

polynomial ↥(ring.closure ↑(finsupp.frange p))

Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.

Equations

p.restriction = {support := p.support, to_fun := λ (i : ℕ), ⟨p.to_fun i, _⟩, mem_support_to_fun := _}

source

@[simp]

theorem polynomial.coeff_restriction {R : Type u} [comm_ring R] {p : polynomial R} {n : ℕ} :

↑(p.restriction.coeff n) = p.coeff n

source

@[simp]

theorem polynomial.coeff_restriction' {R : Type u} [comm_ring R] {p : polynomial R} {n : ℕ} :

(p.restriction.coeff n).val = p.coeff n

source

@[simp]

theorem polynomial.map_restriction {R : Type u} [comm_ring R] (p : polynomial R) :

polynomial.map (algebra_map ↥(ring.closure ↑(finsupp.frange p)) R) p.restriction = p

source

@[simp]

theorem polynomial.degree_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

p.restriction.degree = p.degree

source

@[simp]

theorem polynomial.nat_degree_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

p.restriction.nat_degree = p.nat_degree

source

@[simp]

theorem polynomial.monic_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

p.restriction.monic ↔ p.monic

source

@[simp]

theorem polynomial.restriction_zero {R : Type u} [comm_ring R] :

0.restriction = 0

source

@[simp]

theorem polynomial.restriction_one {R : Type u} [comm_ring R] :

1.restriction = 1

source

theorem polynomial.eval₂_restriction {R : Type u} [comm_ring R] {S : Type v} [ring S] {f : R →+* S} {x : S} {p : polynomial R} :

polynomial.eval₂ f x p = polynomial.eval₂ (f.comp (is_subring.subtype (ring.closure ↑(finsupp.frange p)))) x p.restriction

source

def polynomial.to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) :

polynomial ↥T

Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in `T.

Equations

p.to_subring T hp = {support := p.support, to_fun := λ (i : ℕ), ⟨p.to_fun i, _⟩, mem_support_to_fun := _}

source

@[simp]

theorem polynomial.coeff_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) {n : ℕ} :

↑((p.to_subring T hp).coeff n) = p.coeff n

source

@[simp]

theorem polynomial.coeff_to_subring' {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) {n : ℕ} :

((p.to_subring T hp).coeff n).val = p.coeff n

source

@[simp]

theorem polynomial.degree_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) :

(p.to_subring T hp).degree = p.degree

source

@[simp]

theorem polynomial.nat_degree_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) :

(p.to_subring T hp).nat_degree = p.nat_degree

source

@[simp]

theorem polynomial.monic_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) :

(p.to_subring T hp).monic ↔ p.monic

source

@[simp]

theorem polynomial.to_subring_zero {R : Type u} [comm_ring R] (T : set R) [is_subring T] :

0.to_subring T _ = 0

source

@[simp]

theorem polynomial.to_subring_one {R : Type u} [comm_ring R] (T : set R) [is_subring T] :

1.to_subring T _ = 1

source

@[simp]

theorem polynomial.map_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : ↑(finsupp.frange p) ⊆ T) :

polynomial.map (is_subring.subtype T) (p.to_subring T hp) = p

source

def polynomial.of_subring {R : Type u} [comm_ring R] (T : set R) [is_subring T] (p : polynomial ↥T) :

polynomial R

Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefificents are in the ambient ring.

Equations

polynomial.of_subring T p = {support := p.support, to_fun := subtype.val ∘ p.to_fun, mem_support_to_fun := _}

source

@[simp]

theorem polynomial.frange_of_subring {R : Type u} [comm_ring R] (T : set R) [is_subring T] {p : polynomial ↥T} :

↑(finsupp.frange (polynomial.of_subring T p)) ⊆ T

source

theorem ideal.mem_map_C_iff {R : Type u} [comm_ring R] {I : ideal R} {f : polynomial R} :

f ∈ ideal.map polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

The push-forward of an ideal I of R to polynomial R via inclusion is exactly the set of polynomials whose coefficients are in I

source

theorem ideal.quotient_map_C_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (a : R) (H : a ∈ I) :

⇑((ideal.quotient.mk (ideal.map polynomial.C I)).comp polynomial.C) a = 0

source

theorem ideal.eval₂_C_mk_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (f : polynomial R) (H : f ∈ ideal.map polynomial.C I) :

⇑(polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) f = 0

source

def ideal.polynomial_quotient_equiv_quotient_polynomial {R : Type u} [comm_ring R] {I : ideal R} :

polynomial I.quotient ≃+* (ideal.map polynomial.C I).quotient

If I is an ideal of R, then the ring polynomials over the quotient ring I.quotient is isomorphic to the quotient of polynomial R by the ideal map C I, where map C I contains exactly the polynomials whose coefficients all lie in I

Equations

source

def ideal.of_polynomial {R : Type u} [comm_ring R] (I : ideal (polynomial R)) :

submodule R (polynomial R)

Transport an ideal of R[X] to an R-submodule of R[X].

Equations

I.of_polynomial = {carrier := I.carrier, zero_mem' := _, add_mem' := _, smul_mem' := _}

source

theorem ideal.mem_of_polynomial {R : Type u} [comm_ring R] {I : ideal (polynomial R)} (x : polynomial R) :

x ∈ I.of_polynomial ↔ x ∈ I

source

def ideal.degree_le {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : with_bot ℕ) :

submodule R (polynomial R)

Given an ideal I of R[X], make the R-submodule of I consisting of polynomials of degree ≤ n.

Equations

I.degree_le n = polynomial.degree_le R n ⊓ I.of_polynomial

source

def ideal.leading_coeff_nth {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : ℕ) :

ideal R

Given an ideal I of R[X], make the ideal in R of leading coefficients of polynomials in I with degree ≤ n.

Equations

I.leading_coeff_nth n = submodule.map (polynomial.lcoeff R n) (I.degree_le ↑n)

source

theorem ideal.mem_leading_coeff_nth {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : ℕ) (x : R) :

x ∈ I.leading_coeff_nth n ↔ ∃ (p : polynomial R) (H : p ∈ I), p.degree ≤ ↑n ∧ p.leading_coeff = x

source

theorem ideal.mem_leading_coeff_nth_zero {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (x : R) :

x ∈ I.leading_coeff_nth 0 ↔ ⇑polynomial.C x ∈ I

source

theorem ideal.leading_coeff_nth_mono {R : Type u} [comm_ring R] (I : ideal (polynomial R)) {m n : ℕ} (H : m ≤ n) :

I.leading_coeff_nth m ≤ I.leading_coeff_nth n

source

def ideal.leading_coeff {R : Type u} [comm_ring R] (I : ideal (polynomial R)) :

ideal R

Given an ideal I in R[X], make the ideal in R of the leading coefficients in I.

Equations

I.leading_coeff = ⨆ (n : ℕ), I.leading_coeff_nth n

source

theorem ideal.mem_leading_coeff {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (x : R) :

x ∈ I.leading_coeff ↔ ∃ (p : polynomial R) (H : p ∈ I), p.leading_coeff = x

source

theorem ideal.is_fg_degree_le {R : Type u} [comm_ring R] (I : ideal (polynomial R)) [is_noetherian_ring R] (n : ℕ) :

(I.degree_le ↑n).fg

source

@[instance]

theorem polynomial.is_noetherian_ring {R : Type u} [comm_ring R] [is_noetherian_ring R] :

is_noetherian_ring (polynomial R)

Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring.

source

theorem polynomial.exists_irreducible_of_degree_pos {R : Type u} [integral_domain R] [is_noetherian_ring R] {f : polynomial R} (hf : 0 < f.degree) :

∃ (g : polynomial R), irreducible g ∧ g ∣ f

source

theorem polynomial.exists_irreducible_of_nat_degree_pos {R : Type u} [integral_domain R] [is_noetherian_ring R] {f : polynomial R} (hf : 0 < f.nat_degree) :

∃ (g : polynomial R), irreducible g ∧ g ∣ f

source

theorem polynomial.exists_irreducible_of_nat_degree_ne_zero {R : Type u} [integral_domain R] [is_noetherian_ring R] {f : polynomial R} (hf : f.nat_degree ≠ 0) :

∃ (g : polynomial R), irreducible g ∧ g ∣ f

source

theorem polynomial.linear_independent_powers_iff_eval₂ {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) (v : M) :

linear_independent R (λ (n : ℕ), ⇑(f ^ n) v) ↔ ∀ (p : polynomial R), ⇑(⇑(polynomial.aeval f) p) v = 0 → p = 0

source

theorem polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :

disjoint (⇑(polynomial.aeval f) p).ker (⇑(polynomial.aeval f) q).ker

source

theorem polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :

(⇑(polynomial.aeval f) p).range ⊔ (⇑(polynomial.aeval f) q).range = ⊤

source

theorem polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : M →ₗ[R] M} {p q : polynomial R} :

(⇑(polynomial.aeval f) p).ker ⊔ (⇑(polynomial.aeval f) q).ker ≤ (⇑(polynomial.aeval f) (p * q)).ker

source

theorem polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :

(⇑(polynomial.aeval f) p).ker ⊔ (⇑(polynomial.aeval f) q).ker = (⇑(polynomial.aeval f) (p * q)).ker

source

theorem mv_polynomial.is_noetherian_ring_fin_0 {R : Type u} [comm_ring R] [is_noetherian_ring R] :

is_noetherian_ring (mv_polynomial (fin 0) R)

source

theorem mv_polynomial.is_noetherian_ring_fin {R : Type u} [comm_ring R] [is_noetherian_ring R] {n : ℕ} :

is_noetherian_ring (mv_polynomial (fin n) R)

source

@[instance]

def mv_polynomial.is_noetherian_ring {R : Type u} {σ : Type v} [comm_ring R] [fintype σ] [is_noetherian_ring R] :

is_noetherian_ring (mv_polynomial σ R)

The multivariate polynomial ring in finitely many variables over a noetherian ring is itself a noetherian ring.

source

theorem mv_polynomial.is_integral_domain_fin_zero (R : Type u) [comm_ring R] (hR : is_integral_domain R) :

is_integral_domain (mv_polynomial (fin 0) R)

source

theorem mv_polynomial.is_integral_domain_fin (R : Type u) [comm_ring R] (hR : is_integral_domain R) (n : ℕ) :

is_integral_domain (mv_polynomial (fin n) R)

Auxilliary lemma: Multivariate polynomials over an integral domain with variables indexed by fin n form an integral domain. This fact is proven inductively, and then used to prove the general case without any finiteness hypotheses. See mv_polynomial.integral_domain for the general case.

source

theorem mv_polynomial.is_integral_domain_fintype (R : Type u) (σ : Type v) [comm_ring R] [fintype σ] (hR : is_integral_domain R) :

is_integral_domain (mv_polynomial σ R)

source

def mv_polynomial.integral_domain_fintype (R : Type u) (σ : Type v) [integral_domain R] [fintype σ] :

integral_domain (mv_polynomial σ R)

Auxilliary definition: Multivariate polynomials in finitely many variables over an integral domain form an integral domain. This fact is proven by transport of structure from the mv_polynomial.integral_domain_fin, and then used to prove the general case without finiteness hypotheses. See mv_polynomial.integral_domain for the general case.

Equations

mv_polynomial.integral_domain_fintype R σ = is_integral_domain.to_integral_domain (mv_polynomial σ R) _

source

theorem mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u} [integral_domain R] {σ : Type v} (p q : mv_polynomial σ R) (h : p * q = 0) :

p = 0 ∨ q = 0

source

@[instance]

def mv_polynomial.integral_domain {R : Type u} {σ : Type v} [integral_domain R] :

integral_domain (mv_polynomial σ R)

The multivariate polynomial ring over an integral domain is an integral domain.

Equations

mv_polynomial.integral_domain = {add := comm_ring.add mv_polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero mv_polynomial.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg mv_polynomial.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul mv_polynomial.comm_ring, mul_assoc := _, one := comm_ring.one mv_polynomial.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}