Mathlib.RingTheory.Polynomial.Basic

Polynomial.instCharP instance

(p : ℕ) [h : CharP R p] : CharP R[X] p

Full source

instance instCharP (p : ℕ) [h : CharP R p] : CharP R[X] p :=
  let ⟨h⟩ := h
  ⟨fun n => by rw [← map_natCast C, ← C_0, C_inj, h]⟩

Polynomial Ring Preserves Characteristic

Informal description

For any natural number $p$ and any ring $R$ of characteristic $p$, the polynomial ring $R[X]$ also has characteristic $p$.

Polynomial.instExpChar instance

(p : ℕ) [h : ExpChar R p] : ExpChar R[X] p

Full source

instance instExpChar (p : ℕ) [h : ExpChar R p] : ExpChar R[X] p := by
  cases h; exacts [ExpChar.zero, ExpChar.prime ‹_›]

Polynomial Ring Preserves Exponential Characteristic

Informal description

For any natural number $p$ and any ring $R$ of exponential characteristic $p$, the polynomial ring $R[X]$ also has exponential characteristic $p$.

Polynomial.degreeLE definition

(n : WithBot ℕ) : Submodule R R[X]

Full source

/-- The `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n`. -/
def degreeLE (n : WithBot ℕ) : Submodule R R[X] :=
  ⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff R k)

Submodule of polynomials with degree at most $n$

Informal description

For a commutative ring $R$ and an extended natural number $n \in \mathbb{N} \cup \{\bot\}$, the $R$-submodule $\text{degreeLE}(R, n)$ consists of all polynomials $f \in R[X]$ with degree at most $n$. This is defined as the intersection of the kernels of the leading coefficient functions $\text{lcoeff}(R, k)$ for all natural numbers $k > n$.

Polynomial.degreeLT definition

(n : ℕ) : Submodule R R[X]

Full source

/-- The `R`-submodule of `R[X]` consisting of polynomials of degree < `n`. -/
def degreeLT (n : ℕ) : Submodule R R[X] :=
  ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff R k)

Submodule of polynomials with degree less than n

Informal description

For a commutative ring $R$ and natural number $n$, the $R$-submodule $\text{degreeLT}(R, n)$ consists of all polynomials $f \in R[X]$ with degree strictly less than $n$. This is equivalently defined as the intersection of the kernels of the leading coefficient functions $\text{lcoeff}(R, k)$ for all $k \geq n$.

Polynomial.mem_degreeLE theorem

{n : WithBot ℕ} {f : R[X]} : f ∈ degreeLE R n ↔ degree f ≤ n

Full source

theorem mem_degreeLE {n : WithBot ℕ} {f : R[X]} : f ∈ degreeLE R nf ∈ degreeLE R n ↔ degree f ≤ n := by
  simp only [degreeLE, Submodule.mem_iInf, degree_le_iff_coeff_zero, LinearMap.mem_ker]; rfl

Membership Criterion for Polynomials of Bounded Degree: $f \in \text{degreeLE}(R, n) \leftrightarrow \deg(f) \leq n$

Informal description

For any polynomial $f \in R[X]$ and extended natural number $n \in \mathbb{N} \cup \{\bot\}$, the polynomial $f$ belongs to the submodule of polynomials with degree at most $n$ if and only if the degree of $f$ is less than or equal to $n$, i.e., $f \in \text{degreeLE}(R, n) \leftrightarrow \deg(f) \leq n$.

Polynomial.degreeLE_mono theorem

{m n : WithBot ℕ} (H : m ≤ n) : degreeLE R m ≤ degreeLE R n

Full source

@[mono]
theorem degreeLE_mono {m n : WithBot ℕ} (H : m ≤ n) : degreeLE R m ≤ degreeLE R n := fun _ hf =>
  mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) H)

Monotonicity of Polynomial Degree Submodules: $\text{degreeLE}(R, m) \subseteq \text{degreeLE}(R, n)$ for $m \leq n$

Informal description

For any extended natural numbers $m, n \in \mathbb{N} \cup \{\bot\}$ such that $m \leq n$, the submodule of polynomials with degree at most $m$ is contained in the submodule of polynomials with degree at most $n$.

Polynomial.degreeLE_eq_span_X_pow theorem

[DecidableEq R] {n : ℕ} : degreeLE R n = Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : R[X]) ^ n)

Full source

theorem degreeLE_eq_span_X_pow [DecidableEq R] {n : ℕ} :
    degreeLE R n = Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : R[X]) ^ n) := by
  apply le_antisymm
  · intro p hp
    replace hp := mem_degreeLE.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_le_coe.1 (Finset.sup_le_iff.1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <|
            Finset.mem_image.2 ⟨_, Finset.mem_range.2 (Nat.lt_succ_of_le this), rfl⟩)
  rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
  intro k hk
  apply mem_degreeLE.2
  exact
    (degree_X_pow_le _).trans (WithBot.coe_le_coe.2 <| Nat.le_of_lt_succ <| Finset.mem_range.1 hk)

Polynomials of Bounded Degree as Span of Monomials: $\text{degreeLE}(R, n) = \operatorname{span}_R \{X^k \mid 0 \leq k \leq n\}$

Informal description

For any commutative ring $R$ with decidable equality and any natural number $n$, the submodule of polynomials with degree at most $n$ is equal to the $R$-linear span of the set $\{X^k \mid 0 \leq k \leq n\}$, where $X$ is the polynomial variable.

Polynomial.mem_degreeLT theorem

{n : ℕ} {f : R[X]} : f ∈ degreeLT R n ↔ degree f < n

Full source

theorem mem_degreeLT {n : ℕ} {f : R[X]} : f ∈ degreeLT R nf ∈ degreeLT R n ↔ degree f < n := by
  rw [degreeLT, Submodule.mem_iInf]
  conv_lhs => intro i; rw [Submodule.mem_iInf]
  rw [degree, Finset.max_eq_sup_coe]
  rw [Finset.sup_lt_iff ?_]
  rotate_left
  · apply WithBot.bot_lt_coe
  conv_rhs =>
    simp only [mem_support_iff]
    intro b
    rw [Nat.cast_withBot, WithBot.coe_lt_coe, lt_iff_not_le, Ne, not_imp_not]
  rfl

Characterization of Polynomials in $\text{degreeLT}(R, n)$: $f \in \text{degreeLT}(R, n) \leftrightarrow \deg(f) < n$

Informal description

For any polynomial $f$ over a commutative ring $R$ and any natural number $n$, the polynomial $f$ belongs to the submodule of polynomials with degree strictly less than $n$ if and only if the degree of $f$ is strictly less than $n$. In other words, \[ f \in \text{degreeLT}(R, n) \leftrightarrow \deg(f) < n. \]

Polynomial.degreeLT_mono theorem

{m n : ℕ} (H : m ≤ n) : degreeLT R m ≤ degreeLT R n

Full source

@[mono]
theorem degreeLT_mono {m n : ℕ} (H : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
  mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 H)

Monotonicity of Degree-Bounded Polynomial Submodules: $\text{degreeLT}(R, m) \subseteq \text{degreeLT}(R, n)$ for $m \leq n$

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the submodule of polynomials with degree less than $m$ is contained in the submodule of polynomials with degree less than $n$. In other words, if $m \leq n$, then $\text{degreeLT}(R, m) \subseteq \text{degreeLT}(R, n)$.

Polynomial.degreeLT_eq_span_X_pow theorem

[DecidableEq R] {n : ℕ} : degreeLT R n = Submodule.span R ↑((Finset.range n).image fun n => X ^ n : Finset R[X])

Full source

theorem degreeLT_eq_span_X_pow [DecidableEq R] {n : ℕ} :
    degreeLT R n = Submodule.span R ↑((Finset.range n).image fun n => X ^ n : Finset R[X]) := by
  apply le_antisymm
  · intro p hp
    replace hp := mem_degreeLT.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine
      Submodule.smul_mem _ _
        (Submodule.subset_span <|
          Finset.mem_coe.2 <| Finset.mem_image.2 ⟨_, Finset.mem_range.2 this, rfl⟩)
  rw [Submodule.span_le, Finset.coe_image, Set.image_subset_iff]
  intro k hk
  apply mem_degreeLT.2
  exact lt_of_le_of_lt (degree_X_pow_le _) (WithBot.coe_lt_coe.2 <| Finset.mem_range.1 hk)

Degree-bounded polynomials as span of monomials: $\text{degreeLT}(R, n) = \operatorname{span}_R\{1, X, \ldots, X^{n-1}\}$

Informal description

For a commutative ring $R$ with decidable equality and a natural number $n$, the submodule of polynomials with degree less than $n$ is equal to the $R$-linear span of the finite set $\{X^0, X^1, \ldots, X^{n-1}\}$.

Polynomial.degreeLTEquiv definition

(R) [Semiring R] (n : ℕ) : degreeLT R n ≃ₗ[R] Fin n → R

Full source

