feat(ring_theory/unique_factorization_domain): descending chain condition for divisibility (#4031)

Defines the strict divisibility relation `dvd_not_unit`
Defines class `wf_dvd_monoid`, indicating that `dvd_not_unit` is well-founded
Provides instances of `wf_dvd_monoid`
Prepares to refactor `unique_factorization_domain` as a predicate extending `wf_dvd_monoid`



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: awainverse

src/algebra/associated.lean

@@ -35,7 +35,7 @@ lemma is_unit_of_dvd_one [comm_monoid α] : ∀a ∣ 1, is_unit (a:α)
 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
 
 lemma dvd_and_not_dvd_iff [comm_cancel_monoid_with_zero α] {x y : α} :
-  x ∣ y ∧ ¬y ∣ x ↔ x ≠ 0 ∧ ∃ d : α, ¬ is_unit d ∧ y = x * d :=
+  x ∣ y ∧ ¬y ∣ x ↔ dvd_not_unit x y :=
 ⟨λ ⟨⟨d, hd⟩, hyx⟩, ⟨λ hx0, by simpa [hx0] using hyx, ⟨d,
     mt is_unit_iff_dvd_one.1 (λ ⟨e, he⟩, hyx ⟨e, by rw [hd, mul_assoc, ← he, mul_one]⟩), hd⟩⟩,
   λ ⟨hx0, d, hdu, hdx⟩, ⟨⟨d, hdx⟩, λ ⟨e, he⟩, hdu (is_unit_of_dvd_one _
@@ -367,6 +367,9 @@ iff.intro
   (assume h a, h _)
   (assume h a, quotient.induction_on a h)
 
+theorem mk_surjective [monoid α] : function.surjective (@associates.mk α _) :=
+forall_associated.2 (λ a, ⟨a, rfl⟩)
+
 instance [monoid α] : has_one (associates α) := ⟨⟦ 1 ⟧⟩
 
 theorem one_eq_mk_one [monoid α] : (1 : associates α) = associates.mk 1 := rfl
@@ -547,6 +550,55 @@ begin
   rw [mk_mul_mk, mk_dvd_mk, mk_dvd_mk, mk_dvd_mk],
 end
 
+theorem irreducible_mk (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
+begin
+  simp only [irreducible, is_unit_mk],
+  apply and_congr iff.rfl,
+  split,
+  { rintro h x y rfl,
+    simpa [is_unit_mk] using h (associates.mk x) (associates.mk y) rfl },
+  { intros h x y,
+    refine quotient.induction_on₂ x y (assume x y a_eq, _),
+    rcases quotient.exact a_eq.symm with ⟨u, a_eq⟩,
+    rw mul_assoc at a_eq,
+    show is_unit (associates.mk x) ∨ is_unit (associates.mk y),
+    simpa [is_unit_mk] using h _ _ a_eq.symm }
+end
+
+theorem mk_dvd_not_unit_mk_iff {a b : α} :
+  dvd_not_unit (associates.mk a) (associates.mk b) ↔
+  dvd_not_unit a b :=
+begin
+  rw [dvd_not_unit, dvd_not_unit, ne, ne, mk_eq_zero],
+  apply and_congr_right, intro ane0,
+  split,
+  { contrapose!, rw forall_associated,
+    intros h x hx hbax,
+    rw [mk_mul_mk, mk_eq_mk_iff_associated] at hbax,
+    cases hbax with u hu,
+    apply h (x * ↑u⁻¹),
+    { rw is_unit_mk at hx,
+      rw is_unit_iff_of_associated,
+      apply hx,
+      use u,
+      simp, },
+    simp [← mul_assoc, ← hu] },
+  { rintro ⟨x, ⟨hx, rfl⟩⟩,
+    use associates.mk x,
+    simp [is_unit_mk, mk_mul_mk, hx], }
+end
+
+theorem dvd_not_unit_of_lt {a b : associates α} (hlt : a < b) :
+  dvd_not_unit a b :=
+begin
+  split, { rintro rfl, apply not_lt_of_le _ hlt, apply dvd_zero },
+  rcases hlt with ⟨⟨x, rfl⟩, ndvd⟩,
+  refine ⟨x, _, rfl⟩,
+  contrapose! ndvd,
+  rcases ndvd with ⟨u, rfl⟩,
+  simp,
+end
+
 end comm_monoid_with_zero
 
 section comm_cancel_monoid_with_zero
@@ -579,27 +631,11 @@ theorem prod_eq_zero_iff [nontrivial α] {s : multiset (associates α)} :
 multiset.induction_on s (by simp) $
   assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
 
-theorem irreducible_mk_iff (a : α) : irreducible (associates.mk a) ↔ irreducible a :=
-begin
-  simp [irreducible, is_unit_mk],
-  apply and_congr iff.rfl,
-  split,
-  { assume h x y eq,
-    have : is_unit (associates.mk x) ∨ is_unit (associates.mk y),
-      from h _ _ (by rw [eq]; refl),
-    simpa [is_unit_mk] },
-  { refine assume h x y, quotient.induction_on₂ x y (assume x y eq, _),
-    rcases quotient.exact eq.symm with ⟨u, eq⟩,
-    have : a = x * (y * u), by rwa [mul_assoc, eq_comm] at eq,
-    show is_unit (associates.mk x) ∨ is_unit (associates.mk y),
-    simpa [is_unit_mk] using h _ _ this }
-end
-
 theorem irreducible_iff_prime_iff :
   (∀ a : α, irreducible a ↔ prime a) ↔ (∀ a : (associates α), irreducible a ↔ prime a) :=
 begin
   rw forall_associated, split;
-  intros h a; have ha := h a; rw irreducible_mk_iff at *; rw prime_mk at *; exact ha,
+  intros h a; have ha := h a; rw irreducible_mk at *; rw prime_mk at *; exact ha,
 end
 
 lemma eq_of_mul_eq_mul_left :
@@ -619,10 +655,6 @@ lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :
   a * b ≤ a * c → b ≤ c
 | ⟨d, hd⟩ := ⟨d, eq_of_mul_eq_mul_left a _ _ ha $ by rwa ← mul_assoc⟩
 
-lemma le_of_mul_le_mul_right (a b c : associates α) (hb : b ≠ 0) :
-  a * b ≤ c * b → a ≤ c :=
-(mul_comm b a) ▸ (mul_comm b c) ▸ (le_of_mul_le_mul_left b a c hb)
-
 lemma one_or_eq_of_le_of_prime :
   ∀(p m : associates α), prime p → m ≤ p → (m = 1 ∨ m = p)
 | _ m ⟨hp0, hp1, h⟩ ⟨d, rfl⟩ :=
@@ -644,6 +676,10 @@ instance : comm_cancel_monoid_with_zero (associates α) :=
   mul_right_cancel_of_ne_zero := eq_of_mul_eq_mul_right,
   .. (infer_instance : comm_monoid_with_zero (associates α)) }
 
+theorem dvd_not_unit_iff_lt {a b : associates α} :
+  dvd_not_unit a b ↔ a < b :=
+dvd_and_not_dvd_iff.symm
+
 end comm_cancel_monoid_with_zero
 
 end associates

src/algebra/divisibility.lean

@@ -222,3 +222,23 @@ by { rcases hu with ⟨u, rfl⟩, apply units.mul_left_dvd, }
 end comm_monoid
 
 end is_unit
+
+section comm_monoid_with_zero
+
+variable [comm_monoid_with_zero α]
+
+/-- `dvd_not_unit a b` expresses that `a` divides `b` "strictly", i.e. that `b` divided by `a` is not a unit. -/
+def dvd_not_unit (a b : α) : Prop := a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x
+
+lemma dvd_not_unit_of_dvd_of_not_dvd {a b : α} (hd : a ∣ b) (hnd : ¬ b ∣ a) :
+  dvd_not_unit a b :=
+begin
+  split,
+  { rintro rfl, exact hnd (dvd_zero _) },
+  { rcases hd with ⟨c, rfl⟩,
+    refine ⟨c, _, rfl⟩,
+    rintro ⟨u, rfl⟩,
+    simpa using hnd }
+end
+
+end comm_monoid_with_zero

src/field_theory/splitting_field.lean

@@ -130,7 +130,7 @@ lemma exists_root_of_splits {f : polynomial α} (hs : splits i f) (hf0 : degree
   ∃ x, eval₂ i x f = 0 :=
 if hf0 : f = 0 then ⟨37, by simp [hf0]⟩
 else
-  let ⟨g, hg⟩ := is_noetherian_ring.exists_irreducible_factor
+  let ⟨g, hg⟩ := wf_dvd_monoid.exists_irreducible_factor
     (show ¬ is_unit (f.map i), from mt is_unit_iff_degree_eq_zero.1 (by rwa degree_map))
     (map_ne_zero hf0) in
   let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0 hg.1 hg.2) in
@@ -143,7 +143,7 @@ lemma exists_multiset_of_splits {f : polynomial α} : splits i f →
 suffices splits (ring_hom.id _) (f.map i) → ∃ s : multiset β, f.map i =
   (C (f.map i).leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod,
 by rwa [splits_map_iff, leading_coeff_map i] at this,
-is_noetherian_ring.irreducible_induction_on (f.map i)
+wf_dvd_monoid.induction_on_irreducible (f.map i)
   (λ _, ⟨{37}, by simp [i.map_zero]⟩)
   (λ u hu _, ⟨0,
     by conv_lhs { rw eq_C_of_degree_eq_zero (is_unit_iff_degree_eq_zero.1 hu) };
@@ -328,8 +328,8 @@ end
 theorem factor_dvd_of_not_is_unit {f : polynomial α} (hf1 : ¬is_unit f) : factor f ∣ f :=
 begin
   by_cases hf2 : f = 0, { rw hf2, exact dvd_zero _ },
-  rw [factor, dif_pos (is_noetherian_ring.exists_irreducible_factor hf1 hf2)],
-  exact (classical.some_spec $ is_noetherian_ring.exists_irreducible_factor hf1 hf2).2
+  rw [factor, dif_pos (wf_dvd_monoid.exists_irreducible_factor hf1 hf2)],
+  exact (classical.some_spec $ wf_dvd_monoid.exists_irreducible_factor hf1 hf2).2
 end
 
 theorem factor_dvd_of_degree_ne_zero {f : polynomial α} (hf : f.degree ≠ 0) : factor f ∣ f :=

src/ring_theory/ideal/basic.lean

@@ -255,7 +255,7 @@ theorem mem_span_pair {x y z : α} :
 by simp [mem_span_insert, mem_span_singleton', @eq_comm _ _ z]
 
 lemma span_singleton_lt_span_singleton [integral_domain β] {x y : β} :
-  span ({x} : set β) < span ({y} : set β) ↔ y ≠ 0 ∧ ∃ d : β, ¬ is_unit d ∧ x = y * d :=
+  span ({x} : set β) < span ({y} : set β) ↔ dvd_not_unit y x :=
 by rw [lt_iff_le_not_le, span_singleton_le_span_singleton, span_singleton_le_span_singleton,
   dvd_and_not_dvd_iff]
 

src/ring_theory/noetherian.lean

@@ -451,56 +451,6 @@ theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
   (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=
 is_noetherian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective
 
-namespace is_noetherian_ring
-
-variables {R : Type*} [integral_domain R] [is_noetherian_ring R]
-open associates nat
-
-local attribute [elab_as_eliminator] well_founded.fix
-
-lemma well_founded_dvd_not_unit : well_founded (λ a b : R, a ≠ 0 ∧ ∃ x, ¬is_unit x ∧ b = a * x) :=
-by simp only [ideal.span_singleton_lt_span_singleton.symm];
-   exact inv_image.wf (λ a, ideal.span ({a} : set R)) (well_founded_submodule_gt _ _)
-
-lemma exists_irreducible_factor {a : R} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
-  ∃ i, irreducible i ∧ i ∣ a :=
-(irreducible_or_factor a ha).elim (λ hai, ⟨a, hai, dvd_refl _⟩)
-  (well_founded.fix
-    well_founded_dvd_not_unit
-    (λ a ih ha ha0 ⟨x, y, hx, hy, hxy⟩,
-      have hx0 : x ≠ 0, from λ hx0, ha0 (by rw [← hxy, hx0, zero_mul]),
-      (irreducible_or_factor x hx).elim
-        (λ hxi, ⟨x, hxi, hxy ▸ by simp⟩)
-        (λ hxf, let ⟨i, hi⟩ := ih x ⟨hx0, y, hy, hxy.symm⟩ hx hx0 hxf in
-          ⟨i, hi.1, dvd.trans hi.2 (hxy ▸ by simp)⟩)) a ha ha0)
-
-@[elab_as_eliminator] lemma irreducible_induction_on {P : R → Prop} (a : R)
-  (h0 : P 0) (hu : ∀ u : R, is_unit u → P u)
-  (hi : ∀ a i : R, a ≠ 0 → irreducible i → P a → P (i * a)) :
-  P a :=
-by haveI := classical.dec; exact
-well_founded.fix well_founded_dvd_not_unit
-  (λ a ih, if ha0 : a = 0 then ha0.symm ▸ h0
-    else if hau : is_unit a then hu a hau
-    else let ⟨i, hii, ⟨b, hb⟩⟩ := exists_irreducible_factor hau ha0 in
-      have hb0 : b ≠ 0, from λ hb0, by simp * at *,
-      hb.symm ▸ hi _ _ hb0 hii (ih _ ⟨hb0, i,
-        hii.1, by rw [hb, mul_comm]⟩))
-  a
-
-lemma exists_factors (a : R) : a ≠ 0 →
-  ∃f : multiset R, (∀b ∈ f, irreducible b) ∧ associated a f.prod :=
-is_noetherian_ring.irreducible_induction_on a
-  (λ h, (h rfl).elim)
-  (λ u hu _, ⟨0, by simp [associated_one_iff_is_unit, hu]⟩)
-  (λ a i ha0 hii ih hia0,
-    let ⟨s, hs⟩ := ih ha0 in
-    ⟨i::s, ⟨by clear _let_match; finish,
-      by rw multiset.prod_cons;
-        exact associated_mul_mul (by refl) hs.2⟩⟩)
-
-end is_noetherian_ring
-
 namespace submodule
 variables {R : Type*} {A : Type*} [comm_ring R] [ring A] [algebra R A]
 variables (M N : submodule R A)

src/ring_theory/polynomial/basic.lean

@@ -413,7 +413,7 @@ namespace polynomial
 
 theorem exists_irreducible_of_degree_pos {R : Type u} [integral_domain R] [is_noetherian_ring R]
   {f : polynomial R} (hf : 0 < f.degree) : ∃ g, irreducible g ∧ g ∣ f :=
-is_noetherian_ring.exists_irreducible_factor
+wf_dvd_monoid.exists_irreducible_factor
   (λ huf, ne_of_gt hf $ degree_eq_zero_of_is_unit huf)
   (λ hf0, not_lt_of_lt hf $ hf0.symm ▸ (@degree_zero R _).symm ▸ with_bot.bot_lt_coe _)
 

src/ring_theory/principal_ideal_domain.lean

@@ -163,15 +163,13 @@ open_locale classical
 
 /-- `factors a` is a multiset of irreducible elements whose product is `a`, up to units -/
 noncomputable def factors (a : R) : multiset R :=
-if h : a = 0 then ∅ else classical.some
-  (is_noetherian_ring.exists_factors a h)
+if h : a = 0 then ∅ else classical.some (wf_dvd_monoid.exists_factors a h)
 
 lemma factors_spec (a : R) (h : a ≠ 0) :
   (∀b∈factors a, irreducible b) ∧ associated a (factors a).prod :=
 begin
   unfold factors, rw [dif_neg h],
-  exact classical.some_spec
-    (is_noetherian_ring.exists_factors a h)
+  exact classical.some_spec (wf_dvd_monoid.exists_factors a h)
 end
 
 lemma ne_zero_of_mem_factors {R : Type v} [integral_domain R] [is_principal_ideal_ring R] {a b : R}