Mathlib.RingTheory.Polynomial.IntegralNormalization

Polynomial.integralNormalization definition

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

Full source

/-- If `p : R[X]` is a nonzero polynomial with root `z`, `integralNormalization p` is
a monic polynomial with root `leadingCoeff f * z`.

Moreover, `integralNormalization 0 = 0`.
-/
noncomputable def integralNormalization (p : R[X]) : R[X] :=
  p.sum fun i a ↦
    monomial i (if p.degree = i then 1 else a * p.leadingCoeff ^ (p.natDegree - 1 - i))

Integral normalization of a polynomial

Informal description

For a nonzero polynomial $ p \in R[X] $ with a root $ z $, the polynomial $ \text{integralNormalization}(p) $ is a monic polynomial with root $ \text{leadingCoeff}(p) \cdot z $. If $ p = 0 $, then $ \text{integralNormalization}(p) = 0 $. More precisely, for a polynomial $ p = \sum_{i} a_i X^i $, the integral normalization is defined as: \[ \text{integralNormalization}(p) = \sum_{i} \begin{cases} X^i & \text{if } i = \deg(p) \\ a_i \cdot (\text{leadingCoeff}(p))^{\deg(p) - 1 - i} X^i & \text{otherwise} \end{cases} \]

Polynomial.integralNormalization_zero theorem

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

Full source

@[simp]
theorem integralNormalization_zero : integralNormalization (0 : R[X]) = 0 := by
  simp [integralNormalization]

Integral Normalization of Zero Polynomial is Zero

Informal description

The integral normalization of the zero polynomial is zero, i.e., $\text{integralNormalization}(0) = 0$.

Polynomial.integralNormalization_C theorem

{x : R} (hx : x ≠ 0) : integralNormalization (C x) = 1

Full source

@[simp]
theorem integralNormalization_C {x : R} (hx : x ≠ 0) : integralNormalization (C x) = 1 := by
  simp [integralNormalization, sum_def, support_C hx, degree_C hx]

Integral Normalization of Nonzero Constant Polynomial is One

Informal description

For any nonzero element $x$ in a ring $R$, the integral normalization of the constant polynomial $C(x)$ is the monic polynomial $1$.

Polynomial.integralNormalization_coeff theorem

 {i : ℕ} :
  (integralNormalization p).coeff i = if p.degree = i then 1 else coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Full source

theorem integralNormalization_coeff {i : ℕ} :
    (integralNormalization p).coeff i =
      if p.degree = i then 1 else coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) := by
  have : p.coeff i = 0 → p.degree ≠ i := fun hc hd => coeff_ne_zero_of_eq_degree hd hc
  simp +contextual [sum_def, integralNormalization, coeff_monomial, this,
    mem_support_iff]

Coefficient Formula for Integral Normalization of Polynomials

Informal description

For any polynomial $p \in R[X]$ and any natural number $i$, the coefficient of $X^i$ in the integral normalization of $p$ is given by: \[ (\text{integralNormalization}(p))_i = \begin{cases} 1 & \text{if } \deg(p) = i, \\ p_i \cdot (\text{leadingCoeff}(p))^{\deg(p) - 1 - i} & \text{otherwise.} \end{cases} \]

Polynomial.support_integralNormalization_subset theorem

: (integralNormalization p).support ⊆ p.support

Full source

theorem support_integralNormalization_subset :
    (integralNormalization p).support ⊆ p.support := by
  intro
  simp +contextual [sum_def, integralNormalization, coeff_monomial, mem_support_iff]

Support of Integral Normalization is Subset of Original Polynomial's Support

Informal description

For any polynomial $p \in R[X]$, the support of its integral normalization $\text{integralNormalization}(p)$ is a subset of the support of $p$. In other words, if a monomial $X^i$ appears in $\text{integralNormalization}(p)$, then it must also appear in $p$.

Polynomial.integralNormalization_coeff_degree theorem

{i : ℕ} (hi : p.degree = i) : (integralNormalization p).coeff i = 1

Full source

theorem integralNormalization_coeff_degree {i : ℕ} (hi : p.degree = i) :
    (integralNormalization p).coeff i = 1 := by rw [integralNormalization_coeff, if_pos hi]

Leading Coefficient of Integral Normalization is One

Informal description

For any polynomial $p \in R[X]$ and any natural number $i$ such that the degree of $p$ is equal to $i$, the coefficient of $X^i$ in the integral normalization of $p$ is equal to $1$, i.e., \[ (\text{integralNormalization}(p))_i = 1. \]