/-- The first `n` coefficients on `degreeLT n` form a linear equivalence with `Fin n → R`. -/
def degreeLTEquiv (R) [Semiring R] (n : ℕ) : degreeLTdegreeLT R n ≃ₗ[R] Fin n → R where
  toFun p n := (↑p : R[X]).coeff n
  invFun f :=
    ⟨∑ i : Fin n, monomial i (f i),
      (degreeLT R n).sum_mem fun i _ =>
        mem_degreeLT.mpr
          (lt_of_le_of_lt (degree_monomial_le i (f i)) (WithBot.coe_lt_coe.mpr i.is_lt))⟩
  map_add' p q := by
    ext
    dsimp
    rw [coeff_add]
  map_smul' x p := by
    ext
    dsimp
    rw [coeff_smul]
    rfl
  left_inv := by
    rintro ⟨p, hp⟩
    ext1
    simp only [Submodule.coe_mk]
    by_cases hp0 : p = 0
    · subst hp0
      simp only [coeff_zero, LinearMap.map_zero, Finset.sum_const_zero]
    rw [mem_degreeLT, degree_eq_natDegree hp0, Nat.cast_lt] at hp
    conv_rhs => rw [p.as_sum_range' n hp, ← Fin.sum_univ_eq_sum_range]
  right_inv f := by
    ext i
    simp only [finset_sum_coeff, Submodule.coe_mk]
    rw [Finset.sum_eq_single i, coeff_monomial, if_pos rfl]
    · rintro j - hji
      rw [coeff_monomial, if_neg]
      rwa [← Fin.ext_iff]
    · intro h
      exact (h (Finset.mem_univ _)).elim

Linear equivalence between degree-bounded polynomials and coefficient functions

Informal description

For a semiring $R$ and natural number $n$, there exists a linear equivalence between the submodule of polynomials with degree less than $n$ and the space of functions from $\mathrm{Fin}(n)$ to $R$. Specifically: - The forward map takes a polynomial $p$ in $\mathrm{degreeLT}(R, n)$ to its coefficients as a function $i \mapsto p_i$ for $i \in \mathrm{Fin}(n)$. - The inverse map takes a function $f : \mathrm{Fin}(n) \to R$ and constructs the polynomial $\sum_{i} f(i) X^i$ in $\mathrm{degreeLT}(R, n)$. This equivalence preserves addition and scalar multiplication, making it an isomorphism of $R$-modules.

Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero theorem

{n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) : degreeLTEquiv _ _ ⟨p, hp⟩ = 0 ↔ p = 0

Full source

theorem degreeLTEquiv_eq_zero_iff_eq_zero {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) :
    degreeLTEquivdegreeLTEquiv _ _ ⟨p, hp⟩ = 0 ↔ p = 0 := by simp

$\text{degreeLTEquiv}_R(n)$ is injective on degree-bounded polynomials

Informal description

For any natural number $n$ and polynomial $p \in R[X]$ with degree less than $n$, the linear equivalence $\text{degreeLTEquiv}_R(n)$ maps $p$ to the zero function if and only if $p$ is the zero polynomial.

Polynomial.eval_eq_sum_degreeLTEquiv theorem

 {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) (x : R) : p.eval x = ∑ i, degreeLTEquiv _ _ ⟨p, hp⟩ i * x ^ (i : ℕ)

Full source

theorem eval_eq_sum_degreeLTEquiv {n : ℕ} {p : R[X]} (hp : p ∈ degreeLT R n) (x : R) :
    p.eval x = ∑ i, degreeLTEquiv _ _ ⟨p, hp⟩ i * x ^ (i : ℕ) := by
  simp_rw [eval_eq_sum]
  exact (sum_fin _ (by simp_rw [zero_mul, forall_const]) (mem_degreeLT.mp hp)).symm

Polynomial Evaluation as Finite Sum of Coefficients Times Powers

Informal description

For any natural number $n$, polynomial $p \in R[X]$ with degree less than $n$, and element $x \in R$, the evaluation of $p$ at $x$ equals the sum over $i \in \mathrm{Fin}(n)$ of the $i$-th coefficient of $p$ (given by the linear equivalence $\mathrm{degreeLTEquiv}_R(n)$) multiplied by $x^i$. That is, \[ p(x) = \sum_{i \in \mathrm{Fin}(n)} p_i \cdot x^i. \]

Polynomial.degreeLT_succ_eq_degreeLE theorem

{n : ℕ} : degreeLT R (n + 1) = degreeLE R n

Full source

theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R n := by
  ext x
  by_cases x_zero : x = 0
  · simp_rw [x_zero, Submodule.zero_mem]
  · rw [mem_degreeLT, mem_degreeLE, ← natDegree_lt_iff_degree_lt (by rwa [ne_eq]),
      ← natDegree_le_iff_degree_le, Nat.lt_succ]

Equality of Degree-Bounded Polynomial Submodules: $\text{degreeLT}(R, n+1) = \text{degreeLE}(R, n)$

Informal description

For any natural number $n$ and commutative ring $R$, the submodule of polynomials with degree strictly less than $n+1$ is equal to the submodule of polynomials with degree at most $n$, i.e., \[ \text{degreeLT}(R, n+1) = \text{degreeLE}(R, n). \]

Polynomial.monicEquivDegreeLT definition

[Nontrivial R] (n : ℕ) : { p : R[X] // p.Monic ∧ p.natDegree = n } ≃ degreeLT R n

Full source

/-- The equivalence between monic polynomials of degree `n` and polynomials of degree less than
`n`, formed by adding a term `X ^ n`. -/
def monicEquivDegreeLT [Nontrivial R] (n : ℕ) :
    { p : R[X] // p.Monic ∧ p.natDegree = n }{ p : R[X] // p.Monic ∧ p.natDegree = n } ≃ degreeLT R n where
  toFun p := ⟨p.1.eraseLead, by
    rcases p with ⟨p, hp, rfl⟩
    simp only [mem_degreeLT]
    refine lt_of_lt_of_le ?_ degree_le_natDegree
    exact degree_eraseLead_lt (ne_zero_of_ne_zero_of_monic one_ne_zero hp)⟩
  invFun := fun p =>
    ⟨X^n + p.1, monic_X_pow_add (mem_degreeLT.1 p.2), by
        rw [natDegree_add_eq_left_of_degree_lt]
        · simp
        · simp [mem_degreeLT.1 p.2]⟩
  left_inv := by
    rintro ⟨p, hp, rfl⟩
    ext1
    simp only
    conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]
    simp [Monic.def.1 hp, add_comm]
  right_inv := by
    rintro ⟨p, hp⟩
    ext1
    simp only
    rw [eraseLead_add_of_degree_lt_left]
    · simp
    · simp [mem_degreeLT.1 hp]

Equivalence between monic polynomials and degree-restricted polynomials

Informal description

For a nontrivial commutative ring $R$ and a natural number $n$, there is a bijection between the set of monic polynomials of degree $n$ in $R[X]$ and the submodule of polynomials with degree strictly less than $n$. The bijection is given by: - Forward direction: For a monic polynomial $p$ of degree $n$, remove its leading term to obtain a polynomial in $\text{degreeLT}(R, n)$. - Backward direction: For a polynomial $q \in \text{degreeLT}(R, n)$, construct the monic polynomial $X^n + q$ of degree $n$.

Polynomial.exists_degree_le_of_mem_span theorem

{s : Set R[X]} {p : R[X]} (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) : ∃ p' ∈ s, degree p ≤ degree p'

Full source

/-- For every polynomial `p` in the span of a set `s : Set R[X]`, there exists a polynomial of
  `p' ∈ s` with higher degree. See also `Polynomial.exists_degree_le_of_mem_span_of_finite`. -/
theorem exists_degree_le_of_mem_span {s : Set R[X]} {p : R[X]}
    (hs : s.Nonempty) (hp : p ∈ Submodule.span R s) :
    ∃ p' ∈ s, degree p ≤ degree p' := by
  by_contra! h
  by_cases hp_zero : p = 0
  · rw [hp_zero, degree_zero] at h
    rcases hs with ⟨x, hx⟩
    exact not_lt_bot (h x hx)
  · have : p ∈ degreeLT R (natDegree p) := by
      refine (Submodule.span_le.mpr fun p' p'_mem => ?_) hp
      rw [SetLike.mem_coe, mem_degreeLT, Nat.cast_withBot]
      exact lt_of_lt_of_le (h p' p'_mem) degree_le_natDegree
    rwa [mem_degreeLT, Nat.cast_withBot, degree_eq_natDegree hp_zero,
      Nat.cast_withBot, lt_self_iff_false] at this

Existence of Dominant Degree Polynomial in Span: $\exists p' \in s, \deg(p) \leq \deg(p')$ for $p \in \operatorname{span}_R s$

Informal description

For any nonempty set $s$ of polynomials over a commutative ring $R$ and any polynomial $p$ in the span of $s$, there exists a polynomial $p' \in s$ such that the degree of $p$ is less than or equal to the degree of $p'$.

Polynomial.exists_degree_le_of_mem_span_of_finite theorem

 {s : Set R[X]} (s_fin : s.Finite) (hs : s.Nonempty) :
  ∃ p' ∈ s, ∀ (p : R[X]), p ∈ Submodule.span R s → degree p ≤ degree p'

Full source

/-- A stronger version of `Polynomial.exists_degree_le_of_mem_span` under the assumption that the
set `s : R[X]` is finite. There exists a polynomial `p' ∈ s` whose degree dominates the degree of
every element of `p ∈ span R s`. -/
theorem exists_degree_le_of_mem_span_of_finite {s : Set R[X]} (s_fin : s.Finite) (hs : s.Nonempty) :
    ∃ p' ∈ s, ∀ (p : R[X]), p ∈ Submodule.span R s → degree p ≤ degree p' := by
  rcases Set.Finite.exists_maximal_wrt degree s s_fin hs with ⟨a, has, hmax⟩
  refine ⟨a, has, fun p hp => ?_⟩
  rcases exists_degree_le_of_mem_span hs hp with ⟨p', hp'⟩
  by_cases h : degree a ≤ degree p'
  · rw [← hmax p' hp'.left h] at hp'; exact hp'.right
  · exact le_trans hp'.right (not_le.mp h).le

Existence of Maximal Degree Polynomial in Finite Span: $\exists p' \in s, \forall p \in \operatorname{span}_R s, \deg(p) \leq \deg(p')$

Informal description

For any finite nonempty set $s$ of polynomials over a commutative ring $R$, there exists a polynomial $p' \in s$ such that for every polynomial $p$ in the span of $s$, the degree of $p$ is less than or equal to the degree of $p'$.

Polynomial.span_le_degreeLE_of_finite theorem

{s : Set R[X]} (s_fin : s.Finite) : ∃ n : ℕ, Submodule.span R s ≤ degreeLE R n

Full source

/-- The span of every finite set of polynomials is contained in a `degreeLE n` for some `n`. -/
theorem span_le_degreeLE_of_finite {s : Set R[X]} (s_fin : s.Finite) :
    ∃ n : ℕ, Submodule.span R s ≤ degreeLE R n := by
  by_cases s_emp : s.Nonempty
  · rcases exists_degree_le_of_mem_span_of_finite s_fin s_emp with ⟨p', _, hp'max⟩
    exact ⟨natDegree p', fun p hp => mem_degreeLE.mpr ((hp'max _ hp).trans degree_le_natDegree)⟩
  · rw [Set.not_nonempty_iff_eq_empty] at s_emp
    rw [s_emp, Submodule.span_empty]
    exact ⟨0, bot_le⟩

Finite Span of Polynomials is Contained in a Degree-Bounded Submodule

Informal description

For any finite set $s$ of polynomials over a commutative ring $R$, there exists a natural number $n$ such that the span of $s$ is contained in the submodule of polynomials with degree at most $n$, i.e., $\operatorname{span}_R s \subseteq \{ f \in R[X] \mid \deg(f) \leq n \}$.

Polynomial.span_of_finite_le_degreeLT theorem

{s : Set R[X]} (s_fin : s.Finite) : ∃ n : ℕ, Submodule.span R s ≤ degreeLT R n

Full source

/-- The span of every finite set of polynomials is contained in a `degreeLT n` for some `n`. -/
theorem span_of_finite_le_degreeLT {s : Set R[X]} (s_fin : s.Finite) :
    ∃ n : ℕ, Submodule.span R s ≤ degreeLT R n := by
  rcases span_le_degreeLE_of_finite s_fin with ⟨n, _⟩
  exact ⟨n + 1, by rwa [degreeLT_succ_eq_degreeLE]⟩

Finite Span of Polynomials is Contained in a Strict Degree-Bounded Submodule

Informal description

For any finite set $s$ of polynomials over a commutative ring $R$, there exists a natural number $n$ such that the span of $s$ is contained in the submodule of polynomials with degree strictly less than $n$, i.e., $\operatorname{span}_R s \subseteq \{ f \in R[X] \mid \deg(f) < n \}$.

Polynomial.not_finite theorem

[Nontrivial R] : ¬Module.Finite R R[X]

Full source

/-- If `R` is a nontrivial ring, the polynomials `R[X]` are not finite as an `R`-module. When `R` is
a field, this is equivalent to `R[X]` being an infinite-dimensional vector space over `R`. -/
theorem not_finite [Nontrivial R] : ¬ Module.Finite R R[X] := by
  rw [Module.finite_def, Submodule.fg_def]
  push_neg
  intro s hs contra
  rcases span_le_degreeLE_of_finite hs with ⟨n,hn⟩
  have : ((X : R[X]) ^ (n + 1)) ∈ Polynomial.degreeLE R ↑n := by
    rw [contra] at hn
    exact hn Submodule.mem_top
  rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this
  exact one_ne_zero this

Non-finiteness of Polynomial Ring as Module over Nontrivial Ring

Informal description

If $R$ is a nontrivial ring, then the polynomial ring $R[X]$ is not finitely generated as an $R$-module.

Polynomial.geom_sum_X_comp_X_add_one_eq_sum theorem

 (n : ℕ) :
  (∑ i ∈ range n, (X : R[X]) ^ i).comp (X + 1) = (Finset.range n).sum fun i : ℕ => (n.choose (i + 1) : R[X]) * X ^ i

Full source

theorem geom_sum_X_comp_X_add_one_eq_sum (n : ℕ) :
    (∑ i ∈ range n, (X : R[X]) ^ i).comp (X + 1) =
      (Finset.range n).sum fun i : ℕ => (n.choose (i + 1) : R[X]) * X ^ i := by
  ext i
  trans (n.choose (i + 1) : R); swap
  · simp only [finset_sum_coeff, ← C_eq_natCast, coeff_C_mul_X_pow]
    rw [Finset.sum_eq_single i, if_pos rfl]
    · simp +contextual only [@eq_comm _ i, if_false, eq_self_iff_true,
        imp_true_iff]
    · simp +contextual only [Nat.lt_add_one_iff, Nat.choose_eq_zero_of_lt,
        Nat.cast_zero, Finset.mem_range, not_lt, eq_self_iff_true, if_true, imp_true_iff]
  induction' n with n ih generalizing i
  · dsimp; simp only [zero_comp, coeff_zero, Nat.cast_zero]
  · simp only [geom_sum_succ', ih, add_comp, X_pow_comp, coeff_add, Nat.choose_succ_succ,
    Nat.cast_add, coeff_X_add_one_pow]

