Mathlib.FieldTheory.Minpoly.Basic

minpoly definition

(x : B) : A[X]

Full source

/-- Suppose `x : B`, where `B` is an `A`-algebra.

The minimal polynomial `minpoly A x` of `x`
is a monic polynomial with coefficients in `A` of smallest degree that has `x` as its root,
if such exists (`IsIntegral A x`) or zero otherwise.

For example, if `V` is a `𝕜`-vector space for some field `𝕜` and `f : V →ₗ[𝕜] V` then
the minimal polynomial of `f` is `minpoly 𝕜 f`.
-/
@[stacks 09GM]
noncomputable def minpoly (x : B) : A[X] :=
  if hx : IsIntegral A x then degree_lt_wf.min _ hx else 0

Minimal polynomial of an integral element

Informal description

Given an element $ x $ in an $ A $-algebra $ B $, the minimal polynomial $\text{minpoly}_A(x)$ is defined as the monic polynomial of minimal degree in $ A[X] $ that has $ x $ as a root, provided $ x $ is integral over $ A $. If $ x $ is not integral over $ A $, the minimal polynomial is defined to be zero.

minpoly.monic theorem

(hx : IsIntegral A x) : Monic (minpoly A x)

Full source

/-- A minimal polynomial is monic. -/
theorem monic (hx : IsIntegral A x) : Monic (minpoly A x) := by
  delta minpoly
  rw [dif_pos hx]
  exact (degree_lt_wf.min_mem _ hx).1

Monicity of the Minimal Polynomial of an Integral Element

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, the minimal polynomial $\text{minpoly}_A(x)$ is monic.

minpoly.ne_zero theorem

[Nontrivial A] (hx : IsIntegral A x) : minpoly A x ≠ 0

Full source

/-- A minimal polynomial is nonzero. -/
theorem ne_zero [Nontrivial A] (hx : IsIntegral A x) : minpolyminpoly A x ≠ 0 :=
  (monic hx).ne_zero

Nonvanishing of Minimal Polynomial for Integral Elements

Informal description

Let $A$ be a nontrivial commutative ring and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, the minimal polynomial $\text{minpoly}_A(x)$ is nonzero.

minpoly.ne_zero_iff theorem

[Nontrivial A] : minpoly A x ≠ 0 ↔ IsIntegral A x

Full source

theorem ne_zero_iff [Nontrivial A] : minpolyminpoly A x ≠ 0minpoly A x ≠ 0 ↔ IsIntegral A x :=
  ⟨fun h => of_not_not <| eq_zero.mt h, ne_zero⟩

Nonvanishing of Minimal Polynomial Characterizes Integral Elements

Informal description

Let $A$ be a nontrivial commutative ring and $B$ an $A$-algebra. For an element $x \in B$, the minimal polynomial $\text{minpoly}_A(x)$ is nonzero if and only if $x$ is integral over $A$.

minpoly.algHom_eq theorem

(f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) : minpoly A (f x) = minpoly A x

Full source

theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
    minpoly A (f x) = minpoly A x := by
  classical
  simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
    AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

Invariance of Minimal Polynomial under Injective Algebra Homomorphism

Informal description

Let $A$ be a commutative ring and $B$, $B'$ be $A$-algebras. Given an injective $A$-algebra homomorphism $f \colon B \to B'$ and an element $x \in B$, the minimal polynomial of $f(x)$ over $A$ is equal to the minimal polynomial of $x$ over $A$. In other words, $\text{minpoly}_A(f(x)) = \text{minpoly}_A(x)$.