Polynomial.integralNormalization_coeff_natDegree theorem

(hp : p ≠ 0) : (integralNormalization p).coeff (natDegree p) = 1

Full source

theorem integralNormalization_coeff_natDegree (hp : p ≠ 0) :
    (integralNormalization p).coeff (natDegree p) = 1 :=
  integralNormalization_coeff_degree (degree_eq_natDegree hp)

Leading coefficient of integral normalization is one for nonzero polynomials

Informal description

For any nonzero polynomial $p \in R[X]$, the coefficient of $X^{\deg(p)}$ in the integral normalization of $p$ is equal to $1$, i.e., \[ (\text{integralNormalization}(p))_{\deg(p)} = 1. \]

Polynomial.integralNormalization_coeff_degree_ne theorem

 {i : ℕ} (hi : p.degree ≠ i) : coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Full source

theorem integralNormalization_coeff_degree_ne {i : ℕ} (hi : p.degree ≠ i) :
    coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) := by
  rw [integralNormalization_coeff, if_neg hi]

Coefficient Formula for Integral Normalization at Non-Degree Index

Informal description

For any polynomial $p \in R[X]$ and any natural number $i$ such that $\deg(p) \neq i$, the coefficient of $X^i$ in the integral normalization of $p$ is given by: \[ (\text{integralNormalization}(p))_i = p_i \cdot (\text{leadingCoeff}(p))^{\deg(p) - 1 - i}. \]

Polynomial.integralNormalization_coeff_ne_natDegree theorem

 {i : ℕ} (hi : i ≠ natDegree p) : coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i)

Full source

theorem integralNormalization_coeff_ne_natDegree {i : ℕ} (hi : i ≠ natDegree p) :
    coeff (integralNormalization p) i = coeff p i * p.leadingCoeff ^ (p.natDegree - 1 - i) :=
  integralNormalization_coeff_degree_ne (degree_ne_of_natDegree_ne hi.symm)

Coefficient Formula for Integral Normalization at Non-Degree Index

Informal description

For any polynomial $p \in R[X]$ and any natural number $i$ such that $i \neq \deg(p)$, the coefficient of $X^i$ in the integral normalization of $p$ is given by: \[ (\text{integralNormalization}(p))_i = p_i \cdot (\text{leadingCoeff}(p))^{\deg(p) - 1 - i}. \]

Polynomial.monic_integralNormalization theorem

(hp : p ≠ 0) : Monic (integralNormalization p)

Full source

theorem monic_integralNormalization (hp : p ≠ 0) : Monic (integralNormalization p) :=
  monic_of_degree_le p.natDegree
    (Finset.sup_le fun i h =>
      WithBot.coe_le_coe.2 <| le_natDegree_of_mem_supp i <| support_integralNormalization_subset h)
    (integralNormalization_coeff_natDegree hp)

Integral Normalization of a Nonzero Polynomial is Monic

Informal description

For any nonzero polynomial $p \in R[X]$, its integral normalization $\text{integralNormalization}(p)$ is monic, meaning the leading coefficient of $\text{integralNormalization}(p)$ is equal to $1$.

Polynomial.integralNormalization_coeff_mul_leadingCoeff_pow theorem

 (i : ℕ) (hp : 1 ≤ natDegree p) :
  (integralNormalization p).coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Full source