Geometric Sum Composition Identity: $(\sum_{i=0}^{n-1} X^i) \circ (X + 1) = \sum_{i=0}^{n-1} \binom{n}{i+1} X^i$

Informal description

For any natural number $n$, the composition of the geometric sum $\sum_{i=0}^{n-1} X^i$ with the polynomial $X + 1$ equals the sum $\sum_{i=0}^{n-1} \binom{n}{i+1} X^i$ in the polynomial ring $R[X]$.

Polynomial.Monic.geom_sum theorem

{P : R[X]} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, P ^ i).Monic

Full source

theorem Monic.geom_sum {P : R[X]} (hP : P.Monic) (hdeg : 0 < P.natDegree) {n : ℕ} (hn : n ≠ 0) :
    (∑ i ∈ range n, P ^ i).Monic := by
  nontriviality R
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
  rw [geom_sum_succ']
  refine (hP.pow _).add_of_left ?_
  refine lt_of_le_of_lt (degree_sum_le _ _) ?_
  rw [Finset.sup_lt_iff]
  · simp only [Finset.mem_range, degree_eq_natDegree (hP.pow _).ne_zero]
    simp only [Nat.cast_lt, hP.natDegree_pow]
    intro k
    exact nsmul_lt_nsmul_left hdeg
  · rw [bot_lt_iff_ne_bot, Ne, degree_eq_bot]
    exact (hP.pow _).ne_zero

Monicity of Geometric Sum of Monic Polynomials: $\sum_{i=0}^{n-1} P^i$ is monic when $P$ is monic and $\deg P > 0$

Informal description

Let $P$ be a monic polynomial in $R[X]$ with positive degree, and let $n$ be a nonzero natural number. Then the geometric sum $\sum_{i=0}^{n-1} P^i$ is also monic.

Polynomial.Monic.geom_sum' theorem

{P : R[X]} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, P ^ i).Monic

Full source

theorem Monic.geom_sum' {P : R[X]} (hP : P.Monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) :
    (∑ i ∈ range n, P ^ i).Monic :=
  hP.geom_sum (natDegree_pos_iff_degree_pos.2 hdeg) hn

Monicity of Geometric Sum of Monic Polynomials: $\sum_{i=0}^{n-1} P^i$ is monic when $P$ is monic and $\deg P > 0$

Informal description

Let $P$ be a monic polynomial in $R[X]$ with positive degree, and let $n$ be a nonzero natural number. Then the geometric sum $\sum_{i=0}^{n-1} P^i$ is also monic.

Polynomial.monic_geom_sum_X theorem

{n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, (X : R[X]) ^ i).Monic

Full source

theorem monic_geom_sum_X {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, (X : R[X]) ^ i).Monic := by
  nontriviality R
  apply monic_X.geom_sum _ hn
  simp only [natDegree_X, zero_lt_one]

Monicity of Geometric Sum of Powers of $X$: $\sum_{i=0}^{n-1} X^i$ is monic for $n \neq 0$

Informal description

For any nonzero natural number $n$, the geometric sum $\sum_{i=0}^{n-1} X^i$ is a monic polynomial in $R[X]$, where $X$ is the polynomial variable.

Polynomial.restriction definition

(p : R[X]) : Polynomial (Subring.closure (↑p.coeffs : Set R))

Full source

/-- Given a polynomial, return the polynomial whose coefficients are in
the ring closure of the original coefficients. -/
def restriction (p : R[X]) : Polynomial (Subring.closure (↑p.coeffs : Set R)) :=
  ∑ i ∈ p.support,
    monomial i
      (⟨p.coeff i,
          letI := Classical.decEq R
          if H : p.coeff i = 0 then H.symm ▸ (Subring.closure _).zero_mem
          else Subring.subset_closure (p.coeff_mem_coeffs _ H)⟩ :
        Subring.closure (↑p.coeffs : Set R))

Polynomial with coefficients in the subring generated by original coefficients

Informal description

Given a polynomial $p$ with coefficients in a ring $R$, the function returns a new polynomial with coefficients in the subring of $R$ generated by the coefficients of $p$. Specifically, for each coefficient $a_i$ of $p$, if $a_i \neq 0$, then $a_i$ is included in the subring closure of the coefficients of $p$.

Polynomial.coeff_restriction theorem

{p : R[X]} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n

Full source

