feat(data/polynomial): irreducibility criteria for (quadratic) monic polynomials (#17664)

alreadydone · alreadydone · commit fa256f00ce01 · 2022-12-06T17:02:06.000Z
+ To show a monic polynomial `p` over a commutative semiring without zero divisors is irreducible, it suffices to show that `p ≠ 1` and that there doesn't exist a factorization into the product of two monic polynomials of positive degrees: `monic.irreducible_iff_nat_degree`. + If such a factorization exists, one of the polynomial must have degree less than or equal to `p.nat_degree / 2`: `monic.irreducible_iff_nat_degree'`. + To show a quadratic monic polynomial `p` is reducible, it suffices to it doesn't factor as `(X+c)(X+c')`, i.e. there don't exist `c` and `c'` that add up to the 1st coefficient and multiply up to the 0th coefficient: `not_irreducible_iff_exists_add_mul_eq_coeff`. + Define the ring homomorphism `constant_coeff` in *coeff.lean* which is analogous to [mv_polynomial.constant_coeff](https://leanprover-community.github.io/mathlib_docs/data/mv_polynomial/basic.html#mv_polynomial.constant_coeff); use it to golf and generalize `is_unit_C` and `eq_one_of_is_unit_of_monic` in *monic.lean* and various lemmas in *ring_division.lean*. + Add `monic.is_unit_iff`. + Golf some lemmas in *erase_lead.lean*. Co-authored-by: Thomas Browning <thomas.l.browning@gmail.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl> Inspired by #17631
diff --git a/src/data/polynomial/coeff.lean b/src/data/polynomial/coeff.lean
@@ -96,11 +96,17 @@ end
 @[simp] lemma mul_coeff_zero (p q : R[X]) : coeff (p * q) 0 = coeff p 0 * coeff q 0 :=
 by simp [coeff_mul]
 
--- TODO: golf using `constant_coeff` once #17664 is merged
+/-- `constant_coeff p` returns the constant term of the polynomial `p`,
+  defined as `coeff p 0`. This is a ring homomorphism. -/
+@[simps] def constant_coeff : R[X] →+* R :=
+{ to_fun := λ p, coeff p 0,
+  map_one' := coeff_one_zero,
+  map_mul' := mul_coeff_zero,
+  map_zero' := coeff_zero 0,
+  map_add' :=  λ p q, coeff_add p q 0 }
+
 lemma is_unit_C {x : R} : is_unit (C x) ↔ is_unit x :=
-⟨by { rintros ⟨⟨q, p, hqp, hpq⟩, rfl : q = C x⟩,
-  exact ⟨⟨(C x).coeff 0, p.coeff 0, by rw [←mul_coeff_zero, hqp, coeff_one_zero],
-    by rw [←mul_coeff_zero, hpq, coeff_one_zero]⟩, coeff_C_zero⟩ }, is_unit.map C⟩
+⟨λ h, (congr_arg is_unit coeff_C_zero).mp (h.map $ @constant_coeff R _), λ h, h.map C⟩
 
 lemma coeff_mul_X_zero (p : R[X]) : coeff (p * X) 0 = 0 := by simp
 
diff --git a/src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/definitions.lean
@@ -347,12 +347,15 @@ ext (λ n, nat.cases_on n (by simp)
 lemma eq_X_add_C_of_degree_eq_one (h : degree p = 1) :
   p = C (p.leading_coeff) * X + C (p.coeff 0) :=
 (eq_X_add_C_of_degree_le_one (show degree p ≤ 1, from h ▸ le_rfl)).trans
-  (by simp [leading_coeff, nat_degree_eq_of_degree_eq_some h])
+  (by simp only [leading_coeff, nat_degree_eq_of_degree_eq_some h])
 
 lemma eq_X_add_C_of_nat_degree_le_one (h : nat_degree p ≤ 1) :
   p = C (p.coeff 1) * X + C (p.coeff 0) :=
 eq_X_add_C_of_degree_le_one $ degree_le_of_nat_degree_le h
 
+lemma monic.eq_X_add_C (hm : p.monic) (hnd : p.nat_degree = 1) : p = X + C (p.coeff 0) :=
+by rw [←one_mul X, ←C_1, ←hm.coeff_nat_degree, hnd, ←eq_X_add_C_of_nat_degree_le_one hnd.le]
+
 lemma exists_eq_X_add_C_of_nat_degree_le_one (h : nat_degree p ≤ 1) :
   ∃ a b, p = C a * X + C b :=
 ⟨p.coeff 1, p.coeff 0, eq_X_add_C_of_nat_degree_le_one h⟩
@@ -1116,6 +1119,12 @@ begin
   { exact nat_degree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r) },
 end
 
+lemma X_pow_add_C_ne_one {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 1 :=
+λ h, hn.ne' $ by simpa only [nat_degree_X_pow_add_C, nat_degree_one] using congr_arg nat_degree h
+
+theorem X_add_C_ne_one (r : R) : X + C r ≠ 1 :=
+pow_one (X : R[X]) ▸ X_pow_add_C_ne_one zero_lt_one r
+
 end semiring
 end nonzero_ring
 
diff --git a/src/data/polynomial/erase_lead.lean b/src/data/polynomial/erase_lead.lean
@@ -54,13 +54,7 @@ by simp only [erase_lead, erase_zero]
 
 @[simp] lemma erase_lead_add_monomial_nat_degree_leading_coeff (f : R[X]) :
   f.erase_lead + monomial f.nat_degree f.leading_coeff = f :=
-begin
-  ext i,
-  simp only [erase_lead_coeff, coeff_monomial, coeff_add, @eq_comm _ _ i],
-  split_ifs with h,
-  { subst i, simp only [leading_coeff, zero_add] },
-  { exact add_zero _ }
-end
+(add_comm _ _).trans (f.monomial_add_erase _)
 
 @[simp] lemma erase_lead_add_C_mul_X_pow (f : R[X]) :
   f.erase_lead + (C f.leading_coeff) * X ^ f.nat_degree = f :=
@@ -76,7 +70,7 @@ by rw [C_mul_X_pow_eq_monomial, self_sub_monomial_nat_degree_leading_coeff]
 
 lemma erase_lead_ne_zero (f0 : 2 ≤ f.support.card) : erase_lead f ≠ 0 :=
 begin
-  rw [ne.def, ← card_support_eq_zero, erase_lead_support],
+  rw [ne, ← card_support_eq_zero, erase_lead_support],
   exact (zero_lt_one.trans_le $ (tsub_le_tsub_right f0 1).trans
     finset.pred_card_le_card_erase).ne.symm
 end
@@ -85,7 +79,7 @@ lemma lt_nat_degree_of_mem_erase_lead_support {a : ℕ} (h : a ∈ (erase_lead f
   a < f.nat_degree :=
 begin
   rw [erase_lead_support, mem_erase] at h,
-  exact lt_of_le_of_ne (le_nat_degree_of_mem_supp a h.2) h.1,
+  exact (le_nat_degree_of_mem_supp a h.2).lt_of_ne h.1,
 end
 
 lemma ne_nat_degree_of_mem_erase_lead_support {a : ℕ} (h : a ∈ (erase_lead f).support) :
@@ -157,14 +151,7 @@ begin
     exact nd (nat_degree_add_eq_right_of_nat_degree_lt pq) }
 end
 
-lemma erase_lead_degree_le : (erase_lead f).degree ≤ f.degree :=
-begin
-  rw degree_le_iff_coeff_zero,
-  intros i hi,
-  rw erase_lead_coeff,
-  split_ifs with h, { refl },
-  apply coeff_eq_zero_of_degree_lt hi
-end
+lemma erase_lead_degree_le : (erase_lead f).degree ≤ f.degree := f.degree_erase_le _
 
 lemma erase_lead_nat_degree_le_aux : (erase_lead f).nat_degree ≤ f.nat_degree :=
 nat_degree_le_nat_degree erase_lead_degree_le
diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
@@ -786,6 +786,9 @@ def eval_ring_hom : R → R[X] →+* R := eval₂_ring_hom (ring_hom.id _)
 
 @[simp] lemma coe_eval_ring_hom (r : R) : ((eval_ring_hom r) : R[X] → R) = eval r := rfl
 
+lemma eval_ring_hom_zero : eval_ring_hom 0 = constant_coeff :=
+fun_like.ext _ _ $ λ p, p.coeff_zero_eq_eval_zero.symm
+
 @[simp] lemma eval_pow (n : ℕ) : (p ^ n).eval x = p.eval x ^ n := eval₂_pow _ _ _
 
 @[simp]
diff --git a/src/data/polynomial/monic.lean b/src/data/polynomial/monic.lean
@@ -222,6 +222,9 @@ begin
   exact hm.nat_degree_eq_zero_iff_eq_one.mp this.1,
 end
 
+lemma monic.is_unit_iff (hm : p.monic) : is_unit p ↔ p = 1 :=
+⟨hm.eq_one_of_is_unit, λ h, h.symm ▸ is_unit_one⟩
+
 end semiring
 
 section comm_semiring
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
@@ -183,9 +183,12 @@ begin
 end
 
 lemma degree_eq_zero_of_is_unit [nontrivial R] (h : is_unit p) : degree p = 0 :=
-le_antisymm (nat_degree_eq_zero_iff_degree_le_zero.mp (nat_degree_eq_zero_of_is_unit h))
+(nat_degree_eq_zero_iff_degree_le_zero.mp $ nat_degree_eq_zero_of_is_unit h).antisymm
   (zero_le_degree_iff.mpr h.ne_zero)
 
+@[simp] lemma degree_coe_units [nontrivial R] (u : R[X]ˣ) : degree (u : R[X]) = 0 :=
+degree_eq_zero_of_is_unit ⟨u, rfl⟩
+
 theorem is_unit_iff : is_unit p ↔ ∃ r : R, is_unit r ∧ C r = p :=
 ⟨λ hp, ⟨p.coeff 0, let h := eq_C_of_nat_degree_eq_zero (nat_degree_eq_zero_of_is_unit hp) in
   ⟨is_unit_C.1 (h ▸ hp), h.symm⟩⟩, λ ⟨r, hr, hrp⟩, hrp ▸ is_unit_C.2 hr⟩
@@ -228,16 +231,58 @@ variables [comm_semiring R] [no_zero_divisors R] {p q : R[X]}
 lemma irreducible_of_monic (hp : p.monic) (hp1 : p ≠ 1) :
   irreducible p ↔ ∀ f g : R[X], f.monic → g.monic → f * g = p → f = 1 ∨ g = 1 :=
 begin
-  refine ⟨λ h f g hf hg hp, (h.2 f g hp.symm).elim (or.inl ∘ hf.eq_one_of_is_unit)
-    (or.inr ∘ hg.eq_one_of_is_unit), λ h, ⟨hp1 ∘ hp.eq_one_of_is_unit, λ f g hfg,
-      (h (g * C f.leading_coeff) (f * C g.leading_coeff) _ _ _).elim
-        (or.inr ∘ is_unit_of_mul_eq_one g _) (or.inl ∘ is_unit_of_mul_eq_one f _)⟩⟩,
+  refine ⟨λ h f g hf hg hp, (h.2 f g hp.symm).imp hf.eq_one_of_is_unit hg.eq_one_of_is_unit,
+    λ h, ⟨hp1 ∘ hp.eq_one_of_is_unit, λ f g hfg, (h (g * C f.leading_coeff) (f * C g.leading_coeff)
+      _ _ _).symm.imp (is_unit_of_mul_eq_one f _) (is_unit_of_mul_eq_one g _)⟩⟩,
   { rwa [monic, leading_coeff_mul, leading_coeff_C, ←leading_coeff_mul, mul_comm, ←hfg, ←monic] },
   { rwa [monic, leading_coeff_mul, leading_coeff_C, ←leading_coeff_mul, ←hfg, ←monic] },
   { rw [mul_mul_mul_comm, ←C_mul, ←leading_coeff_mul, ←hfg, hp.leading_coeff, C_1, mul_one,
         mul_comm, ←hfg] },
 end
 
+lemma monic.irreducible_iff_nat_degree (hp : p.monic) : irreducible p ↔
+  p ≠ 1 ∧ ∀ f g : R[X], f.monic → g.monic → f * g = p → f.nat_degree = 0 ∨ g.nat_degree = 0 :=
+begin
+  by_cases hp1 : p = 1, { simp [hp1] },
+  rw [irreducible_of_monic hp hp1, and_iff_right hp1],
+  refine forall₄_congr (λ a b ha hb, _),
+  rw [ha.nat_degree_eq_zero_iff_eq_one, hb.nat_degree_eq_zero_iff_eq_one],
+end
+
+lemma monic.irreducible_iff_nat_degree' (hp : p.monic) : irreducible p ↔ p ≠ 1 ∧
+  ∀ f g : R[X], f.monic → g.monic → f * g = p → g.nat_degree ∉ Ioc 0 (p.nat_degree / 2) :=
+begin
+  simp_rw [hp.irreducible_iff_nat_degree, mem_Ioc, nat.le_div_iff_mul_le zero_lt_two, mul_two],
+  apply and_congr_right',
+  split; intros h f g hf hg he; subst he,
+  { rw [hf.nat_degree_mul hg, add_le_add_iff_right],
+    exact λ ha, (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne' },
+  { simp_rw [hf.nat_degree_mul hg, pos_iff_ne_zero] at h,
+    contrapose! h,
+    obtain hl|hl := le_total f.nat_degree g.nat_degree,
+    { exact ⟨g, f, hg, hf, mul_comm g f, h.1, add_le_add_left hl _⟩ },
+    { exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩ } },
+end
+
+lemma monic.not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.monic) (hnd : p.nat_degree = 2) :
+  ¬ irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂ :=
+begin
+  casesI subsingleton_or_nontrivial R,
+  { simpa only [nat_degree_of_subsingleton] using hnd },
+  rw [hm.irreducible_iff_nat_degree', and_iff_right, hnd],
+  push_neg, split,
+  { rintros ⟨a, b, ha, hb, rfl, hdb|⟨⟨⟩⟩⟩,
+    have hda := hnd, rw [ha.nat_degree_mul hb, hdb] at hda,
+    use [a.coeff 0, b.coeff 0, mul_coeff_zero a b],
+    simpa only [next_coeff, hnd, add_right_cancel hda, hdb] using ha.next_coeff_mul hb },
+  { rintros ⟨c₁, c₂, hmul, hadd⟩,
+    refine ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, _, or.inl $ nat_degree_X_add_C _⟩,
+    rw [p.as_sum_range_C_mul_X_pow, hnd, finset.sum_range_succ, finset.sum_range_succ,
+      finset.sum_range_one, ← hnd, hm.coeff_nat_degree, hnd, hmul, hadd, C_mul, C_add, C_1],
+    ring },
+  { rintro rfl, simpa only [nat_degree_one] using hnd },
+end
+
 lemma root_mul : is_root (p * q) a ↔ is_root p a ∨ is_root q a :=
 by simp_rw [is_root, eval_mul, mul_eq_zero]
 
@@ -291,10 +336,6 @@ section roots
 
 open multiset
 
-@[simp] lemma degree_coe_units (u : R[X]ˣ) :
-  degree (u : R[X]) = 0 :=
-degree_eq_zero_of_is_unit ⟨u, rfl⟩
-
 theorem prime_X_sub_C (r : R) : prime (X - C r) :=
 ⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C r,
  λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩
@@ -322,10 +363,10 @@ theorem eq_of_monic_of_associated (hp : p.monic) (hq : q.monic) (hpq : associate
 begin
   obtain ⟨u, hu⟩ := hpq,
   unfold monic at hp hq,
-  rw eq_C_of_degree_le_zero (le_of_eq $ degree_coe_units _) at hu,
+  rw eq_C_of_degree_le_zero (degree_coe_units _).le at hu,
   rw [← hu, leading_coeff_mul, hp, one_mul, leading_coeff_C] at hq,
   rwa [hq, C_1, mul_one] at hu,
-  apply_instance,
+  all_goals { apply_instance },
 end
 
 lemma root_multiplicity_mul {p q : R[X]} {x : R} (hpq : p * q ≠ 0) :