theorem integralNormalization_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ natDegree p) :
    (integralNormalization p).coeff i * p.leadingCoeff ^ i =
      p.coeff i * p.leadingCoeff ^ (p.natDegree - 1) := by
  rw [integralNormalization_coeff]
  split_ifs with h
  · simp [natDegree_eq_of_degree_eq_some h, leadingCoeff,
      ← pow_succ', tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]
  · simp only [mul_assoc, ← pow_add]
    by_cases h' : i < p.degree
    · rw [tsub_add_cancel_of_le]
      rw [le_tsub_iff_right hp, Nat.succ_le_iff]
      exact coe_lt_degree.mp h'
    · simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Coefficient relation in integral normalization: $(\text{integralNormalization}(p))_i \cdot a^i = p_i \cdot a^{d-1}$ where $a$ is the leading coefficient and $d$ is the degree of $p$

Informal description

For any polynomial $p \in R[X]$ with $\deg(p) \geq 1$ and any natural number $i$, the coefficient of $X^i$ in the integral normalization of $p$ multiplied by $(\text{leadingCoeff}(p))^i$ equals the coefficient of $X^i$ in $p$ multiplied by $(\text{leadingCoeff}(p))^{\deg(p)-1}$. In other words: \[ (\text{integralNormalization}(p))_i \cdot (\text{leadingCoeff}(p))^i = p_i \cdot (\text{leadingCoeff}(p))^{\deg(p)-1} \]

Polynomial.integralNormalization_mul_C_leadingCoeff theorem

(p : R[X]) : integralNormalization p * C p.leadingCoeff = scaleRoots p p.leadingCoeff

Full source

theorem integralNormalization_mul_C_leadingCoeff (p : R[X]) :
    integralNormalization p * C p.leadingCoeff = scaleRoots p p.leadingCoeff := by
  ext i
  rw [coeff_mul_C, integralNormalization_coeff]
  split_ifs with h
  · simp [natDegree_eq_of_degree_eq_some h, leadingCoeff]
  · simp only [ge_iff_le, tsub_le_iff_right, smul_eq_mul, coeff_scaleRoots]
    by_cases h' : i < p.degree
    · rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]
      rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]
      exact coe_lt_degree.mp h'
    · simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Relation Between Integral Normalization and Scaled Roots of a Polynomial

Informal description

For any polynomial $p \in R[X]$, the product of its integral normalization $\text{integralNormalization}(p)$ and the constant polynomial $C(\text{leadingCoeff}(p))$ equals the scaled roots polynomial $\text{scaleRoots}(p, \text{leadingCoeff}(p))$. In other words, \[ \text{integralNormalization}(p) \cdot C(\text{leadingCoeff}(p)) = \text{scaleRoots}(p, \text{leadingCoeff}(p)). \]

Polynomial.integralNormalization_degree theorem

: (integralNormalization p).degree = p.degree

Full source

theorem integralNormalization_degree : (integralNormalization p).degree = p.degree := by
  apply le_antisymm
  · exact Finset.sup_mono p.support_integralNormalization_subset
  · rw [← degree_scaleRoots, ← integralNormalization_mul_C_leadingCoeff]
    exact (degree_mul_le _ _).trans (add_le_of_nonpos_right degree_C_le)

Degree Preservation under Integral Normalization: $\deg(\text{integralNormalization}(p)) = \deg(p)$

Informal description

For any polynomial $p$, the degree of its integral normalization $\text{integralNormalization}(p)$ is equal to the degree of $p$, i.e., \[ \deg(\text{integralNormalization}(p)) = \deg(p). \]

Polynomial.leadingCoeff_smul_integralNormalization theorem

(p : S[X]) : p.leadingCoeff • integralNormalization p = scaleRoots p p.leadingCoeff

Full source

theorem leadingCoeff_smul_integralNormalization (p : S[X]) :
    p.leadingCoeff • integralNormalization p = scaleRoots p p.leadingCoeff := by
  rw [Algebra.smul_def, algebraMap_eq, mul_comm, integralNormalization_mul_C_leadingCoeff]

Scalar Multiple of Integral Normalization Equals Scaled Roots Polynomial

Informal description

For any polynomial $p \in S[X]$, the scalar multiple of the leading coefficient of $p$ and its integral normalization equals the scaled roots polynomial with scaling factor given by the leading coefficient. That is, \[ \text{leadingCoeff}(p) \cdot \text{integralNormalization}(p) = \text{scaleRoots}(p, \text{leadingCoeff}(p)). \]

Polynomial.integralNormalization_eval₂_leadingCoeff_mul_of_commute theorem

 (h : 1 ≤ p.natDegree) (f : R →+* A) (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r'}, Commute (f r) (f r')) :
  (integralNormalization p).eval₂ f (f p.leadingCoeff * x) = f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x

Full source

theorem integralNormalization_eval₂_leadingCoeff_mul_of_commute (h : 1 ≤ p.natDegree) (f : R →+* A)
    (x : A) (h₁ : Commute (f p.leadingCoeff) x) (h₂ : ∀ {r r'}, Commute (f r) (f r')) :
    (integralNormalization p).eval₂ f (f p.leadingCoeff * x) =
      f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x := by
  rw [eval₂_eq_sum_range, eval₂_eq_sum_range, Finset.mul_sum]
  apply Finset.sum_congr
  · rw [natDegree_eq_of_degree_eq p.integralNormalization_degree]
  intro n _hn
  rw [h₁.mul_pow, ← mul_assoc, ← f.map_pow, ← f.map_mul,
    integralNormalization_coeff_mul_leadingCoeff_pow _ h, f.map_mul, h₂.eq, f.map_pow, mul_assoc]