@[simp]
theorem coeff_restriction {p : R[X]} {n : ℕ} : ↑(coeff (restriction p) n) = coeff p n := by
  classical
  simp only [restriction, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

Preservation of Coefficients under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$ and any natural number $n$, the $n$-th coefficient of the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is equal to the $n$-th coefficient of $p$ when viewed in $R$. In other words, the coefficients are preserved under the restriction operation.

Polynomial.coeff_restriction' theorem

{p : R[X]} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n

Full source

theorem coeff_restriction' {p : R[X]} {n : ℕ} : (coeff (restriction p) n).1 = coeff p n := by
  simp

Coefficient Preservation under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$ and any natural number $n$, the $n$-th coefficient of the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is equal to the $n$-th coefficient of $p$ when viewed in $R$.

Polynomial.support_restriction theorem

(p : R[X]) : support (restriction p) = support p

Full source

@[simp]
theorem support_restriction (p : R[X]) : support (restriction p) = support p := by
  ext i
  simp only [mem_support_iff, not_iff_not, Ne]
  conv_rhs => rw [← coeff_restriction]
  exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

Support Preservation under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$, the support of the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is equal to the support of $p$. Here, the support of a polynomial is the set of indices where its coefficients are nonzero.

Polynomial.map_restriction theorem

{R : Type u} [CommRing R] (p : R[X]) : p.restriction.map (algebraMap _ _) = p

Full source

@[simp]
theorem map_restriction {R : Type u} [CommRing R] (p : R[X]) :
    p.restriction.map (algebraMap _ _) = p :=
  ext fun n => by rw [coeff_map, Algebra.algebraMap_ofSubring_apply, coeff_restriction]

Restriction and Canonical Embedding Preserve Polynomial Identity

Informal description

For any polynomial $p$ with coefficients in a commutative ring $R$, the polynomial obtained by first restricting $p$ to the subring generated by its coefficients and then mapping it back to $R$ via the canonical algebra map is equal to $p$ itself. In other words, the composition of restriction and the canonical embedding is the identity on $p$.

Polynomial.degree_restriction theorem

{p : R[X]} : (restriction p).degree = p.degree

Full source

@[simp]
theorem degree_restriction {p : R[X]} : (restriction p).degree = p.degree := by simp [degree]

Degree Preservation under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$, the degree of the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is equal to the degree of $p$.

Polynomial.natDegree_restriction theorem

{p : R[X]} : (restriction p).natDegree = p.natDegree

Full source

@[simp]
theorem natDegree_restriction {p : R[X]} : (restriction p).natDegree = p.natDegree := by
  simp [natDegree]

Natural Degree Preservation under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$, the natural degree of the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is equal to the natural degree of $p$.

Polynomial.monic_restriction theorem

{p : R[X]} : Monic (restriction p) ↔ Monic p

Full source

@[simp]
theorem monic_restriction {p : R[X]} : MonicMonic (restriction p) ↔ Monic p := by
  simp only [Monic, leadingCoeff, natDegree_restriction]
  rw [← @coeff_restriction _ _ p]
  exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

Monicity Preservation under Polynomial Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$, the restricted polynomial (with coefficients in the subring generated by $p$'s coefficients) is monic if and only if $p$ is monic.

Polynomial.restriction_zero theorem

: restriction (0 : R[X]) = 0

Full source

@[simp]
theorem restriction_zero : restriction (0 : R[X]) = 0 := by
  simp only [restriction, Finset.sum_empty, support_zero]

Restriction of Zero Polynomial is Zero

Informal description

The restriction of the zero polynomial is equal to the zero polynomial, i.e., $\text{restriction}(0) = 0$.

Polynomial.restriction_one theorem

: restriction (1 : R[X]) = 1

Full source

@[simp]
theorem restriction_one : restriction (1 : R[X]) = 1 :=
  ext fun i => Subtype.eq <| by rw [coeff_restriction', coeff_one, coeff_one]; split_ifs <;> rfl

Restriction of One Polynomial is One

Informal description

The restriction of the constant polynomial $1$ is equal to the constant polynomial $1$, i.e., $\text{restriction}(1) = 1$.

Polynomial.eval₂_restriction theorem

{p : R[X]} : eval₂ f x p = eval₂ (f.comp (Subring.subtype (Subring.closure (p.coeffs : Set R)))) x p.restriction

Full source

theorem eval₂_restriction {p : R[X]} :
    eval₂ f x p =
      eval₂ (f.comp (Subring.subtype (Subring.closure (p.coeffs : Set R)))) x p.restriction := by
  simp only [eval₂_eq_sum, sum, support_restriction, ← @coeff_restriction _ _ p, RingHom.comp_apply,
    Subring.coe_subtype]

Equality of Polynomial Evaluations under Restriction

Informal description

For any polynomial $p$ with coefficients in a ring $R$, the evaluation of $p$ at $x$ via the ring homomorphism $f$ is equal to the evaluation of the restricted polynomial $p.\text{restriction}$ at $x$ via the composition of $f$ with the inclusion map of the subring generated by the coefficients of $p$. In other words, we have: \[ \text{eval}_2(f, x, p) = \text{eval}_2(f \circ \iota, x, p.\text{restriction}) \] where $\iota$ is the inclusion map of the subring $\text{Subring.closure}(p.\text{coeffs})$ into $R$.

Polynomial.toSubring definition

(hp : (↑p.coeffs : Set R) ⊆ T) : T[X]

Full source

/-- Given a polynomial `p` and a subring `T` that contains the coefficients of `p`,
return the corresponding polynomial whose coefficients are in `T`. -/
def toSubring (hp : (↑p.coeffs : Set R) ⊆ T) : T[X] :=
  ∑ i ∈ p.support,
    monomial i
      (⟨p.coeff i,
        letI := Classical.decEq R
        if H : p.coeff i = 0 then H.symm ▸ T.zero_mem else hp (p.coeff_mem_coeffs _ H)⟩ : T)

Polynomial restriction to a subring

Informal description

Given a polynomial $p$ with coefficients in a ring $R$ and a subring $T$ of $R$ that contains all the coefficients of $p$, the function returns the polynomial with coefficients in $T$ obtained by restricting each coefficient of $p$ to $T$.

Polynomial.coeff_toSubring theorem

{n : ℕ} : ↑(coeff (toSubring p T hp) n) = coeff p n

Full source

@[simp]
theorem coeff_toSubring {n : ℕ} : ↑(coeff (toSubring p T hp) n) = coeff p n := by
  classical
  simp only [toSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

Coefficient Preservation under Polynomial Restriction to Subring

Informal description

For any natural number $n$, the $n$-th coefficient of the polynomial $p$ restricted to a subring $T$ (where all coefficients of $p$ lie in $T$) is equal to the $n$-th coefficient of $p$ when viewed in the larger ring $R$.

Polynomial.coeff_toSubring' theorem

{n : ℕ} : (coeff (toSubring p T hp) n).1 = coeff p n

Full source

theorem coeff_toSubring' {n : ℕ} : (coeff (toSubring p T hp) n).1 = coeff p n := by
  simp

Coefficient Preservation under Polynomial Restriction to Subring (Unwrapped)

Informal description

For any natural number $n$, the $n$-th coefficient of the polynomial $p$ restricted to a subring $T$ (where all coefficients of $p$ lie in $T$) is equal to the $n$-th coefficient of $p$ when viewed in the larger ring $R$.

Polynomial.support_toSubring theorem

: support (toSubring p T hp) = support p

Full source

@[simp]
theorem support_toSubring : support (toSubring p T hp) = support p := by
  ext i
  simp only [mem_support_iff, not_iff_not, Ne]
  conv_rhs => rw [← coeff_toSubring p T hp]
  exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

Support Preservation under Polynomial Restriction to Subring

Informal description

For a polynomial $p$ with coefficients in a ring $R$ and a subring $T \subseteq R$ containing all coefficients of $p$, the support of the polynomial $p$ restricted to $T$ is equal to the support of $p$ in $R$. That is, $\text{support}(\text{toSubring}(p, T, hp)) = \text{support}(p)$.

Polynomial.degree_toSubring theorem

: (toSubring p T hp).degree = p.degree

Full source

@[simp]
theorem degree_toSubring : (toSubring p T hp).degree = p.degree := by simp [degree]

Degree Preservation under Polynomial Restriction to Subring

Informal description

For a polynomial $p$ with coefficients in a ring $R$ and a subring $T \subseteq R$ containing all coefficients of $p$, the degree of the polynomial $p$ restricted to $T$ is equal to the degree of $p$ in $R$. That is, $\deg(\text{toSubring}(p, T, hp)) = \deg(p)$.

Polynomial.natDegree_toSubring theorem

: (toSubring p T hp).natDegree = p.natDegree

Full source

@[simp]
theorem natDegree_toSubring : (toSubring p T hp).natDegree = p.natDegree := by simp [natDegree]

Natural Degree Preservation under Polynomial Restriction to Subring

Informal description

For a polynomial $p$ with coefficients in a ring $R$ and a subring $T \subseteq R$ containing all coefficients of $p$, the natural degree of the polynomial $p$ restricted to $T$ is equal to the natural degree of $p$ in $R$. That is, $\text{natDegree}(\text{toSubring}(p, T, hp)) = \text{natDegree}(p)$.

Polynomial.monic_toSubring theorem

: Monic (toSubring p T hp) ↔ Monic p

Full source

@[simp]
theorem monic_toSubring : MonicMonic (toSubring p T hp) ↔ Monic p := by
  simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]
  exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

Monicity Preservation under Polynomial Restriction to Subring

Informal description

For a polynomial $p$ with coefficients in a ring $R$ and a subring $T \subseteq R$ containing all coefficients of $p$, the restricted polynomial $\text{toSubring}(p, T, hp)$ is monic if and only if $p$ is monic.

Polynomial.toSubring_zero theorem

: toSubring (0 : R[X]) T (by simp [coeffs]) = 0

Full source

@[simp]
theorem toSubring_zero : toSubring (0 : R[X]) T (by simp [coeffs]) = 0 := by
  ext i
  simp

Zero Polynomial Restriction to Subring Yields Zero Polynomial

Informal description

The restriction of the zero polynomial to a subring $T$ is equal to the zero polynomial in $T[X]$.

Polynomial.toSubring_one theorem

: toSubring (1 : R[X]) T (Set.Subset.trans coeffs_one <| Finset.singleton_subset_set_iff.2 T.one_mem) = 1

Full source

@[simp]
theorem toSubring_one :
    toSubring (1 : R[X]) T
        (Set.Subset.trans coeffs_one <| Finset.singleton_subset_set_iff.2 T.one_mem) =
      1 :=
  ext fun i => Subtype.eq <| by
    rw [coeff_toSubring', coeff_one, coeff_one, apply_ite Subtype.val, ZeroMemClass.coe_zero,
      OneMemClass.coe_one]

Restriction of Unity Polynomial to Subring Preserves Unity

Informal description

Let $R$ be a ring and $T$ be a subring of $R$. The restriction of the polynomial $1 \in R[X]$ to $T[X]$, denoted by $\text{toSubring}(1, T)$, is equal to the polynomial $1 \in T[X]$. This holds because the coefficient of the constant polynomial $1$ lies in $T$ (as $T$ contains the multiplicative identity of $R$).

Polynomial.map_toSubring theorem

: (p.toSubring T hp).map (Subring.subtype T) = p

Full source

@[simp]
theorem map_toSubring : (p.toSubring T hp).map (Subring.subtype T) = p := by
  ext n
  simp [coeff_map]

Polynomial Restriction and Inclusion Map Yields Original Polynomial

Informal description

Let $R$ be a ring and $T$ be a subring of $R$. For any polynomial $p \in R[X]$ whose coefficients all lie in $T$, the polynomial obtained by first restricting $p$ to $T[X]$ (via `toSubring`) and then mapping it back to $R[X]$ via the inclusion map $T \hookrightarrow R$ is equal to the original polynomial $p$.

Polynomial.ofSubring definition

(p : T[X]) : R[X]

Full source

/-- Given a polynomial whose coefficients are in some subring, return
the corresponding polynomial whose coefficients are in the ambient ring. -/
def ofSubring (p : T[X]) : R[X] :=
  ∑ i ∈ p.support, monomial i (p.coeff i : R)

Polynomial lift from subring to ambient ring

Informal description

Given a polynomial $p$ with coefficients in a subring $T$ of a ring $R$, the function returns the corresponding polynomial with coefficients in the ambient ring $R$ by lifting each coefficient from $T$ to $R$. Specifically, the polynomial is reconstructed as $\sum_{i \in \text{support}(p)} x^i \cdot (p_i : R)$, where $p_i$ are the coefficients of $p$ in $T$ and $x^i$ denotes the monomial of degree $i$.

Polynomial.coeff_ofSubring theorem

(p : T[X]) (n : ℕ) : coeff (ofSubring T p) n = (coeff p n : T)

Full source

theorem coeff_ofSubring (p : T[X]) (n : ℕ) : coeff (ofSubring T p) n = (coeff p n : T) := by
  simp only [ofSubring, coeff_monomial, finset_sum_coeff, mem_support_iff, Finset.sum_ite_eq',
    ite_eq_right_iff, Ne, ite_not, Classical.not_not, ite_eq_left_iff]
  intro h
  rw [h, ZeroMemClass.coe_zero]

Coefficient Preservation in Polynomial Lift from Subring to Ambient Ring

Informal description

For any polynomial $p$ with coefficients in a subring $T$ of a ring $R$, and for any natural number $n$, the $n$-th coefficient of the polynomial obtained by lifting $p$ to $R[X]$ via `ofSubring` is equal to the $n$-th coefficient of $p$ viewed as an element of $T$.

Polynomial.coeffs_ofSubring theorem

{p : T[X]} : (↑(p.ofSubring T).coeffs : Set R) ⊆ T

Full source

@[simp]
theorem coeffs_ofSubring {p : T[X]} : (↑(p.ofSubring T).coeffs : Set R) ⊆ T := by
  classical
  intro i hi
  simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
    (Finset.coe_image)] at hi
  rcases hi with ⟨n, _, h'n⟩
  rw [← h'n, coeff_ofSubring]
  exact Subtype.mem (coeff p n : T)

Coefficient Subset Property for Polynomial Lift from Subring to Ambient Ring

Informal description

For any polynomial $p$ with coefficients in a subring $T$ of a ring $R$, the set of coefficients of the polynomial obtained by lifting $p$ to $R[X]$ via `ofSubring` is a subset of $T$ when viewed as elements of $R$.

Ideal.ofPolynomial definition

(I : Ideal R[X]) : Submodule R R[X]

Full source

/-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
def ofPolynomial (I : Ideal R[X]) : Submodule R R[X] where
  carrier := I.carrier
  zero_mem' := I.zero_mem
  add_mem' := I.add_mem
  smul_mem' c x H := by
    rw [← C_mul']
    exact I.mul_mem_left _ H

Submodule associated to a polynomial ideal

Informal description

Given an ideal $ I $ of the polynomial ring $ R[X] $, the function maps $ I $ to the $ R $-submodule of $ R[X] $ with the same underlying set as $ I $, where the submodule structure is defined by the ideal properties: it contains zero, is closed under addition, and is closed under scalar multiplication by elements of $ R $ (via multiplication by constant polynomials).

Ideal.mem_ofPolynomial theorem

(x) : x ∈ I.ofPolynomial ↔ x ∈ I

Full source

theorem mem_ofPolynomial (x) : x ∈ I.ofPolynomialx ∈ I.ofPolynomial ↔ x ∈ I :=
  Iff.rfl

Membership Equivalence for Polynomial Ideal and Associated Submodule

Informal description

For any polynomial $x$ in the polynomial ring $R[X]$, $x$ belongs to the submodule $I.\text{ofPolynomial}$ if and only if $x$ belongs to the ideal $I$.

Ideal.degreeLE definition

(n : WithBot ℕ) : Submodule R R[X]

Full source

/-- Given an ideal `I` of `R[X]`, make the `R`-submodule of `I`
consisting of polynomials of degree ≤ `n`. -/
def degreeLE (n : WithBot ℕ) : Submodule R R[X] :=
  Polynomial.degreeLEPolynomial.degreeLE R n ⊓ I.ofPolynomial

Submodule of polynomials in an ideal with bounded degree

Informal description

For an ideal $ I $ of the polynomial ring $ R[X] $ and an extended natural number $ n \in \mathbb{N} \cup \{\bot\} $, the $ R $-submodule $ \text{degreeLE}(I, n) $ consists of all polynomials in $ I $ with degree at most $ n $. This is defined as the intersection of the submodule of polynomials of degree at most $ n $ with the submodule associated to the ideal $ I $.

Ideal.leadingCoeffNth definition

(n : ℕ) : Ideal R

Full source

/-- Given an ideal `I` of `R[X]`, make the ideal in `R` of
leading coefficients of polynomials in `I` with degree ≤ `n`. -/
def leadingCoeffNth (n : ℕ) : Ideal R :=
  (I.degreeLE n).map <| lcoeff R n

Ideal of leading coefficients of bounded degree polynomials

Informal description

For an ideal $ I $ of the polynomial ring $ R[X] $ and a natural number $ n $, the ideal $ \text{leadingCoeffNth}(I, n) $ in $ R $ consists of the leading coefficients of all polynomials in $ I $ with degree at most $ n $. This is obtained by mapping the submodule of polynomials in $ I $ with degree at most $ n $ via the leading coefficient function for degree $ n $.

Ideal.leadingCoeff definition

: Ideal R

Full source

/-- Given an ideal `I` in `R[X]`, make the ideal in `R` of the
leading coefficients in `I`. -/
def leadingCoeff : Ideal R :=
  ⨆ n : ℕ, I.leadingCoeffNth n

Ideal of leading coefficients in a polynomial ring

Informal description

Given an ideal $ I $ in the polynomial ring $ R[X] $, the ideal $ \text{leadingCoeff}(I) $ in $ R $ consists of the leading coefficients of all polynomials in $ I $. It is defined as the supremum of the ideals $ \text{leadingCoeffNth}(I, n) $ for all natural numbers $ n $, where each $ \text{leadingCoeffNth}(I, n) $ is the ideal of leading coefficients of polynomials in $ I $ with degree at most $ n $.

Ideal.polynomial_mem_ideal_of_coeff_mem_ideal theorem

(I : Ideal R[X]) (p : R[X]) (hp : ∀ n : ℕ, p.coeff n ∈ I.comap (C : R →+* R[X])) : p ∈ I

Full source

/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself -/
theorem polynomial_mem_ideal_of_coeff_mem_ideal (I : Ideal R[X]) (p : R[X])
    (hp : ∀ n : ℕ, p.coeff n ∈ I.comap (C : R →+* R[X])) : p ∈ I :=
  sum_C_mul_X_pow_eq p ▸ Submodule.sum_mem I fun n _ => I.mul_mem_right _ (hp n)

Polynomial Membership via Coefficient Membership in Ideal Preimage

Informal description

Let $I$ be an ideal in the polynomial ring $R[X]$, and let $p \in R[X]$ be a polynomial such that for every natural number $n$, the coefficient of $X^n$ in $p$ belongs to the preimage of $I$ under the canonical embedding $C \colon R \to R[X]$. Then $p$ belongs to $I$.

Ideal.mem_map_C_iff theorem

{I : Ideal R} {f : R[X]} : f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X]) ↔ ∀ n : ℕ, f.coeff n ∈ I

Full source

/-- The push-forward of an ideal `I` of `R` to `R[X]` via inclusion
 is exactly the set of polynomials whose coefficients are in `I` -/
theorem mem_map_C_iff {I : Ideal R} {f : R[X]} :
    f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X])f ∈ (Ideal.map (C : R →+* R[X]) I : Ideal R[X]) ↔ ∀ n : ℕ, f.coeff n ∈ I := by
  constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · refine fun f g _ hg n => ?_
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [← sum_monomial_eq f]
    refine (I.map C : Ideal R[X]).sum_mem fun n _ => ?_
    simp only [← C_mul_X_pow_eq_monomial, ne_eq]
    rw [mul_comm]
    exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Polynomial Membership in Mapped Ideal via Coefficient Condition

