feat(Data/Polynomial): irreducibility of degree-{2,3} polynomials (#9697)

The goal is to show that a degree 2 or 3 polynomial is irreducible iff it doesn't have roots. We already have `Polynomial.Monic.irreducible_iff_natDegree'` and some existing results in Lean 3: https://github.com/lean-forward/class-group-and-mordell-equation/blob/main/src/number_theory/assorted_lemmas.lean#L254 and the main work is to connect these bits together.

I added a few helper lemmas about the "monicization" of a polynomial `p`, `p * C (leadingCoeff p)⁻¹`. Then I used these to show the `Polynomial.Monic.irreducible_iff ...` statements could be translated to (not necessarily monic) polynomials over a field, then I specialized these results to the degree-{2,3} case.

I created a new file because I couldn't find an obvious place that imported both `Polynomial.FieldDivision` and `Tactic.IntervalCases`.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Polynomial.20irreducible




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: Vierkantor

Mathlib.lean

@@ -1933,6 +1933,7 @@ import Mathlib.Data.Polynomial.PartialFractions
 import Mathlib.Data.Polynomial.Reverse
 import Mathlib.Data.Polynomial.RingDivision
 import Mathlib.Data.Polynomial.Smeval
+import Mathlib.Data.Polynomial.SpecificDegree
 import Mathlib.Data.Polynomial.Splits
 import Mathlib.Data.Polynomial.Taylor
 import Mathlib.Data.Polynomial.UnitTrinomial

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -1685,6 +1685,10 @@ theorem leadingCoeff_pow (p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCo
   (leadingCoeffHom : R[X] →* R).map_pow p n
 #align polynomial.leading_coeff_pow Polynomial.leadingCoeff_pow
 
+theorem leadingCoeff_dvd_leadingCoeff {a p : R[X]} (hap : a ∣ p) :
+    a.leadingCoeff ∣ p.leadingCoeff :=
+  map_dvd leadingCoeffHom hap
+
 end NoZeroDivisors
 
 end Polynomial

Mathlib/Data/Polynomial/Degree/Lemmas.lean

@@ -421,4 +421,59 @@ theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
 
 end NoZeroDivisors
 
+section DivisionRing
+
+variable {K : Type*} [DivisionRing K]
+
+/-! Useful lemmas for the "monicization" of a nonzero polynomial `p`. -/
+@[simp]
+theorem irreducible_mul_leadingCoeff_inv {p : K[X]} :
+    Irreducible (p * C (leadingCoeff p)⁻¹) ↔ Irreducible p := by
+  by_cases hp0 : p = 0
+  · simp [hp0]
+  exact irreducible_mul_isUnit
+    (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))
+
+@[simp] lemma dvd_mul_leadingCoeff_inv {p q : K[X]} (hp0 : p ≠ 0) :
+    q ∣ p * C (leadingCoeff p)⁻¹ ↔ q ∣ p :=
+  IsUnit.dvd_mul_right <| isUnit_C.mpr <| IsUnit.mk0 _ <|
+    inv_ne_zero <| leadingCoeff_ne_zero.mpr hp0
+
+theorem monic_mul_leadingCoeff_inv {p : K[X]} (h : p ≠ 0) : Monic (p * C (leadingCoeff p)⁻¹) := by
+  rw [Monic, leadingCoeff_mul, leadingCoeff_C,
+    mul_inv_cancel (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
+#align polynomial.monic_mul_leading_coeff_inv Polynomial.monic_mul_leadingCoeff_inv
+
+-- `simp` normal form of `degree_mul_leadingCoeff_inv`
+@[simp] lemma degree_leadingCoeff_inv {p : K[X]} (hp0 : p ≠ 0) :
+    degree (C (leadingCoeff p)⁻¹) = 0 :=
+  degree_C (inv_ne_zero <| leadingCoeff_ne_zero.mpr hp0)
+
+theorem degree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) :
+    degree (p * C (leadingCoeff q)⁻¹) = degree p := by
+  have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
+  rw [degree_mul_C h₁]
+#align polynomial.degree_mul_leading_coeff_inv Polynomial.degree_mul_leadingCoeff_inv
+
+theorem natDegree_mul_leadingCoeff_inv (p : K[X]) {q : K[X]} (h : q ≠ 0) :
+    natDegree (p * C (leadingCoeff q)⁻¹) = natDegree p :=
+  natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_inv _ h)
+
+theorem degree_mul_leadingCoeff_self_inv (p : K[X]) :
+    degree (p * C (leadingCoeff p)⁻¹) = degree p := by
+  by_cases hp : p = 0
+  · simp [hp]
+  exact degree_mul_leadingCoeff_inv _ hp
+
+theorem natDegree_mul_leadingCoeff_self_inv (p : K[X]) :
+    natDegree (p * C (leadingCoeff p)⁻¹) = natDegree p :=
+  natDegree_eq_of_degree_eq (degree_mul_leadingCoeff_self_inv _)
+
+-- `simp` normal form of `degree_mul_leadingCoeff_self_inv`
+@[simp] lemma degree_add_degree_leadingCoeff_inv (p : K[X]) :
+    degree p + degree (C (leadingCoeff p)⁻¹) = degree p := by
+  rw [← degree_mul, degree_mul_leadingCoeff_self_inv]
+
+end DivisionRing
+
 end Polynomial

Mathlib/Data/Polynomial/FieldDivision.lean

@@ -225,17 +225,6 @@ theorem degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬IsUnit p) : 0 <
     exact hp (IsUnit.map C (IsUnit.mk0 (coeff p 0) (mt C_inj.2 (by simpa using hp0))))
 #align polynomial.degree_pos_of_ne_zero_of_nonunit Polynomial.degree_pos_of_ne_zero_of_nonunit
 
-theorem monic_mul_leadingCoeff_inv (h : p ≠ 0) : Monic (p * C (leadingCoeff p)⁻¹) := by
-  rw [Monic, leadingCoeff_mul, leadingCoeff_C,
-    mul_inv_cancel (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]
-#align polynomial.monic_mul_leading_coeff_inv Polynomial.monic_mul_leadingCoeff_inv
-
-theorem degree_mul_leadingCoeff_inv (p : R[X]) (h : q ≠ 0) :
-    degree (p * C (leadingCoeff q)⁻¹) = degree p := by
-  have h₁ : (leadingCoeff q)⁻¹ ≠ 0 := inv_ne_zero (mt leadingCoeff_eq_zero.1 h)
-  rw [degree_mul, degree_C h₁, add_zero]
-#align polynomial.degree_mul_leading_coeff_inv Polynomial.degree_mul_leadingCoeff_inv
-
 @[simp]
 theorem map_eq_zero [Semiring S] [Nontrivial S] (f : R →+* S) : p.map f = 0 ↔ p = 0 := by
   simp only [Polynomial.ext_iff]
@@ -655,6 +644,35 @@ theorem isCoprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [Field K] (f
   rwa [← C_inj, C_0]
 #align polynomial.is_coprime_of_is_root_of_eval_derivative_ne_zero Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero
 
+/-- To check a polynomial over a field is irreducible, it suffices to check only for
+divisors that have smaller degree.
+
+See also: `Polynomial.Monic.irreducible_iff_natDegree`.
+-/
+theorem irreducible_iff_degree_lt (p : R[X]) (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
+    Irreducible p ↔ ∀ q, q.degree ≤ ↑(natDegree p / 2) → q ∣ p → IsUnit q := by
+  rw [← irreducible_mul_leadingCoeff_inv,
+      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_degree_lt]
+  simp [hp0, natDegree_mul_leadingCoeff_inv]
+  · contrapose! hpu
+    exact isUnit_of_mul_eq_one _ _ hpu
+
+/-- To check a polynomial `p` over a field is irreducible, it suffices to check there are no
+divisors of degree `0 < d ≤ degree p / 2`.
+
+See also: `Polynomial.Monic.irreducible_iff_natDegree'`.
+-/
+theorem irreducible_iff_lt_natDegree_lt {p : R[X]} (hp0 : p ≠ 0) (hpu : ¬ IsUnit p) :
+    Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p := by
+  have : p * C (leadingCoeff p)⁻¹ ≠ 1
+  · contrapose! hpu
+    exact isUnit_of_mul_eq_one _ _ hpu
+  rw [← irreducible_mul_leadingCoeff_inv,
+      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
+      natDegree_mul_leadingCoeff_inv _ hp0]
+  simp only [IsUnit.dvd_mul_right
+    (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]
+
 end Field
 
 end Polynomial

Mathlib/Data/Polynomial/RingDivision.lean

@@ -239,6 +239,17 @@ theorem isUnit_iff : IsUnit p ↔ ∃ r : R, IsUnit r ∧ C r = p :=
     fun ⟨_, hr, hrp⟩ => hrp ▸ isUnit_C.2 hr⟩
 #align polynomial.is_unit_iff Polynomial.isUnit_iff
 
+theorem not_isUnit_of_degree_pos (p : R[X])
+    (hpl : 0 < p.degree) : ¬ IsUnit p := by
+  cases subsingleton_or_nontrivial R
+  · simp [Subsingleton.elim p 0] at hpl
+  intro h
+  simp [degree_eq_zero_of_isUnit h] at hpl
+
+theorem not_isUnit_of_natDegree_pos (p : R[X])
+    (hpl : 0 < p.natDegree) : ¬ IsUnit p :=
+  not_isUnit_of_degree_pos _ (natDegree_pos_iff_degree_pos.mp hpl)
+
 variable [CharZero R]
 
 -- Porting note: bit0/bit1 are deprecated
@@ -314,6 +325,17 @@ theorem Monic.irreducible_iff_natDegree' (hp : p.Monic) : Irreducible p ↔ p 
     · exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩
 #align polynomial.monic.irreducible_iff_nat_degree' Polynomial.Monic.irreducible_iff_natDegree'
 
+/-- Alternate phrasing of `Polynomial.Monic.irreducible_iff_natDegree'` where we only have to check
+one divisor at a time. -/
+theorem Monic.irreducible_iff_lt_natDegree_lt {p : R[X]} (hp : p.Monic) (hp1 : p ≠ 1) :
+    Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p := by
+  rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
+  constructor
+  · rintro h g hg hdg ⟨f, rfl⟩
+    exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg
+  · rintro h f g - hg rfl hdg
+    exact h g hg hdg (dvd_mul_left g f)
+
 theorem Monic.not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.Monic) (hnd : p.natDegree = 2) :
     ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂ := by
   cases subsingleton_or_nontrivial R
@@ -358,6 +380,38 @@ instance : IsDomain R[X] :=
 
 end Ring
 
+section CommSemiring
+
+variable [CommSemiring R]
+
+theorem Monic.C_dvd_iff_isUnit {p : R[X]} (hp : Monic p) {a : R} :
+    C a ∣ p ↔ IsUnit a :=
+  ⟨fun h => isUnit_iff_dvd_one.mpr <|
+      hp.coeff_natDegree ▸ (C_dvd_iff_dvd_coeff _ _).mp h p.natDegree,
+   fun ha => (ha.map C).dvd⟩
+
+theorem degree_pos_of_not_isUnit_of_dvd_monic {a p : R[X]} (ha : ¬ IsUnit a)
+    (hap : a ∣ p) (hp : Monic p) :
+    0 < degree a :=
+  lt_of_not_ge <| fun h => ha <| by
+    rw [Polynomial.eq_C_of_degree_le_zero h] at hap ⊢
+    simpa [hp.C_dvd_iff_isUnit, isUnit_C] using hap
+
+theorem natDegree_pos_of_not_isUnit_of_dvd_monic {a p : R[X]} (ha : ¬ IsUnit a)
+    (hap : a ∣ p) (hp : Monic p) :
+    0 < natDegree a :=
+  natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_not_isUnit_of_dvd_monic ha hap hp
+
+theorem degree_pos_of_monic_of_not_isUnit {a : R[X]} (hu : ¬ IsUnit a) (ha : Monic a) :
+    0 < degree a :=
+  degree_pos_of_not_isUnit_of_dvd_monic hu dvd_rfl ha
+
+theorem natDegree_pos_of_monic_of_not_isUnit {a : R[X]} (hu : ¬ IsUnit a) (ha : Monic a) :
+    0 < natDegree a :=
+  natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_monic_of_not_isUnit hu ha
+
+end CommSemiring
+
 section CommRing
 
 variable [CommRing R]
@@ -1440,6 +1494,31 @@ theorem prod_multiset_X_sub_C_of_monic_of_roots_card_eq (hp : p.Monic)
 set_option linter.uppercaseLean3 false in
 #align polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq
 
+theorem Monic.isUnit_leadingCoeff_of_dvd {a p : R[X]} (hp : Monic p) (hap : a ∣ p) :
+    IsUnit a.leadingCoeff :=
+  isUnit_of_dvd_one (by simpa only [hp.leadingCoeff] using leadingCoeff_dvd_leadingCoeff hap)
+
+/-- To check a monic polynomial is irreducible, it suffices to check only for
+divisors that have smaller degree.
+
+See also: `Polynomial.Monic.irreducible_iff_natDegree`.
+-/
+theorem Monic.irreducible_iff_degree_lt {p : R[X]} (p_monic : Monic p) (p_1 : p ≠ 1) :
+    Irreducible p ↔ ∀ q, degree q ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q := by
+  simp only [p_monic.irreducible_iff_lt_natDegree_lt p_1, mem_Ioc, and_imp,
+    natDegree_pos_iff_degree_pos, natDegree_le_iff_degree_le]
+  constructor
+  · rintro h q deg_le dvd
+    by_contra q_unit
+    have := degree_pos_of_not_isUnit_of_dvd_monic q_unit dvd p_monic
+    have hu := p_monic.isUnit_leadingCoeff_of_dvd dvd
+    refine (h _ (monic_of_isUnit_leadingCoeff_inv_smul hu) ?_ ?_ (dvd_trans ?_ dvd)).elim
+    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
+    · rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]
+    · rw [Units.smul_def, Polynomial.smul_eq_C_mul, (isUnit_C.mpr (Units.isUnit _)).mul_left_dvd]
+  · rintro h q _ deg_pos deg_le dvd
+    exact deg_pos.ne' <| degree_eq_zero_of_isUnit (h q deg_le dvd)
+
 end CommRing
 
 section