Evaluation of Integral Normalization at Scaled Point: $\text{eval}_2(f, a x)(\tilde{p}) = a^{d-1} \text{eval}_2(f, x)(p)$ where $a$ is the leading coefficient and $d$ is the degree of $p$

Informal description

Let $p \in R[X]$ be a polynomial with $\deg(p) \geq 1$, and let $f: R \to A$ be a ring homomorphism. For any element $x \in A$ such that $f(\text{leadingCoeff}(p))$ commutes with $x$, and for any $r, r' \in R$, $f(r)$ commutes with $f(r')$, we have: \[ \text{eval}_2(f, f(\text{leadingCoeff}(p)) \cdot x)(\text{integralNormalization}(p)) = f(\text{leadingCoeff}(p))^{\deg(p)-1} \cdot \text{eval}_2(f, x)(p) \] where $\text{eval}_2(f, y)(q)$ denotes the evaluation of polynomial $q$ at $y$ via the homomorphism $f$.

Polynomial.integralNormalization_eval₂_leadingCoeff_mul theorem

 (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :
  (integralNormalization p).eval₂ f (f p.leadingCoeff * x) = f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x

Full source

theorem integralNormalization_eval₂_leadingCoeff_mul (h : 1 ≤ p.natDegree) (f : R →+* S) (x : S) :
    (integralNormalization p).eval₂ f (f p.leadingCoeff * x) =
      f p.leadingCoeff ^ (p.natDegree - 1) * p.eval₂ f x :=
  integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ (.all _ _) (.all _ _)

Evaluation of Integral Normalization at Scaled Point: $\text{eval}_2(f, a x)(\tilde{p}) = a^{d-1} \text{eval}_2(f, x)(p)$ for $a = \text{leadingCoeff}(p)$ and $d = \deg(p)$

Informal description

Let $p \in R[X]$ be a polynomial with $\deg(p) \geq 1$, and let $f: R \to S$ be a ring homomorphism. For any element $x \in S$, the evaluation of the integral normalization of $p$ at $f(\text{leadingCoeff}(p)) \cdot x$ via $f$ satisfies: \[ \text{eval}_2(f, f(\text{leadingCoeff}(p)) \cdot x)(\text{integralNormalization}(p)) = f(\text{leadingCoeff}(p))^{\deg(p)-1} \cdot \text{eval}_2(f, x)(p), \] where $\text{eval}_2(f, y)(q)$ denotes the evaluation of polynomial $q$ at $y$ via the homomorphism $f$.

Polynomial.integralNormalization_eval₂_eq_zero_of_commute theorem

 {p : R[X]} (f : R →+* A) {z : A} (hz : eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z)
  (h₂ : ∀ {r r'}, Commute (f r) (f r')) (inj : ∀ x : R, f x = 0 → x = 0) :
  eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0

Full source

theorem integralNormalization_eval₂_eq_zero_of_commute {p : R[X]} (f : R →+* A) {z : A}
    (hz : eval₂ f z p = 0) (h₁ : Commute (f p.leadingCoeff) z) (h₂ : ∀ {r r'}, Commute (f r) (f r'))
    (inj : ∀ x : R, f x = 0 → x = 0) :
    eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 := by
  obtain (h | h) := p.natDegree.eq_zero_or_pos
  · by_cases h0 : coeff p 0 = 0
    · rw [eq_C_of_natDegree_eq_zero h]
      simp [h0]
    · rw [eq_C_of_natDegree_eq_zero h, eval₂_C] at hz
      exact absurd (inj _ hz) h0
  · rw [integralNormalization_eval₂_leadingCoeff_mul_of_commute h _ _ h₁ h₂, hz, mul_zero]

Vanishing of Integral Normalization at Scaled Root with Commutativity Conditions

Informal description

Let $p \in R[X]$ be a polynomial, $f: R \to A$ a ring homomorphism, and $z \in A$ such that: 1. $p$ evaluates to zero at $z$ via $f$ (i.e., $\text{eval}_2(f, z)(p) = 0$), 2. $f(\text{leadingCoeff}(p))$ commutes with $z$, 3. For any $r, r' \in R$, $f(r)$ commutes with $f(r')$, 4. $f$ is injective (i.e., $f(x) = 0$ implies $x = 0$ for all $x \in R$). Then the integral normalization of $p$ evaluates to zero at $f(\text{leadingCoeff}(p)) \cdot z$ via $f$, i.e., \[ \text{eval}_2(f, f(\text{leadingCoeff}(p)) \cdot z)(\text{integralNormalization}(p)) = 0. \]