Informal description

Let $I$ be an ideal of a ring $R$ and let $f \in R[X]$ be a polynomial. Then $f$ belongs to the ideal generated by the image of $I$ under the canonical embedding $C \colon R \to R[X]$ if and only if every coefficient of $f$ belongs to $I$.

Polynomial.ker_mapRingHom theorem

(f : R →+* S) : RingHom.ker (Polynomial.mapRingHom f) = (RingHom.ker f).map (C : R →+* R[X])

Full source

theorem _root_.Polynomial.ker_mapRingHom (f : R →+* S) :
    RingHom.ker (Polynomial.mapRingHom f) = (RingHom.ker f).map (C : R →+* R[X]) := by
  ext
  simp only [RingHom.mem_ker, coe_mapRingHom]
  rw [mem_map_C_iff, Polynomial.ext_iff]
  simp [RingHom.mem_ker]

Kernel of Polynomial Map Induced by Ring Homomorphism

Informal description

Let $f \colon R \to S$ be a ring homomorphism. The kernel of the induced polynomial ring homomorphism $\text{mapRingHom}(f) \colon R[X] \to S[X]$ is equal to the ideal generated by the image of the kernel of $f$ under the canonical embedding $C \colon R \to R[X]$. In other words, \[ \ker(\text{mapRingHom}(f)) = (C(\ker f))R[X]. \]

Ideal.mem_leadingCoeffNth theorem

(n : ℕ) (x) : x ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, degree p ≤ n ∧ p.leadingCoeff = x

Full source

theorem mem_leadingCoeffNth (n : ℕ) (x) :
    x ∈ I.leadingCoeffNth nx ∈ I.leadingCoeffNth n ↔ ∃ p ∈ I, degree p ≤ n ∧ p.leadingCoeff = x := by
  simp only [leadingCoeffNth, degreeLE, Submodule.mem_map, lcoeff_apply, Submodule.mem_inf,
    mem_degreeLE]
  constructor
  · rintro ⟨p, ⟨hpdeg, hpI⟩, rfl⟩
    rcases lt_or_eq_of_le hpdeg with hpdeg | hpdeg
    · refine ⟨0, I.zero_mem, bot_le, ?_⟩
      rw [leadingCoeff_zero, eq_comm]
      exact coeff_eq_zero_of_degree_lt hpdeg
    · refine ⟨p, hpI, le_of_eq hpdeg, ?_⟩
      rw [Polynomial.leadingCoeff, natDegree, hpdeg, Nat.cast_withBot, WithBot.unbotD_coe]
  · rintro ⟨p, hpI, hpdeg, rfl⟩
    have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
    refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
    · apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]
    · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Characterization of Leading Coefficient Ideal Membership: $x \in \text{leadingCoeffNth}(I, n) \leftrightarrow \exists p \in I, \deg(p) \leq n \land \text{lead}(p) = x$

Informal description

For an ideal $I$ of the polynomial ring $R[X]$, a natural number $n$, and an element $x \in R$, we have $x \in \text{leadingCoeffNth}(I, n)$ if and only if there exists a polynomial $p \in I$ such that $\deg(p) \leq n$ and the leading coefficient of $p$ equals $x$.

Ideal.mem_leadingCoeffNth_zero theorem

(x) : x ∈ I.leadingCoeffNth 0 ↔ C x ∈ I

Full source

theorem mem_leadingCoeffNth_zero (x) : x ∈ I.leadingCoeffNth 0x ∈ I.leadingCoeffNth 0 ↔ C x ∈ I :=
  (mem_leadingCoeffNth _ _ _).trans
    ⟨fun ⟨p, hpI, hpdeg, hpx⟩ => by
      rwa [← hpx, Polynomial.leadingCoeff,
        Nat.eq_zero_of_le_zero (natDegree_le_of_degree_le hpdeg), ← eq_C_of_degree_le_zero hpdeg],
      fun hx => ⟨C x, hx, degree_C_le, leadingCoeff_C x⟩⟩

Characterization of Leading Coefficient Ideal Membership for Degree Zero: $x \in \text{leadingCoeffNth}(I, 0) \leftrightarrow C(x) \in I$

Informal description

For any element $x$ in the ring $R$, $x$ belongs to the leading coefficient ideal $\text{leadingCoeffNth}(I, 0)$ if and only if the constant polynomial $C(x)$ is an element of the ideal $I$.

Ideal.leadingCoeffNth_mono theorem