Mathlib/Data/Polynomial/SpecificDegree.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2024 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen, Alex J. Best
+-/
+import Mathlib.Data.Polynomial.RingDivision
+import Mathlib.Tactic.IntervalCases
+
+/-!
+# Polynomials of specific degree
+
+Facts about polynomials that have a specific integer degree.
+-/
+
+namespace Polynomial
+
+section IsDomain
+
+variable {R : Type*} [CommRing R] [IsDomain R]
+
+/-- A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots. -/
+theorem Monic.irreducible_iff_roots_eq_zero_of_degree_le_three {p : R[X]} (hp : p.Monic)
+    (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0 := by
+  have hp0 : p ≠ 0 := hp.ne_zero
+  have hp1 : p ≠ 1 := by rintro rfl; rw [natDegree_one] at hp2; cases hp2
+  rw [hp.irreducible_iff_lt_natDegree_lt hp1]
+  simp_rw [show p.natDegree / 2 = 1 from
+      (Nat.div_le_div_right hp3).antisymm
+        (by apply Nat.div_le_div_right (c := 2) hp2),
+    show Finset.Ioc 0 1 = {1} from rfl,
+    Finset.mem_singleton, Multiset.eq_zero_iff_forall_not_mem, mem_roots hp0, ← dvd_iff_isRoot]
+  refine ⟨fun h r ↦ h _ (monic_X_sub_C r) (natDegree_X_sub_C r), fun h q hq hq1 ↦ ?_⟩
+  rw [hq.eq_X_add_C hq1, ← sub_neg_eq_add, ← C_neg]
+  apply h
+
+end IsDomain
+
+section Field
+
+variable {K : Type*} [Field K]
+
+/-- A polynomial of degree 2 or 3 is irreducible iff it doesn't have roots. -/
+theorem irreducible_iff_roots_eq_zero_of_degree_le_three
+    {p : K[X]} (hp2 : 2 ≤ p.natDegree) (hp3 : p.natDegree ≤ 3) : Irreducible p ↔ p.roots = 0 := by
+  have hp0 : p ≠ 0 := by rintro rfl; rw [natDegree_zero] at hp2; cases hp2
+  rw [← irreducible_mul_leadingCoeff_inv,
+      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_roots_eq_zero_of_degree_le_three,
+      mul_comm, roots_C_mul]
+  · exact inv_ne_zero (leadingCoeff_ne_zero.mpr hp0)
+  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]
+  · rwa [natDegree_mul_leadingCoeff_inv _ hp0]
+
+end Field
+
+end Polynomial

Mathlib/RingTheory/Polynomial/Nilpotent.lean

@@ -169,6 +169,20 @@ lemma isUnit_iff' :
   conv_lhs => rw [← modByMonic_add_div P monic_X]
   simp [modByMonic_X]
 
+theorem not_isUnit_of_natDegree_pos_of_isReduced [IsReduced R] (p : R[X])
+    (hpl : 0 < p.natDegree) : ¬ IsUnit p := by
+  simp only [ne_eq, isNilpotent_iff_eq_zero, not_and, not_forall, exists_prop,
+    Polynomial.isUnit_iff_coeff_isUnit_isNilpotent]
+  intro _
+  refine ⟨p.natDegree, hpl.ne', ?_⟩
+  contrapose! hpl
+  simp only [coeff_natDegree, leadingCoeff_eq_zero] at hpl
+  simp [hpl]
+
+theorem not_isUnit_of_degree_pos_of_isReduced [IsReduced R] (p : R[X])
+    (hpl : 0 < p.degree) : ¬ IsUnit p :=
+  not_isUnit_of_natDegree_pos_of_isReduced _ (natDegree_pos_iff_degree_pos.mpr hpl)
+
 end CommRing
 
 section CommAlgebra