Polynomial.integralNormalization_eval₂_eq_zero theorem

 {p : R[X]} (f : R →+* S) {z : S} (hz : eval₂ f z p = 0) (inj : ∀ x : R, f x = 0 → x = 0) :
  eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0

Full source

theorem integralNormalization_eval₂_eq_zero {p : R[X]} (f : R →+* S) {z : S} (hz : eval₂ f z p = 0)
    (inj : ∀ x : R, f x = 0 → x = 0) :
    eval₂ f (f p.leadingCoeff * z) (integralNormalization p) = 0 :=
  integralNormalization_eval₂_eq_zero_of_commute _ hz (.all _ _) (.all _ _) inj

Vanishing of Integral Normalization at Scaled Root under Injective Homomorphism

Informal description

Let $p \in R[X]$ be a polynomial, $f: R \to S$ a ring homomorphism, and $z \in S$ such that: 1. $p$ evaluates to zero at $z$ via $f$ (i.e., $\text{eval}_2(f, z)(p) = 0$), 2. $f$ is injective (i.e., $f(x) = 0$ implies $x = 0$ for all $x \in R$). Then the integral normalization of $p$ evaluates to zero at $f(\text{leadingCoeff}(p)) \cdot z$ via $f$, i.e., \[ \text{eval}_2(f, f(\text{leadingCoeff}(p)) \cdot z)(\text{integralNormalization}(p)) = 0. \]

Polynomial.integralNormalization_aeval_eq_zero theorem

 [Algebra S A] {f : S[X]} {z : A} (hz : aeval z f = 0) (inj : ∀ x : S, algebraMap S A x = 0 → x = 0) :
  aeval (algebraMap S A f.leadingCoeff * z) (integralNormalization f) = 0

Full source

theorem integralNormalization_aeval_eq_zero [Algebra S A] {f : S[X]} {z : A} (hz : aeval z f = 0)
    (inj : ∀ x : S, algebraMap S A x = 0 → x = 0) :
    aeval (algebraMap S A f.leadingCoeff * z) (integralNormalization f) = 0 :=
  integralNormalization_eval₂_eq_zero_of_commute (algebraMap S A) hz
    (Algebra.commute_algebraMap_left _ _) (.map (.all _ _) _) inj

Vanishing of Integral Normalization under Algebra Evaluation

Informal description

Let $S$ be a commutative ring, $A$ an $S$-algebra, and $f \in S[X]$ a polynomial. For any $z \in A$ such that: 1. The evaluation of $f$ at $z$ via the algebra map is zero (i.e., $\text{aeval}(z)(f) = 0$), 2. The algebra map $\text{algebraMap}_{S \to A}$ is injective (i.e., $\text{algebraMap}(x) = 0$ implies $x = 0$ for all $x \in S$), then the integral normalization of $f$ evaluates to zero at $\text{algebraMap}(\text{leadingCoeff}(f)) \cdot z$ via the algebra map, i.e., \[ \text{aeval}(\text{algebraMap}(\text{leadingCoeff}(f)) \cdot z)(\text{integralNormalization}(f)) = 0. \]

Polynomial.support_integralNormalization theorem

{f : R[X]} : (integralNormalization f).support = f.support

Full source

@[simp]
theorem support_integralNormalization {f : R[X]} :
    (integralNormalization f).support = f.support := by
  nontriviality R using Subsingleton.eq_zero
  have : IsDomain R := {}
  by_cases hf : f = 0; · simp [hf]
  ext i
  refine ⟨fun h => support_integralNormalization_subset h, ?_⟩
  simp only [integralNormalization_coeff, mem_support_iff]
  intro hfi
  split_ifs with hi <;> simp [hf, hfi, hi]

Support Preservation under Integral Normalization of Polynomials

Informal description

For any polynomial $f \in R[X]$, the support of its integral normalization $\text{integralNormalization}(f)$ is equal to the support of $f$. That is, the set of exponents of monomials with nonzero coefficients is preserved under integral normalization.