{m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n

Full source

theorem leadingCoeffNth_mono {m n : ℕ} (H : m ≤ n) : I.leadingCoeffNth m ≤ I.leadingCoeffNth n := by
  intro r hr
  simp only [SetLike.mem_coe, mem_leadingCoeffNth] at hr ⊢
  rcases hr with ⟨p, hpI, hpdeg, rfl⟩
  refine ⟨p * X ^ (n - m), I.mul_mem_right _ hpI, ?_, leadingCoeff_mul_X_pow⟩
  refine le_trans (degree_mul_le _ _) ?_
  refine le_trans (add_le_add hpdeg (degree_X_pow_le _)) ?_
  rw [← Nat.cast_add, add_tsub_cancel_of_le H]

Monotonicity of Leading Coefficient Ideals with Respect to Degree

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the ideal $\text{leadingCoeffNth}(I, m)$ is contained in the ideal $\text{leadingCoeffNth}(I, n)$. Here, $\text{leadingCoeffNth}(I, k)$ denotes the ideal of leading coefficients of all polynomials in $I$ with degree at most $k$.

Ideal.mem_leadingCoeff theorem

(x) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x

Full source

theorem mem_leadingCoeff (x) : x ∈ I.leadingCoeffx ∈ I.leadingCoeff ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x := by
  rw [leadingCoeff, Submodule.mem_iSup_of_directed]
  · simp only [mem_leadingCoeffNth]
    constructor
    · rintro ⟨i, p, hpI, _, rfl⟩
      exact ⟨p, hpI, rfl⟩
    rintro ⟨p, hpI, rfl⟩
    exact ⟨natDegree p, p, hpI, degree_le_natDegree, rfl⟩
  intro i j
  exact
    ⟨i + j, I.leadingCoeffNth_mono (Nat.le_add_right _ _),
      I.leadingCoeffNth_mono (Nat.le_add_left _ _)⟩

Characterization of Membership in Leading Coefficient Ideal: $x \in \text{leadingCoeff}(I) \leftrightarrow \exists p \in I, \text{lc}(p) = x$

Informal description

For any element $x$ in the ring $R$, $x$ belongs to the leading coefficient ideal $\text{leadingCoeff}(I)$ if and only if there exists a polynomial $p \in I$ whose leading coefficient is $x$.

Polynomial.coeff_prod_mem_ideal_pow_tsub theorem

 {ι : Type*} (s : Finset ι) (f : ι → R[X]) (I : Ideal R) (n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k), (f i).coeff k ∈ I ^ (n i - k))
  (k : ℕ) : (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Full source

/-- If `I` is an ideal, and `pᵢ` is a finite family of polynomials each satisfying
`∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ` for some `nᵢ`, then `p = ∏ pᵢ` also satisfies `∀ k, pₖ ∈ Iⁿ⁻ᵏ` with `n = ∑ nᵢ`.
-/
theorem _root_.Polynomial.coeff_prod_mem_ideal_pow_tsub {ι : Type*} (s : Finset ι) (f : ι → R[X])
    (I : Ideal R) (n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) :
    (s.prod f).coeff k ∈ I ^ (s.sum n - k) := by
  classical
    induction' s using Finset.induction with a s ha hs generalizing k
    · rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    · rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact
        Ideal.mul_mem_mul (h _ (Finset.mem_insert.mpr <| Or.inl rfl) _)
          (hs (fun i hi k => h _ (Finset.mem_insert.mpr <| Or.inr hi) _) j)

Coefficient Condition for Product of Polynomials in Ideal Powers: $p_k \in I^{n-k}$ where $n = \sum n_i$

Informal description

Let $R$ be a ring, $I$ an ideal of $R$, and $\{p_i\}_{i \in \iota}$ a finite family of polynomials in $R[X]$ indexed by a finite set $\iota$. Suppose for each $i \in \iota$ there exists $n_i \in \mathbb{N}$ such that for every coefficient index $k$, the $k$-th coefficient of $p_i$ satisfies $(p_i)_k \in I^{n_i - k}$. Then for the product polynomial $p = \prod_{i \in \iota} p_i$ and any coefficient index $k$, we have $p_k \in I^{n - k}$ where $n = \sum_{i \in \iota} n_i$.

Ideal.polynomial_not_isField theorem

: ¬IsField R[X]

Full source

/-- `R[X]` is never a field for any ring `R`. -/
theorem polynomial_not_isField : ¬IsField R[X] := by
  nontriviality R
  intro hR
  obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero
  have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp
  have := degree_lt_degree_mul_X hp0
  rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this
  exact hp0 this

Polynomial Ring Over Any Ring is Not a Field

Informal description

For any ring $R$, the polynomial ring $R[X]$ is not a field.

Ideal.isPrime_map_C_iff_isPrime theorem

(P : Ideal R) : IsPrime (map (C : R →+* R[X]) P : Ideal R[X]) ↔ IsPrime P

Full source

/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`. -/
theorem isPrime_map_C_iff_isPrime (P : Ideal R) :
    IsPrimeIsPrime (map (C : R →+* R[X]) P : Ideal R[X]) ↔ IsPrime P := by
  -- Note: the following proof avoids quotient rings
  -- It can be golfed substantially by using something like
  -- `(Quotient.isDomain_iff_prime (map C P : Ideal R[X]))`
  constructor
  · intro H
    have := comap_isPrime C (map C P)
    convert this using 1
    ext x
    simp only [mem_comap, mem_map_C_iff]
    constructor
    · rintro h (- | n)
      · rwa [coeff_C_zero]
      · simp only [coeff_C_ne_zero (Nat.succ_ne_zero _), Submodule.zero_mem]
    · intro h
      simpa only [coeff_C_zero] using h 0
  · intro h
    constructor
    · rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]
      use 0
      rw [coeff_one_zero, ← eq_top_iff_one]
      exact h.1
    · intro f g
      simp only [mem_map_C_iff]
      contrapose!
      rintro ⟨hf, hg⟩
      classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m,n))).mpr rfl),
          Finset.sum_insert (Finset.not_mem_erase _ _), (P.add_mem_iff_left _).not]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          omega
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)

Prime Ideal Extension Criterion for Polynomial Rings: $P.R[X]$ is prime iff $P$ is prime

Informal description

Let $R$ be a ring and $P$ an ideal of $R$. The ideal $P.R[X]$ (the image of $P$ under the canonical embedding $C : R \to R[X]$) is a prime ideal of the polynomial ring $R[X]$ if and only if $P$ is a prime ideal of $R$.

Ideal.isPrime_map_C_of_isPrime theorem

{P : Ideal R} (H : IsPrime P) : IsPrime (map (C : R →+* R[X]) P : Ideal R[X])

Full source

/-- If `P` is a prime ideal of `R`, then `P.R[x]` is a prime ideal of `R[x]`. -/
theorem isPrime_map_C_of_isPrime {P : Ideal R} (H : IsPrime P) :
    IsPrime (map (C : R →+* R[X]) P : Ideal R[X]) :=
  (isPrime_map_C_iff_isPrime P).mpr H

Extension of Prime Ideal to Polynomial Ring: $P.R[X]$ is prime when $P$ is prime

Informal description

Let $R$ be a ring and $P$ a prime ideal of $R$. Then the ideal $P.R[X]$, defined as the image of $P$ under the canonical embedding $C : R \to R[X]$, is a prime ideal of the polynomial ring $R[X]$.

Ideal.is_fg_degreeLE theorem

[IsNoetherianRing R] (I : Ideal R[X]) (n : ℕ) : Submodule.FG (I.degreeLE n)

Full source

theorem is_fg_degreeLE [IsNoetherianRing R] (I : Ideal R[X]) (n : ℕ) :
    Submodule.FG (I.degreeLE n) :=
  letI := Classical.decEq R
  isNoetherian_submodule_left.1
    (isNoetherian_of_fg_of_noetherian _ ⟨_, degreeLE_eq_span_X_pow.symm⟩) _

Finitely generated property of bounded-degree polynomials in an ideal over a Noetherian ring

Informal description

Let $R$ be a Noetherian ring and $I$ an ideal of the polynomial ring $R[X]$. For any natural number $n$, the submodule of polynomials in $I$ with degree at most $n$ is finitely generated as an $R$-module.

span_le_of_C_coeff_mem theorem

(cf : ∀ i : ℕ, C (f.coeff i) ∈ I) : Ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I

Full source

/-- If the coefficients of a polynomial belong to an ideal, then that ideal contains
the ideal spanned by the coefficients of the polynomial. -/
theorem span_le_of_C_coeff_mem (cf : ∀ i : ℕ, CC (f.coeff i) ∈ I) :
    Ideal.span { g | ∃ i, g = C (f.coeff i) } ≤ I := by
  simp only [@eq_comm _ _ (C _)]
  exact (Ideal.span_le.trans range_subset_iff).mpr cf

Ideal containment criterion for polynomial coefficients

Informal description

Let $R$ be a ring and $f \in R[X]$ be a polynomial. If for every natural number $i$, the constant polynomial $C(f_i)$ (where $f_i$ is the $i$-th coefficient of $f$) belongs to an ideal $I$ of $R[X]$, then the ideal generated by the set $\{C(f_i) \mid i \in \mathbb{N}\}$ is contained in $I$.

mem_span_C_coeff theorem

: f ∈ Ideal.span {g : R[X] | ∃ i : ℕ, g = C (coeff f i)}

Full source

theorem mem_span_C_coeff : f ∈ Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) } := by
  let p := Ideal.span { g : R[X] | ∃ i : ℕ, g = C (coeff f i) }
  nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]
  refine Submodule.sum_mem _ fun n _hn => ?_
  dsimp
  have : CC (coeff f n) ∈ p := by
    apply subset_span
    rw [mem_setOf_eq]
    use n
  have : monomialmonomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
  convert this using 1
  simp only [monomial_mul_C, one_mul, smul_eq_mul]
  rw [← C_mul_X_pow_eq_monomial]

Polynomial Membership in Ideal Generated by Its Coefficients

Informal description

For any polynomial $f$ over a ring $R$, $f$ belongs to the ideal generated by the set $\{C(\text{coeff}(f, i)) \mid i \in \mathbb{N}\}$, where $C$ is the constant polynomial embedding and $\text{coeff}(f, i)$ denotes the $i$-th coefficient of $f$.

exists_C_coeff_not_mem theorem

: f ∉ I → ∃ i : ℕ, C (coeff f i) ∉ I

Full source

theorem exists_C_coeff_not_mem : f ∉ I → ∃ i : ℕ, C (coeff f i) ∉ I :=
  Not.imp_symm fun cf => span_le_of_C_coeff_mem (not_exists_not.mp cf) mem_span_C_coeff

Existence of Non-Member Coefficient in Ideal for Non-Member Polynomial

Informal description

For any polynomial $f$ over a ring $R$ and any ideal $I$ of $R[X]$, if $f$ does not belong to $I$, then there exists a natural number $i$ such that the constant polynomial $C(f_i)$ (where $f_i$ is the $i$-th coefficient of $f$) does not belong to $I$.

Polynomial.prime_C_iff theorem

: Prime (C r) ↔ Prime r

Full source

theorem prime_C_iff : PrimePrime (C r) ↔ Prime r :=
  ⟨comap_prime C (evalRingHom (0 : R)) fun _ => eval_C, fun hr => by
    have := hr.1
    rw [← Ideal.span_singleton_prime] at hr ⊢
    · rw [← Set.image_singleton, ← Ideal.map_span]
      apply Ideal.isPrime_map_C_of_isPrime hr
    · intro h; apply (this (C_eq_zero.mp h))
    · assumption⟩

Prime Constant Polynomial iff Constant is Prime

Informal description

For any element $r$ in a commutative ring $R$, the constant polynomial $C(r)$ in the polynomial ring $R[X]$ is prime if and only if $r$ is a prime element in $R$.

MvPolynomial.prime_C_iff theorem

: Prime (C r : MvPolynomial σ R) ↔ Prime r

Full source

theorem prime_C_iff : PrimePrime (C r : MvPolynomial σ R) ↔ Prime r :=
  ⟨comap_prime C constantCoeff (constantCoeff_C _), fun hr =>
    ⟨fun h => hr.1 <| by
        rw [← C_inj, h]
        simp,
      fun h =>
      hr.2.1 <| by
        rw [← constantCoeff_C _ r]
        exact h.map _,
      fun a b hd => by
      obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
      rw [← algebraMap_eq] at hd
      have : algebraMap R _ r ∣ a' * b' := by
        convert killCompl Subtype.coe_injective |>.toRingHom.map_dvd hd <;> simp
      rw [← rename_C ((↑) : s → σ)]
      let f := (rename (R := R) ((↑) : s → σ)).toRingHom
      exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp f.map_dvd f.map_dvd⟩⟩

Prime Constant Polynomial iff Constant is Prime in Multivariate Polynomial Ring

Informal description

Let $R$ be a commutative ring and $\sigma$ an arbitrary type. The constant polynomial $C(r)$ in the multivariate polynomial ring $\text{MvPolynomial}\,\sigma\,R$ is a prime element if and only if the element $r \in R$ is prime.

MvPolynomial.prime_rename_iff theorem

(s : Set σ) {p : MvPolynomial s R} : Prime (rename ((↑) : s → σ) p) ↔ Prime (p : MvPolynomial s R)

Full source

theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
    PrimePrime (rename ((↑) : s → σ) p) ↔ Prime (p : MvPolynomial s R) := by
  classical
    symm
    let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
    have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by
      apply ringHom_ext
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
          AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp,
          AlgEquiv.coe_trans, Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply,
          iterToSum_C_C, renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
          AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp,
          AlgEquiv.coe_trans, Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply,
          iterToSum_C_X, renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr,
          Equiv.Set.sumCompl_apply_inl]
    apply_fun (· p) at this
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_eq_coe,
      AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, Function.comp_apply] at this
    rw [this, MulEquiv.prime_iff, prime_C_iff]

Prime Preservation under Variable Renaming in Multivariate Polynomial Rings

Informal description

Let $R$ be a commutative ring, $\sigma$ a type, and $s \subseteq \sigma$ a subset. For any polynomial $p$ in the multivariate polynomial ring $\text{MvPolynomial}\,s\,R$, the polynomial obtained by renaming the variables in $p$ via the inclusion map $s \hookrightarrow \sigma$ is prime in $\text{MvPolynomial}\,\sigma\,R$ if and only if $p$ is prime in $\text{MvPolynomial}\,s\,R$.

Polynomial.isNoetherianRing theorem

[inst : IsNoetherianRing R] : IsNoetherianRing R[X]

Full source

/-- **Hilbert basis theorem**: a polynomial ring over a Noetherian ring is a Noetherian ring. -/
protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X] :=
  isNoetherianRing_iff.2
    ⟨fun I : Ideal R[X] =>
      let M := inst.wf.min (Set.range I.leadingCoeffNth) ⟨_, ⟨0, rfl⟩⟩
      have hm : M ∈ Set.range I.leadingCoeffNth := WellFounded.min_mem _ _ _
      let ⟨N, HN⟩ := hm
      let ⟨s, hs⟩ := I.is_fg_degreeLE N
      have hm2 : ∀ k, I.leadingCoeffNth k ≤ M := fun k =>
        Or.casesOn (le_or_lt k N) (fun h => HN ▸ I.leadingCoeffNth_mono h) fun h _ hx =>
          Classical.by_contradiction fun hxm =>
            haveI : IsNoetherian R R := inst
            have : ¬M < I.leadingCoeffNth k := by
              refine WellFounded.not_lt_min inst.wf _ _ ?_; exact ⟨k, rfl⟩
            this ⟨HN ▸ I.leadingCoeffNth_mono (le_of_lt h), fun H => hxm (H hx)⟩
      have hs2 : ∀ {x}, x ∈ I.degreeLE N → x ∈ Ideal.span (↑s : Set R[X]) :=
        hs ▸ fun hx =>
          Submodule.span_induction (hx := hx) (fun _ hx => Ideal.subset_span hx) (Ideal.zero_mem _)
            (fun _ _ _ _ => Ideal.add_mem _) fun c f _ hf => f.C_mul' c ▸ Ideal.mul_mem_left _ _ hf
      ⟨s, le_antisymm (Ideal.span_le.2 fun x hx =>
          have : x ∈ I.degreeLE N := hs ▸ Submodule.subset_span hx
          this.2) <| by
        have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl
        rw [this]
        intro p hp
        generalize hn : p.natDegree = k
        induction' k using Nat.strong_induction_on with k ih generalizing p
        rcases le_or_lt k N with h | h
        · subst k
          refine hs2 ⟨Polynomial.mem_degreeLE.2
            (le_trans Polynomial.degree_le_natDegree <| WithBot.coe_le_coe.2 h), hp⟩
        · have hp0 : p ≠ 0 := by
            rintro rfl
            cases hn
            exact Nat.not_lt_zero _ h
          have : (0 : R) ≠ 1 := by
            intro h
            apply hp0
            ext i
            refine (mul_one _).symm.trans ?_
            rw [← h, mul_zero]
            rfl
          haveI : Nontrivial R := ⟨⟨0, 1, this⟩⟩
          have : p.leadingCoeff ∈ I.leadingCoeffNth N := by
            rw [HN]
            exact hm2 k ((I.mem_leadingCoeffNth _ _).2
              ⟨_, hp, hn ▸ Polynomial.degree_le_natDegree, rfl⟩)
          rw [I.mem_leadingCoeffNth] at this
          rcases this with ⟨q, hq, hdq, hlqp⟩
          have hq0 : q ≠ 0 := by
            intro H
            rw [← Polynomial.leadingCoeff_eq_zero] at H
            rw [hlqp, Polynomial.leadingCoeff_eq_zero] at H
            exact hp0 H
          have h1 : p.degree = (q * Polynomial.X ^ (k - q.natDegree)).degree := by
            rw [Polynomial.degree_mul', Polynomial.degree_X_pow]
            · rw [Polynomial.degree_eq_natDegree hp0, Polynomial.degree_eq_natDegree hq0]
              rw [← Nat.cast_add, add_tsub_cancel_of_le, hn]
              · refine le_trans (Polynomial.natDegree_le_of_degree_le hdq) (le_of_lt h)
            rw [Polynomial.leadingCoeff_X_pow, mul_one]
            exact mt Polynomial.leadingCoeff_eq_zero.1 hq0
          have h2 : p.leadingCoeff = (q * Polynomial.X ^ (k - q.natDegree)).leadingCoeff := by
            rw [← hlqp, Polynomial.leadingCoeff_mul_X_pow]
          have := Polynomial.degree_sub_lt h1 hp0 h2
          rw [Polynomial.degree_eq_natDegree hp0] at this
          rw [← sub_add_cancel p (q * Polynomial.X ^ (k - q.natDegree))]
          convert (Ideal.span ↑s).add_mem _ ((Ideal.span (s : Set R[X])).mul_mem_right _ _)
          · by_cases hpq : p - q * Polynomial.X ^ (k - q.natDegree) = 0
            · rw [hpq]
              exact Ideal.zero_mem _
            refine ih _ ?_ (I.sub_mem hp (I.mul_mem_right _ hq)) rfl
            rwa [Polynomial.degree_eq_natDegree hpq, Nat.cast_lt, hn] at this
          exact hs2 ⟨Polynomial.mem_degreeLE.2 hdq, hq⟩⟩⟩

Hilbert's Basis Theorem: $R$ Noetherian implies $R[X]$ Noetherian

Informal description

If $R$ is a Noetherian ring, then the polynomial ring $R[X]$ is also Noetherian.

Polynomial.linearIndependent_powers_iff_aeval theorem

 (f : M →ₗ[R] M) (v : M) : (LinearIndependent R fun n : ℕ => (f ^ n) v) ↔ ∀ p : R[X], aeval f p v = 0 → p = 0

Full source

theorem linearIndependent_powers_iff_aeval (f : M →ₗ[R] M) (v : M) :
    (LinearIndependent R fun n : ℕ => (f ^ n) v) ↔ ∀ p : R[X], aeval f p v = 0 → p = 0 := by
  rw [linearIndependent_iff]
  simp only [Finsupp.linearCombination_apply, aeval_endomorphism, forall_iff_forall_finsupp, Sum,
    support, coeff, ofFinsupp_eq_zero]
  exact Iff.rfl

Linear Independence of Powers of a Linear Map is Equivalent to Non-Vanishing of Polynomial Evaluations

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear map. For any vector $v \in M$, the family of vectors $\{f^n(v)\}_{n \in \mathbb{N}}$ is linearly independent over $R$ if and only if for every polynomial $p \in R[X]$, the condition $p(f)(v) = 0$ implies $p = 0$.

Polynomial.disjoint_ker_aeval_of_isCoprime theorem

 (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) : Disjoint (LinearMap.ker (aeval f p)) (LinearMap.ker (aeval f q))

Full source

theorem disjoint_ker_aeval_of_isCoprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
    Disjoint (LinearMap.ker (aeval f p)) (LinearMap.ker (aeval f q)) := by
  rw [disjoint_iff_inf_le]
  intro v hv
  rcases hpq with ⟨p', q', hpq'⟩
  simpa [LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).1,
    LinearMap.mem_ker.1 (Submodule.mem_inf.1 hv).2] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'.symm

Disjointness of Kernels for Coprime Polynomial Evaluations

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear map. For any two coprime polynomials $p, q \in R[X]$, the kernels of the evaluation maps $\operatorname{aeval}(f, p)$ and $\operatorname{aeval}(f, q)$ are disjoint, i.e., $\ker(\operatorname{aeval}(f, p)) \sqcap \ker(\operatorname{aeval}(f, q)) = \bot$.

Polynomial.sup_aeval_range_eq_top_of_isCoprime theorem

 (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) : LinearMap.range (aeval f p) ⊔ LinearMap.range (aeval f q) = ⊤

Full source

theorem sup_aeval_range_eq_top_of_isCoprime (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
    LinearMap.rangeLinearMap.range (aeval f p) ⊔ LinearMap.range (aeval f q) = ⊤ := by
  rw [eq_top_iff]
  intro v _
  rw [Submodule.mem_sup]
  rcases hpq with ⟨p', q', hpq'⟩
  use aeval f (p * p') v
  use LinearMap.mem_range.2 ⟨aeval f p' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
  use aeval f (q * q') v
  use LinearMap.mem_range.2 ⟨aeval f q' v, by simp only [Module.End.mul_apply, aeval_mul]⟩
  simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add] using
    congr_arg (fun p : R[X] => aeval f p v) hpq'

Supremum of Ranges of Coprime Polynomial Evaluations Covers Entire Module

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear map. For any two coprime polynomials $p, q \in R[X]$, the supremum of the ranges of the evaluation maps $\operatorname{aeval}(f, p)$ and $\operatorname{aeval}(f, q)$ is equal to the entire module $M$, i.e., $\operatorname{range}(\operatorname{aeval}(f, p)) \sqcup \operatorname{range}(\operatorname{aeval}(f, q)) = \top$.

Polynomial.sup_ker_aeval_le_ker_aeval_mul theorem

 {f : M →ₗ[R] M} {p q : R[X]} : LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) ≤ LinearMap.ker (aeval f (p * q))

Full source

theorem sup_ker_aeval_le_ker_aeval_mul {f : M →ₗ[R] M} {p q : R[X]} :
    LinearMap.kerLinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) ≤ LinearMap.ker (aeval f (p * q)) := by
  intro v hv
  rcases Submodule.mem_sup.1 hv with ⟨x, hx, y, hy, hxy⟩
  have h_eval_x : aeval f (p * q) x = 0 := by
    rw [mul_comm, aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hx, LinearMap.map_zero]
  have h_eval_y : aeval f (p * q) y = 0 := by
    rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hy, LinearMap.map_zero]
  rw [LinearMap.mem_ker, ← hxy, LinearMap.map_add, h_eval_x, h_eval_y, add_zero]

Supremum of Kernels of Polynomial Evaluations is Contained in Kernel of Product Evaluation

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear map. For any two polynomials $p, q \in R[X]$, the supremum of the kernels of the evaluation maps $\operatorname{aeval}(f, p)$ and $\operatorname{aeval}(f, q)$ is contained in the kernel of the evaluation map $\operatorname{aeval}(f, p \cdot q)$. In other words, \[ \ker(\operatorname{aeval}(f, p)) \sqcup \ker(\operatorname{aeval}(f, q)) \leq \ker(\operatorname{aeval}(f, p \cdot q)). \]

Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime theorem

 (f : M →ₗ[R] M) {p q : R[X]} (hpq : IsCoprime p q) :
  LinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) = LinearMap.ker (aeval f (p * q))

Full source

theorem sup_ker_aeval_eq_ker_aeval_mul_of_coprime (f : M →ₗ[R] M) {p q : R[X]}
    (hpq : IsCoprime p q) :
    LinearMap.kerLinearMap.ker (aeval f p) ⊔ LinearMap.ker (aeval f q) = LinearMap.ker (aeval f (p * q)) := by
  apply le_antisymm sup_ker_aeval_le_ker_aeval_mul
  intro v hv
  rw [Submodule.mem_sup]
  rcases hpq with ⟨p', q', hpq'⟩
  have h_eval₂_qpp' :=
    calc
      aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v := by
        rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]

  have h_eval₂_pqq' :=
    calc
      aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v := by rw [← mul_assoc, mul_comm]
      _ = 0 := by rw [aeval_mul, Module.End.mul_apply, LinearMap.mem_ker.1 hv, LinearMap.map_zero]

  rw [aeval_mul] at h_eval₂_qpp' h_eval₂_pqq'
  refine
    ⟨aeval f (q * q') v, LinearMap.mem_ker.1 h_eval₂_pqq', aeval f (p * p') v,
      LinearMap.mem_ker.1 h_eval₂_qpp', ?_⟩
  rw [add_comm, mul_comm p p', mul_comm q q']
  simpa only [map_add, map_mul, aeval_one] using congr_arg (fun p : R[X] => aeval f p v) hpq'

Kernel Decomposition for Coprime Polynomial Evaluations: $\ker(p(f)) \sqcup \ker(q(f)) = \ker((p \cdot q)(f))$

Informal description

Let $R$ be a commutative ring, $M$ an $R$-module, and $f \colon M \to M$ an $R$-linear map. For any two coprime polynomials $p, q \in R[X]$, the supremum of the kernels of the evaluation maps $\operatorname{aeval}(f, p)$ and $\operatorname{aeval}(f, q)$ equals the kernel of the evaluation map $\operatorname{aeval}(f, p \cdot q)$. In other words, \[ \ker(\operatorname{aeval}(f, p)) \sqcup \ker(\operatorname{aeval}(f, q)) = \ker(\operatorname{aeval}(f, p \cdot q)). \]

MvPolynomial.aeval_natDegree_le theorem

 {R : Type*} [CommSemiring R] {m n : ℕ} (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m) (f : σ → Polynomial R)
  (hf : ∀ i, (f i).natDegree ≤ n) : (MvPolynomial.aeval f F).natDegree ≤ m * n

Full source

lemma aeval_natDegree_le {R : Type*} [CommSemiring R] {m n : ℕ}
    (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m)
    (f : σ → Polynomial R) (hf : ∀ i, (f i).natDegree ≤ n) :
    (MvPolynomial.aeval f F).natDegree ≤ m * n := by
  rw [MvPolynomial.aeval_def, MvPolynomial.eval₂]
  apply (Polynomial.natDegree_sum_le _ _).trans
  apply Finset.sup_le
  intro d hd
  simp_rw [Function.comp_apply, ← C_eq_algebraMap]
  apply (Polynomial.natDegree_C_mul_le _ _).trans
  apply (Polynomial.natDegree_prod_le _ _).trans
  have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
    rw [← Finset.sum_mul]
    apply mul_le_mul' (.trans _ hF) le_rfl
    rw [MvPolynomial.totalDegree]
    exact Finset.le_sup_of_le hd le_rfl
  apply (Finset.sum_le_sum _).trans this
  rintro i -
  apply Polynomial.natDegree_pow_le.trans
  exact mul_le_mul' le_rfl (hf i)

Degree Bound for Evaluation of Multivariate Polynomials: $\deg(\text{aeval}(F, f)) \leq m \cdot n$

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $F$ a multivariate polynomial in $R[\sigma]$. Suppose $F$ has total degree at most $m$, and let $f : \sigma \to R[X]$ be a function such that for each $i \in \sigma$, the polynomial $f(i)$ has degree at most $n$. Then the degree of the polynomial obtained by evaluating $F$ at $f$ is at most $m \cdot n$.

MvPolynomial.isNoetherianRing_fin_0 theorem

[IsNoetherianRing R] : IsNoetherianRing (MvPolynomial (Fin 0) R)

Full source

theorem isNoetherianRing_fin_0 [IsNoetherianRing R] :
    IsNoetherianRing (MvPolynomial (Fin 0) R) := by
  apply isNoetherianRing_of_ringEquiv R
  symm; apply MvPolynomial.isEmptyRingEquiv R (Fin 0)

Noetherian Property of Multivariate Polynomial Ring over $\mathrm{Fin}\,0$

Informal description

If $R$ is a Noetherian ring, then the multivariate polynomial ring $R[\mathrm{Fin}\,0]$ is also Noetherian.

MvPolynomial.isNoetherianRing_fin theorem

[IsNoetherianRing R] : ∀ {n : ℕ}, IsNoetherianRing (MvPolynomial (Fin n) R)

Full source

theorem isNoetherianRing_fin [IsNoetherianRing R] :
    ∀ {n : ℕ}, IsNoetherianRing (MvPolynomial (Fin n) R)
  | 0 => isNoetherianRing_fin_0
  | n + 1 =>
    @isNoetherianRing_of_ringEquiv (Polynomial (MvPolynomial (Fin n) R)) _ _ _
      (MvPolynomial.finSuccEquiv _ n).toRingEquiv.symm
      (@Polynomial.isNoetherianRing (MvPolynomial (Fin n) R) _ isNoetherianRing_fin)

Hilbert's Basis Theorem for Multivariate Polynomial Rings over Finite Variable Sets

Informal description

If $R$ is a Noetherian ring, then for any natural number $n$, the multivariate polynomial ring $R[X_1, \ldots, X_n]$ is also Noetherian.

MvPolynomial.isNoetherianRing instance

[Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)

Full source

/-- The multivariate polynomial ring in finitely many variables over a noetherian ring
is itself a noetherian ring. -/
instance isNoetherianRing [Finite σ] [IsNoetherianRing R] :
    IsNoetherianRing (MvPolynomial σ R) := by
  cases nonempty_fintype σ
  exact
    @isNoetherianRing_of_ringEquiv (MvPolynomial (Fin (Fintype.card σ)) R) _ _ _
      (renameEquiv R (Fintype.equivFin σ).symm).toRingEquiv isNoetherianRing_fin

Hilbert's Basis Theorem for Multivariate Polynomial Rings over Finite Variable Sets

Informal description

For any finite type $\sigma$ and Noetherian ring $R$, the multivariate polynomial ring $R[X_\sigma]$ is also Noetherian.

MvPolynomial.noZeroDivisors_fin theorem

(R : Type u) [CommSemiring R] [NoZeroDivisors R] : ∀ n : ℕ, NoZeroDivisors (MvPolynomial (Fin n) R)

Full source

/-- Auxiliary 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 `MvPolynomial.noZeroDivisors` for the general case. -/
theorem noZeroDivisors_fin (R : Type u) [CommSemiring R] [NoZeroDivisors R] :
    ∀ n : ℕ, NoZeroDivisors (MvPolynomial (Fin n) R)
  | 0 => (MvPolynomial.isEmptyAlgEquiv R _).injective.noZeroDivisors _ (map_zero _) (map_mul _)
  | n + 1 =>
    haveI := noZeroDivisors_fin R n
    (MvPolynomial.finSuccEquiv R n).injective.noZeroDivisors _ (map_zero _) (map_mul _)

Absence of Zero Divisors in Multivariate Polynomial Rings over Finite Variable Sets

Informal description

For any commutative semiring $R$ with no zero divisors and for any natural number $n$, the ring of multivariate polynomials over $R$ with variables indexed by $\mathrm{Fin}\,n$ has no zero divisors.

MvPolynomial.noZeroDivisors_of_finite theorem

(R : Type u) (σ : Type v) [CommSemiring R] [Finite σ] [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R)

Full source

/-- Auxiliary 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 `MvPolynomial.noZeroDivisors_fin`,
and then used to prove the general case without finiteness hypotheses.
See `MvPolynomial.noZeroDivisors` for the general case. -/
theorem noZeroDivisors_of_finite (R : Type u) (σ : Type v) [CommSemiring R] [Finite σ]
    [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R) := by
  cases nonempty_fintype σ
  haveI := noZeroDivisors_fin R (Fintype.card σ)
  exact (renameEquiv R (Fintype.equivFin σ)).injective.noZeroDivisors _ (map_zero _) (map_mul _)

No Zero Divisors in Multivariate Polynomial Rings over Finite Variable Sets

Informal description

Let $R$ be a commutative semiring with no zero divisors, and let $\sigma$ be a finite type. Then the ring of multivariate polynomials $MvPolynomial\,\sigma\,R$ has no zero divisors.

MvPolynomial.instNoZeroDivisors instance

{R : Type u} [CommSemiring R] [NoZeroDivisors R] {σ : Type v} : NoZeroDivisors (MvPolynomial σ R)

Full source

instance {R : Type u} [CommSemiring R] [NoZeroDivisors R] {σ : Type v} :
    NoZeroDivisors (MvPolynomial σ R) where
  eq_zero_or_eq_zero_of_mul_eq_zero {p q} h := by
    obtain ⟨s, p, q, rfl, rfl⟩ := exists_finset_rename₂ p q
    let _nzd := MvPolynomial.noZeroDivisors_of_finite R s
    have : p * q = 0 := by
      apply rename_injective _ Subtype.val_injective
      simpa using h
    rw [mul_eq_zero] at this
    apply this.imp <;> rintro rfl <;> simp

Multivariate Polynomial Rings Preserve No-Zero-Divisor Property

Informal description

For any commutative semiring $R$ with no zero divisors and any type $\sigma$, the ring of multivariate polynomials $R[\sigma]$ has no zero divisors.

MvPolynomial.isDomain instance

{R : Type u} {σ : Type v} [CommRing R] [IsDomain R] : IsDomain (MvPolynomial σ R)

Full source

/-- The multivariate polynomial ring over an integral domain is an integral domain. -/
instance isDomain {R : Type u} {σ : Type v} [CommRing R] [IsDomain R] :
    IsDomain (MvPolynomial σ R) := by
  apply @NoZeroDivisors.to_isDomain (MvPolynomial σ R) _ ?_ _
  apply AddMonoidAlgebra.nontrivial

Multivariate Polynomial Ring over an Integral Domain is an Integral Domain

Informal description

For any commutative ring $R$ that is an integral domain and any type $\sigma$, the ring of multivariate polynomials $R[\sigma]$ is also an integral domain.

MvPolynomial.map_mvPolynomial_eq_eval₂ theorem

 {S : Type*} [CommSemiring S] [Finite σ] (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R) :
  ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p

Full source

theorem map_mvPolynomial_eq_eval₂ {S : Type*} [CommSemiring S] [Finite σ]
    (ϕ : MvPolynomialMvPolynomial σ R →+* S) (p : MvPolynomial σ R) :
    ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p := by
  cases nonempty_fintype σ
  refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_
  rw [MvPolynomial.eval₂_eq', map_sum ϕ]
  congr
  ext
  simp only [monomial_eq, ϕ.map_pow, map_prod ϕ, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]

Evaluation of Polynomial Homomorphism via Composition and Variable Substitution

Informal description

Let $R$ be a commutative semiring, $S$ be a commutative semiring, and $\sigma$ be a finite type. For any ring homomorphism $\phi \colon R[\sigma] \to S$ and any multivariate polynomial $p \in R[\sigma]$, the evaluation of $\phi$ at $p$ equals the evaluation of $p$ under the homomorphism obtained by composing $\phi$ with the constant polynomial embedding $C \colon R \to R[\sigma]$ and evaluating the variables $X_s$ at $\phi(X_s)$ for each $s \in \sigma$. In other words, $\phi(p) = \text{eval}_2 (\phi \circ C) (\lambda s, \phi(X_s)) p$.

MvPolynomial.mem_ideal_of_coeff_mem_ideal theorem

 (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R)
  (hcoe : ∀ m : σ →₀ ℕ, p.coeff m ∈ I.comap (C : R →+* MvPolynomial σ R)) : p ∈ I

Full source

/-- If every coefficient of a polynomial is in an ideal `I`, then so is the polynomial itself,
multivariate version. -/
theorem mem_ideal_of_coeff_mem_ideal (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R)
    (hcoe : ∀ m : σ →₀ ℕ, p.coeff m ∈ I.comap (C : R →+* MvPolynomial σ R)) : p ∈ I := by
  rw [as_sum p]
  suffices ∀ m ∈ p.support, monomial m (MvPolynomial.coeff m p) ∈ I by
    exact Submodule.sum_mem I this
  intro m _
  rw [← mul_one (coeff m p), ← C_mul_monomial]
  suffices CC (coeff m p) ∈ I by exact I.mul_mem_right (monomial m 1) this
  simpa [Ideal.mem_comap] using hcoe m

Polynomial Membership via Coefficient Membership in Multivariate Polynomial Ring

Informal description

Let $R$ be a commutative ring, $\sigma$ a type, and $I$ an ideal of the multivariate polynomial ring $R[\sigma]$. For any polynomial $p \in R[\sigma]$, if every coefficient of $p$ (when viewed as an element of $R$ via the canonical embedding $C \colon R \to R[\sigma]$) belongs to the preimage of $I$ under $C$, then $p$ itself belongs to $I$. In other words, if for every monomial $m$ in $\sigma \to₀ ℕ$, the coefficient $p_m$ satisfies $C(p_m) \in I$, then $p \in I$.

MvPolynomial.mem_map_C_iff theorem

 {I : Ideal R} {f : MvPolynomial σ R} :
  f ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R)) ↔ ∀ m : σ →₀ ℕ, f.coeff m ∈ I

Full source

/-- The push-forward of an ideal `I` of `R` to `MvPolynomial σ R` via inclusion
 is exactly the set of polynomials whose coefficients are in `I` -/
theorem mem_map_C_iff {I : Ideal R} {f : MvPolynomial σ R} :
    f ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R))f ∈ (Ideal.map (C : R →+* MvPolynomial σ R) I : Ideal (MvPolynomial σ R)) ↔
      ∀ m : σ →₀ ℕ, f.coeff m ∈ I := by
  classical
  constructor
  · intro hf
    refine Submodule.span_induction ?_ ?_ ?_ ?_ hf
    · intro f hf n
      obtain ⟨x, hx⟩ := (Set.mem_image _ _ _).mp hf
      rw [← hx.right, coeff_C]
      by_cases h : n = 0
      · simpa [h] using hx.left
      · simp [Ne.symm h]
    · simp
    · exact fun f g _ _ hf hg n => by simp [I.add_mem (hf n) (hg n)]
    · refine fun f g _ hg n => ?_
      rw [smul_eq_mul, coeff_mul]
      exact I.sum_mem fun c _ => I.mul_mem_left (f.coeff c.fst) (hg c.snd)
  · intro hf
    rw [as_sum f]
    suffices ∀ m ∈ f.support, monomial m (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Submodule.sum_mem _ this
    intro m _
    rw [← mul_one (coeff m f), ← C_mul_monomial]
    suffices CC (coeff m f) ∈ (Ideal.map C I : Ideal (MvPolynomial σ R)) by
      exact Ideal.mul_mem_right _ _ this
    apply Ideal.mem_map_of_mem _
    exact hf m

Characterization of Polynomials in the Pushforward Ideal via Coefficients

Informal description

Let $R$ be a commutative ring, $\sigma$ a type, and $I$ an ideal of $R$. For any multivariate polynomial $f \in R[\sigma]$, the polynomial $f$ belongs to the ideal generated by the image of $I$ under the canonical embedding $C \colon R \to R[\sigma]$ if and only if every coefficient of $f$ (with respect to the monomial basis) belongs to $I$.

MvPolynomial.ker_map theorem

 (f : R →+* S) :
  RingHom.ker (map f : MvPolynomial σ R →+* MvPolynomial σ S) = Ideal.map (C : R →+* MvPolynomial σ R) (RingHom.ker f)

Full source

theorem ker_map (f : R →+* S) :
    RingHom.ker (map f : MvPolynomialMvPolynomial σ R →+* MvPolynomial σ S) =
    Ideal.map (C : R →+* MvPolynomial σ R) (RingHom.ker f) := by
  ext
  rw [MvPolynomial.mem_map_C_iff, RingHom.mem_ker, MvPolynomial.ext_iff]
  simp_rw [coeff_map, coeff_zero, RingHom.mem_ker]

Kernel of Polynomial Extension Equals Extension of Kernel

Informal description

Let $R$ and $S$ be commutative rings, $\sigma$ a type, and $f \colon R \to S$ a ring homomorphism. The kernel of the induced homomorphism $\text{map}\, f \colon R[\sigma] \to S[\sigma]$ on multivariate polynomial rings is equal to the ideal generated by the image of $\ker f$ under the canonical embedding $C \colon R \to R[\sigma]$. In other words, $\ker(\text{map}\, f) = \langle C(\ker f) \rangle$ in $R[\sigma]$.

MvPolynomial.ker_mapAlgHom theorem

 {S₁ S₂ σ : Type*} [CommRing S₁] [CommRing S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
  RingHom.ker (MvPolynomial.mapAlgHom (σ := σ) f) = Ideal.map MvPolynomial.C (RingHom.ker f)

Full source

lemma ker_mapAlgHom {S₁ S₂ σ : Type*} [CommRing S₁] [CommRing S₂] [Algebra R S₁]
    [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    RingHom.ker (MvPolynomial.mapAlgHom (σ := σ) f) = Ideal.map MvPolynomial.C (RingHom.ker f) :=
  MvPolynomial.ker_map (f.toRingHom : S₁ →+* S₂)

Kernel of Algebra Homomorphism Extension Equals Extension of Kernel for Multivariate Polynomials

Informal description

Let $R$, $S_1$, and $S_2$ be commutative rings with $S_1$ and $S_2$ being $R$-algebras, and let $\sigma$ be a type. For any $R$-algebra homomorphism $f \colon S_1 \to S_2$, the kernel of the induced homomorphism $\text{mapAlgHom}\, f \colon S_1[\sigma] \to S_2[\sigma]$ on multivariate polynomial rings is equal to the ideal generated by the image of $\ker f$ under the canonical embedding $C \colon S_1 \to S_1[\sigma]$. In other words, $\ker(\text{mapAlgHom}\, f) = \langle C(\ker f) \rangle$ in $S_1[\sigma]$.

Main results