minpoly.algebraMap_eq theorem

 {B} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B'] (h : Function.Injective (algebraMap B B'))
  (x : B) : minpoly A (algebraMap B B' x) = minpoly A x

Full source

theorem algebraMap_eq {B} [CommRing B] [Algebra A B] [Algebra B B'] [IsScalarTower A B B']
    (h : Function.Injective (algebraMap B B')) (x : B) :
    minpoly A (algebraMap B B' x) = minpoly A x :=
  algHom_eq (IsScalarTower.toAlgHom A B B') h x

Invariance of Minimal Polynomial under Injective Algebra Map in Tower of Algebras

Informal description

Let $A$ be a commutative ring, and let $B$ and $B'$ be $A$-algebras such that $B$ is a commutative ring and there is a tower of algebra structures $A \to B \to B'$. If the algebra map $\phi \colon B \to B'$ is injective, then for any element $x \in B$, the minimal polynomial of $\phi(x)$ over $A$ is equal to the minimal polynomial of $x$ over $A$, i.e., $\text{minpoly}_A(\phi(x)) = \text{minpoly}_A(x)$.

minpoly.algEquiv_eq theorem

(f : B ≃ₐ[A] B') (x : B) : minpoly A (f x) = minpoly A x

Full source

@[simp]
theorem algEquiv_eq (f : B ≃ₐ[A] B') (x : B) : minpoly A (f x) = minpoly A x :=
  algHom_eq (f : B →ₐ[A] B') f.injective x

Invariance of Minimal Polynomial under Algebra Isomorphism

Informal description

Let $A$ be a commutative ring and $B$, $B'$ be $A$-algebras. Given an $A$-algebra isomorphism $f \colon B \to B'$ and an element $x \in B$, the minimal polynomial of $f(x)$ over $A$ is equal to the minimal polynomial of $x$ over $A$, i.e., $\text{minpoly}_A(f(x)) = \text{minpoly}_A(x)$.

minpoly.aeval theorem

: aeval x (minpoly A x) = 0

Full source

/-- An element is a root of its minimal polynomial. -/
@[simp]
theorem aeval : aeval x (minpoly A x) = 0 := by
  delta minpoly
  split_ifs with hx
  · exact (degree_lt_wf.min_mem _ hx).2
  · exact aeval_zero _

Root Property of Minimal Polynomial

Informal description

Let $B$ be an $A$-algebra and $x \in B$ be an integral element over $A$. Then $x$ is a root of its minimal polynomial $\text{minpoly}_A(x)$, i.e., the evaluation of $\text{minpoly}_A(x)$ at $x$ is zero.

minpoly.aeval_algHom theorem

(f : B →ₐ[A] B') (x : B) : (Polynomial.aeval (f x)) (minpoly A x) = 0

Full source

/-- Given any `f : B →ₐ[A] B'` and any `x : L`, the minimal polynomial of `x` vanishes at `f x`. -/
@[simp]
theorem aeval_algHom (f : B →ₐ[A] B') (x : B) : (Polynomial.aeval (f x)) (minpoly A x) = 0 := by
  rw [Polynomial.aeval_algHom, AlgHom.coe_comp, comp_apply, aeval, map_zero]

Minimal Polynomial Vanishes Under Algebra Homomorphism

Informal description

Let $B$ and $B'$ be $A$-algebras, $x \in B$ be an element integral over $A$, and $f : B \to B'$ be an $A$-algebra homomorphism. Then the evaluation of the minimal polynomial $\text{minpoly}_A(x)$ at $f(x)$ is zero, i.e., $\text{minpoly}_A(x)(f(x)) = 0$.

minpoly.ne_one theorem

[Nontrivial B] : minpoly A x ≠ 1

Full source

/-- A minimal polynomial is not `1`. -/
theorem ne_one [Nontrivial B] : minpolyminpoly A x ≠ 1 := by
  intro h
  refine (one_ne_zero : (1 : B) ≠ 0) ?_
  simpa using congr_arg (Polynomial.aeval x) h

Non-triviality of minimal polynomial: $\text{minpoly}_A(x) \neq 1$

Informal description

Let $B$ be a nontrivial $A$-algebra and $x \in B$ be an integral element over $A$. Then the minimal polynomial $\text{minpoly}_A(x)$ is not equal to the constant polynomial $1$.

minpoly.map_ne_one theorem

[Nontrivial B] {R : Type*} [Semiring R] [Nontrivial R] (f : A →+* R) : (minpoly A x).map f ≠ 1

Full source

theorem map_ne_one [Nontrivial B] {R : Type*} [Semiring R] [Nontrivial R] (f : A →+* R) :
    (minpoly A x).map f ≠ 1 := by
  by_cases hx : IsIntegral A x
  · exact mt ((monic hx).eq_one_of_map_eq_one f) (ne_one A x)
  · rw [eq_zero hx, Polynomial.map_zero]
    exact zero_ne_one

Non-triviality of mapped minimal polynomial: $(\text{minpoly}_A(x)).\text{map}\,f \neq 1$

Informal description

Let $A$ be a commutative ring and $B$ a nontrivial $A$-algebra. For any integral element $x \in B$ over $A$, and any nontrivial semiring $R$ with a ring homomorphism $f : A \to R$, the image of the minimal polynomial $\text{minpoly}_A(x)$ under the polynomial map induced by $f$ is not equal to the constant polynomial $1$.

minpoly.not_isUnit theorem

[Nontrivial B] : ¬IsUnit (minpoly A x)

Full source

/-- A minimal polynomial is not a unit. -/
theorem not_isUnit [Nontrivial B] : ¬IsUnit (minpoly A x) := by
  haveI : Nontrivial A := (algebraMap A B).domain_nontrivial
  by_cases hx : IsIntegral A x
  · exact mt (monic hx).eq_one_of_isUnit (ne_one A x)
  · rw [eq_zero hx]
    exact not_isUnit_zero

Non-unit Property of Minimal Polynomials

Informal description

Let $A$ be a commutative ring and $B$ a nontrivial $A$-algebra. For any element $x \in B$ that is integral over $A$, the minimal polynomial $\text{minpoly}_A(x)$ is not a unit in the polynomial ring $A[X]$.

minpoly.mem_range_of_degree_eq_one theorem

(hx : (minpoly A x).degree = 1) : x ∈ (algebraMap A B).range

Full source

theorem mem_range_of_degree_eq_one (hx : (minpoly A x).degree = 1) :
    x ∈ (algebraMap A B).range := by
  have h : IsIntegral A x := by
    by_contra h
    rw [eq_zero h, degree_zero, ← WithBot.coe_one] at hx
    exact ne_of_lt (show ⊥ < ↑1 from WithBot.bot_lt_coe 1) hx
  have key := minpoly.aeval A x
  rw [eq_X_add_C_of_degree_eq_one hx, (minpoly.monic h).leadingCoeff, C_1, one_mul, aeval_add,
    aeval_C, aeval_X, ← eq_neg_iff_add_eq_zero, ← RingHom.map_neg] at key
  exact ⟨-(minpoly A x).coeff 0, key.symm⟩

Integral elements with degree-one minimal polynomial are in the algebra map's range

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an integral element $x \in B$ over $A$, if the degree of its minimal polynomial $\text{minpoly}_A(x)$ is equal to $1$, then $x$ is in the range of the canonical algebra homomorphism $\text{algebraMap} : A \to B$.

minpoly.min theorem

{p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0) : degree (minpoly A x) ≤ degree p

Full source

/-- The defining property of the minimal polynomial of an element `x`:
it is the monic polynomial with smallest degree that has `x` as its root. -/
theorem min {p : A[X]} (pmonic : p.Monic) (hp : Polynomial.aeval x p = 0) :
    degree (minpoly A x) ≤ degree p := by
  delta minpoly; split_ifs with hx
  · exact le_of_not_lt (degree_lt_wf.not_lt_min _ hx ⟨pmonic, hp⟩)
  · simp only [degree_zero, bot_le]

Minimality of the minimal polynomial's degree: $\deg(\text{minpoly}_A(x)) \leq \deg(p)$ for monic $p$ with $p(x)=0$

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, if $p \in A[X]$ is a monic polynomial such that $p(x) = 0$, then the degree of the minimal polynomial of $x$ over $A$ is less than or equal to the degree of $p$.

minpoly.unique' theorem

 {p : A[X]} (hm : p.Monic) (hp : Polynomial.aeval x p = 0)
  (hl : ∀ q : A[X], degree q < degree p → q = 0 ∨ Polynomial.aeval x q ≠ 0) : p = minpoly A x

Full source

theorem unique' {p : A[X]} (hm : p.Monic) (hp : Polynomial.aeval x p = 0)
    (hl : ∀ q : A[X], degree q < degree p → q = 0 ∨ Polynomial.aeval x q ≠ 0) :
    p = minpoly A x := by
  nontriviality A
  have hx : IsIntegral A x := ⟨p, hm, hp⟩
  obtain h | h := hl _ ((minpoly A x).degree_modByMonic_lt hm)
  swap
  · exact (h <| (aeval_modByMonic_eq_self_of_root hm hp).trans <| aeval A x).elim
  obtain ⟨r, hr⟩ := (modByMonic_eq_zero_iff_dvd hm).1 h
  rw [hr]
  have hlead := congr_arg leadingCoeff hr
  rw [mul_comm, leadingCoeff_mul_monic hm, (monic hx).leadingCoeff] at hlead
  have : natDegree r ≤ 0 := by
    have hr0 : r ≠ 0 := by
      rintro rfl
      exact ne_zero hx (mul_zero p ▸ hr)
    apply_fun natDegree at hr
    rw [hm.natDegree_mul' hr0] at hr
    apply Nat.le_of_add_le_add_left
    rw [add_zero]
    exact hr.symm.trans_le (natDegree_le_natDegree <| min A x hm hp)
  rw [eq_C_of_natDegree_le_zero this, ← Nat.eq_zero_of_le_zero this, ← leadingCoeff, ← hlead, C_1,
    mul_one]

Uniqueness of Minimal Polynomial for Integral Elements

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an integral element $x \in B$ over $A$, if $p \in A[X]$ is a monic polynomial such that: 1. $p(x) = 0$, and 2. For every polynomial $q \in A[X]$ with $\deg(q) < \deg(p)$, either $q = 0$ or $q(x) \neq 0$, then $p$ is equal to the minimal polynomial of $x$ over $A$, i.e., $p = \text{minpoly}_A(x)$.

minpoly.subsingleton theorem

[Subsingleton B] : minpoly A x = 1

Full source

@[nontriviality]
theorem subsingleton [Subsingleton B] : minpoly A x = 1 := by
  nontriviality A
  have := minpoly.min A x monic_one (Subsingleton.elim _ _)
  rw [degree_one] at this
  rcases le_or_lt (minpoly A x).degree 0 with h | h
  · rwa [(monic ⟨1, monic_one, by simp [eq_iff_true_of_subsingleton]⟩ :
           (minpoly A x).Monic).degree_le_zero_iff_eq_one] at h
  · exact (this.not_lt h).elim

Minimal Polynomial is One in Subsingleton Algebras

Informal description

If the $A$-algebra $B$ is a subsingleton (i.e., has at most one element), then the minimal polynomial of any element $x \in B$ over $A$ is equal to the constant polynomial $1$.

minpoly.natDegree_pos theorem

[Nontrivial B] (hx : IsIntegral A x) : 0 < natDegree (minpoly A x)

Full source

/-- The degree of a minimal polynomial, as a natural number, is positive. -/
theorem natDegree_pos [Nontrivial B] (hx : IsIntegral A x) : 0 < natDegree (minpoly A x) := by
  rw [pos_iff_ne_zero]
  intro ndeg_eq_zero
  have eq_one : minpoly A x = 1 := by
    rw [eq_C_of_natDegree_eq_zero ndeg_eq_zero]
    convert C_1 (R := A)
    simpa only [ndeg_eq_zero.symm] using (monic hx).leadingCoeff
  simpa only [eq_one, map_one, one_ne_zero] using aeval A x

Positivity of the Degree of the Minimal Polynomial of an Integral Element

Informal description

Let $B$ be a nontrivial $A$-algebra and $x \in B$ be an integral element over $A$. Then the minimal polynomial $\text{minpoly}_A(x)$ has positive degree as a natural number, i.e., $\text{natDegree}(\text{minpoly}_A(x)) > 0$.

minpoly.degree_pos theorem

[Nontrivial B] (hx : IsIntegral A x) : 0 < degree (minpoly A x)

Full source

/-- The degree of a minimal polynomial is positive. -/
theorem degree_pos [Nontrivial B] (hx : IsIntegral A x) : 0 < degree (minpoly A x) :=
  natDegree_pos_iff_degree_pos.mp (natDegree_pos hx)

Positivity of Minimal Polynomial Degree for Integral Elements

Informal description

Let $B$ be a nontrivial $A$-algebra and $x \in B$ be an integral element over $A$. Then the minimal polynomial $\text{minpoly}_A(x)$ has positive degree, i.e., $\deg(\text{minpoly}_A(x)) > 0$.

minpoly.degree_eq_one_iff theorem

: (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range

Full source

theorem degree_eq_one_iff : (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range := by
  refine ⟨minpoly.mem_range_of_degree_eq_one _ _, ?_⟩
  rintro ⟨x, rfl⟩
  haveI := Module.nontrivial A B
  exact (degree_X_sub_C x ▸ minpoly.min A (algebraMap A B x) (monic_X_sub_C x) (by simp)).antisymm
    (Nat.WithBot.add_one_le_of_lt <| minpoly.degree_pos isIntegral_algebraMap)

Degree-One Minimal Polynomial Characterizes Elements in the Algebra Map's Range

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an integral element $x \in B$ over $A$, the degree of its minimal polynomial $\text{minpoly}_A(x)$ is equal to $1$ if and only if $x$ is in the range of the canonical algebra homomorphism $\text{algebraMap} : A \to B$.

minpoly.natDegree_eq_one_iff theorem

: (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range

Full source

theorem natDegree_eq_one_iff :
    (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range := by
  rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one]
  exact degree_eq_one_iff

Characterization of Integral Elements with Degree-One Minimal Polynomial via Algebra Map Range

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an integral element $x \in B$ over $A$, the natural degree of its minimal polynomial $\text{minpoly}_A(x)$ is equal to $1$ if and only if $x$ is in the range of the canonical algebra homomorphism $\text{algebraMap} : A \to B$.

minpoly.two_le_natDegree_iff theorem

(int : IsIntegral A x) : 2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range

Full source

theorem two_le_natDegree_iff (int : IsIntegral A x) :
    2 ≤ (minpoly A x).natDegree ↔ x ∉ (algebraMap A B).range := by
  rw [iff_not_comm, ← natDegree_eq_one_iff, not_le]
  exact ⟨fun h ↦ h.trans_lt one_lt_two, fun h ↦ by linarith only [minpoly.natDegree_pos int, h]⟩

Degree-Two Minimal Polynomial Characterizes Non-Algebraic Elements

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an integral element $x \in B$ over $A$, the minimal polynomial $\text{minpoly}_A(x)$ has degree at least 2 if and only if $x$ is not in the range of the canonical algebra homomorphism $\text{algebraMap} : A \to B$.

minpoly.two_le_natDegree_subalgebra theorem

 {B} [CommRing B] [Algebra A B] [Nontrivial B] {S : Subalgebra A B} {x : B} (int : IsIntegral S x) :
  2 ≤ (minpoly S x).natDegree ↔ x ∉ S

Full source

theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B]
    {S : Subalgebra A B} {x : B} (int : IsIntegral S x) : 2 ≤ (minpoly S x).natDegree ↔ x ∉ S := by
  rw [two_le_natDegree_iff int, Iff.not]
  apply Set.ext_iff.mp Subtype.range_val_subtype

Degree-Two Minimal Polynomial Characterizes Non-Subalgebra Elements

Informal description

Let $A$ be a commutative ring and $B$ a commutative $A$-algebra that is nontrivial. Let $S$ be a subalgebra of $B$ over $A$, and let $x \in B$ be an element integral over $S$. Then the minimal polynomial $\text{minpoly}_S(x)$ has degree at least 2 if and only if $x$ does not belong to $S$.

minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly theorem

{a : A[X]} (hx : IsIntegral A x) (hamonic : a.Monic) (hdvd : DvdNotUnit a (minpoly A x)) : Polynomial.aeval x a ≠ 0

Full source

/-- If `a` strictly divides the minimal polynomial of `x`, then `x` cannot be a root for `a`. -/
theorem aeval_ne_zero_of_dvdNotUnit_minpoly {a : A[X]} (hx : IsIntegral A x) (hamonic : a.Monic)
    (hdvd : DvdNotUnit a (minpoly A x)) : Polynomial.aevalPolynomial.aeval x a ≠ 0 := by
  refine fun ha => (min A x hamonic ha).not_lt (degree_lt_degree ?_)
  obtain ⟨_, c, hu, he⟩ := hdvd
  have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
  rw [he, hamonic.natDegree_mul hcm]
  -- TODO: port Nat.lt_add_of_zero_lt_left from lean3 core
  apply lt_add_of_pos_right
  refine (lt_of_not_le fun h => hu ?_)
  rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
    C_1]
  exact isUnit_one

Non-root property for strict divisors of minimal polynomial: $a(x) \neq 0$ when $a$ strictly divides $\text{minpoly}_A(x)$

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For an element $x \in B$ integral over $A$, if a monic polynomial $a \in A[X]$ strictly divides the minimal polynomial of $x$ (i.e., $a$ divides $\text{minpoly}_A(x)$ but is not associated to it via a unit), then $x$ is not a root of $a$, i.e., $a(x) \neq 0$.

minpoly.irreducible theorem

(hx : IsIntegral A x) : Irreducible (minpoly A x)

Full source

/-- A minimal polynomial is irreducible. -/
theorem irreducible (hx : IsIntegral A x) : Irreducible (minpoly A x) := by
  refine (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => ?_
  rw [← hf.isUnit_iff, ← hg.isUnit_iff]
  by_contra! h
  have heval := congr_arg (Polynomial.aeval x) he
  rw [aeval A x, aeval_mul, mul_eq_zero] at heval
  rcases heval with heval | heval
  · exact aeval_ne_zero_of_dvdNotUnit_minpoly hx hf ⟨hf.ne_zero, g, h.2, he.symm⟩ heval
  · refine aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval
    rw [mul_comm, he]

Irreducibility of the Minimal Polynomial of an Integral Element

Informal description

Let $A$ be a commutative ring and $B$ an $A$-algebra. For any element $x \in B$ that is integral over $A$, the minimal polynomial $\text{minpoly}_A(x)$ is irreducible in $A[X]$.