refactor(algebra/divisibility, associated): generalize instances in d…

…ivisibility, associated (#3714)

generalizes the divisibility relation to noncommutative monoids
adds missing headers to algebra/divisibility
generalizes the instances in many of the lemmas in algebra/associated
reunites (some of the) divisibility API for ordinals with general monoids



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

src/algebra/associated.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 -/
 import data.multiset.basic
+import algebra.divisibility
 
 /-!
 # Associated, prime, and irreducible elements.
@@ -14,36 +15,23 @@ variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 lemma is_unit_pow [monoid α] {a : α} (n : ℕ) : is_unit a → is_unit (a ^ n) :=
 λ ⟨u, hu⟩, ⟨u ^ n, by simp *⟩
 
-theorem is_unit_iff_dvd_one [comm_semiring α] {x : α} : is_unit x ↔ x ∣ 1 :=
+theorem is_unit_iff_dvd_one [comm_monoid α] {x : α} : is_unit x ↔ x ∣ 1 :=
 ⟨by rintro ⟨u, rfl⟩; exact ⟨_, u.mul_inv.symm⟩,
  λ ⟨y, h⟩, ⟨⟨x, y, h.symm, by rw [h, mul_comm]⟩, rfl⟩⟩
 
-theorem is_unit_iff_forall_dvd [comm_semiring α] {x : α} :
+theorem is_unit_iff_forall_dvd [comm_monoid α] {x : α} :
   is_unit x ↔ ∀ y, x ∣ y :=
 is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
 
-theorem mul_dvd_of_is_unit_left [comm_semiring α] {x y z : α} (h : is_unit x) : x * y ∣ z ↔ y ∣ z :=
-⟨dvd_trans (dvd_mul_left _ _),
- dvd_trans $ by simpa using mul_dvd_mul_right (is_unit_iff_dvd_one.1 h) y⟩
-
-theorem mul_dvd_of_is_unit_right [comm_semiring α] {x y z : α} (h : is_unit y) : x * y ∣ z ↔ x ∣ z :=
-by rw [mul_comm, mul_dvd_of_is_unit_left h]
-
-@[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
-mul_dvd_of_is_unit_left (is_unit_unit _)
-
-lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
-units.coe_mul_dvd _ _ _
-
-theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
+theorem is_unit_of_dvd_unit {α} [comm_monoid α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
 
 theorem is_unit_int {n : ℤ} : is_unit n ↔ n.nat_abs = 1 :=
 ⟨begin rintro ⟨u, rfl⟩, exact (int.units_eq_one_or u).elim (by simp) (by simp) end,
   λ h, is_unit_iff_dvd_one.2 ⟨n, by rw [← int.nat_abs_mul_self, h]; refl⟩⟩
 
-lemma is_unit_of_dvd_one [comm_semiring α] : ∀a ∣ 1, is_unit (a:α)
+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 [integral_domain α] {x y : α} :
@@ -58,29 +46,33 @@ lemma pow_dvd_pow_iff [integral_domain α] {x : α} {n m : ℕ} (h0 : x ≠ 0) (
 begin
   split,
   { intro h, rw [← not_lt], intro hmn, apply h1,
-    have : x * x ^ m ∣ 1 * x ^ m,
-    { rw [← pow_succ, one_mul], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
-    rwa [mul_dvd_mul_iff_right, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
+    have : x ^ m * x ∣ x ^ m * 1,
+    { rw [← pow_succ', mul_one], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
+    rwa [mul_dvd_mul_iff_left, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
   { apply pow_dvd_pow }
 end
 
-/-- prime element of a semiring -/
-def prime [comm_semiring α] (p : α) : Prop :=
+section prime
+variables [comm_monoid_with_zero α]
+
+/-- prime element of a `comm_monoid_with_zero` -/
+def prime (p : α) : Prop :=
 p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
 
 namespace prime
+variables {p : α} (hp : prime p)
 
-lemma ne_zero [comm_semiring α] {p : α} (hp : prime p) : p ≠ 0 :=
+lemma ne_zero (hp : prime p) : p ≠ 0 :=
 hp.1
 
-lemma not_unit [comm_semiring α] {p : α} (hp : prime p) : ¬ is_unit p :=
+lemma not_unit (hp : prime p) : ¬ is_unit p :=
 hp.2.1
 
-lemma div_or_div [comm_semiring α] {p : α} (hp : prime p) {a b : α} (h : p ∣ a * b) :
+lemma div_or_div (hp : prime p) {a b : α} (h : p ∣ a * b) :
   p ∣ a ∨ p ∣ b :=
 hp.2.2 a b h
 
-lemma dvd_of_dvd_pow [comm_semiring α] {p : α} (hp : prime p) {a : α} {n : ℕ} (h : p ∣ a^n) :
+lemma dvd_of_dvd_pow (hp : prime p) {a : α} {n : ℕ} (h : p ∣ a^n) :
   p ∣ a :=
 begin
   induction n with n ih,
@@ -96,13 +88,13 @@ end
 
 end prime
 
-@[simp] lemma not_prime_zero [comm_semiring α] : ¬ prime (0 : α) :=
+@[simp] lemma not_prime_zero : ¬ prime (0 : α) :=
 λ h, h.ne_zero rfl
 
-@[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
+@[simp] lemma not_prime_one : ¬ prime (1 : α) :=
 λ h, h.not_unit is_unit_one
 
-lemma exists_mem_multiset_dvd_of_prime [comm_semiring α] {s : multiset α} {p : α} (hp : prime p) :
+lemma exists_mem_multiset_dvd_of_prime {s : multiset α} {p : α} (hp : prime p) :
   p ∣ s.prod → ∃a∈s, p ∣ a :=
 multiset.induction_on s (assume h, (hp.not_unit $ is_unit_of_dvd_one _ h).elim) $
 assume a s ih h,
@@ -112,6 +104,8 @@ assume a s ih h,
   | or.inr h := let ⟨a, has, h⟩ := ih h in ⟨a, multiset.mem_cons_of_mem has, h⟩
   end
 
+end prime
+
 /-- `irreducible p` states that `p` is non-unit and only factors into units.
 
 We explicitly avoid stating that `p` is non-zero, this would require a semiring. Assuming only a
@@ -134,11 +128,11 @@ end irreducible
 @[simp] theorem not_irreducible_one [monoid α] : ¬ irreducible (1 : α) :=
 by simp [irreducible]
 
-@[simp] theorem not_irreducible_zero [semiring α] : ¬ irreducible (0 : α)
+@[simp] theorem not_irreducible_zero [monoid_with_zero α] : ¬ irreducible (0 : α)
 | ⟨hn0, h⟩ := have is_unit (0:α) ∨ is_unit (0:α), from h 0 0 ((mul_zero 0).symm),
   this.elim hn0 hn0
 
-theorem irreducible.ne_zero [semiring α] : ∀ {p:α}, irreducible p → p ≠ 0
+theorem irreducible.ne_zero [monoid_with_zero α] : ∀ {p:α}, irreducible p → p ≠ 0
 | _ hp rfl := not_irreducible_zero hp
 
 theorem of_irreducible_mul {α} [monoid α] {x y : α} :
@@ -179,17 +173,15 @@ have hpd : p ∣ x * y, from ⟨z, by rwa [mul_right_inj' hp0] at h⟩,
   (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
 /-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`. -/
-lemma dvd_symm_of_irreducible [comm_semiring α] {p q : α}
+lemma dvd_symm_of_irreducible [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q → q ∣ p :=
 begin
   tactic.unfreeze_local_instances,
   rintros ⟨q', rfl⟩,
-  exact is_unit.mul_right_dvd_of_dvd
-    (or.resolve_left (of_irreducible_mul hq) hp.not_unit)
-    (dvd_refl p)
+  rw is_unit.mul_right_dvd (or.resolve_left (of_irreducible_mul hq) hp.not_unit),
 end
 
-lemma dvd_symm_iff_of_irreducible [comm_semiring α] {p q : α}
+lemma dvd_symm_iff_of_irreducible [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q ↔ q ∣ p :=
 ⟨dvd_symm_of_irreducible hp hq, dvd_symm_of_irreducible hq hp⟩
 
@@ -239,25 +231,28 @@ lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
   a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
 
-lemma dvd_of_associated [comm_ring α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
+lemma dvd_of_associated [monoid α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
 
-lemma dvd_dvd_of_associated [comm_ring α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
+lemma dvd_dvd_of_associated [monoid α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
 ⟨dvd_of_associated h, dvd_of_associated h.symm⟩
 
-theorem associated_of_dvd_dvd [integral_domain α] {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
+theorem associated_of_dvd_dvd [cancel_monoid_with_zero α]
+  {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
 begin
-  haveI := classical.dec_eq α,
   rcases hab with ⟨c, rfl⟩,
   rcases hba with ⟨d, a_eq⟩,
   by_cases ha0 : a = 0,
   { simp [*] at * },
-  have : a * 1 = a * (c * d),
-  { simpa [mul_assoc] using a_eq },
-  have : 1 = (c * d), from mul_left_cancel' ha0 this,
-  exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
+  have hac0 : a * c ≠ 0,
+  { intro con, rw [con, zero_mul] at a_eq, apply ha0 a_eq, },
+  have : a * (c * d) =  a * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
+  have hcd : (c * d) = 1, from mul_left_cancel' ha0 this,
+  have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one],
+  have hdc : d * c = 1, from mul_left_cancel' hac0 this,
+  exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
 end
 
-theorem dvd_dvd_iff_associated [integral_domain α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
+theorem dvd_dvd_iff_associated [cancel_monoid_with_zero α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
 ⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, dvd_dvd_of_associated⟩
 
 lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
@@ -275,14 +270,11 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
   end)
 
-lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
-let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
-
-lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
-units.dvd_coe_mul _ _ _
+lemma dvd_iff_dvd_of_rel_left [comm_monoid_with_zero α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
+let ⟨u, hu⟩ := h in hu ▸ units.mul_right_dvd.symm
 
 lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
-let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm
+let ⟨u, hu⟩ := h in hu ▸ units.dvd_mul_right.symm
 
 lemma eq_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
 ⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
@@ -295,7 +287,7 @@ lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : pri
 ⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
     ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
-      hu ▸ by { simp [mul_unit_dvd_iff], intros a b, exact hp.div_or_div }⟩⟩
+      hu ▸ by { simp [units.mul_right_dvd], intros a b, exact hp.div_or_div }⟩⟩
 
 lemma prime_iff_of_associated [comm_semiring α] {p q : α}
   (h : p ~ᵤ q) : prime p ↔ prime q :=
@@ -386,11 +378,9 @@ instance : comm_monoid (associates α) :=
     assume a b, show ⟦a * b⟧ = ⟦b * a⟧, by rw [mul_comm] }
 
 instance : preorder (associates α) :=
-{ le := λa b, ∃c, a * c = b,
-  le_refl := assume a, ⟨1, by simp⟩,
-  le_trans := assume a b c ⟨f₁, h₁⟩ ⟨f₂, h₂⟩, ⟨f₁ * f₂, h₂ ▸ h₁ ▸ (mul_assoc _ _ _).symm⟩}
-
-instance : has_dvd (associates α) := ⟨(≤)⟩
+{ le := has_dvd.dvd,
+  le_refl := dvd_refl,
+  le_trans := λ a b c, dvd_trans}
 
 @[simp] lemma mk_one : associates.mk (1 : α) = 1 := rfl
 
@@ -439,10 +429,10 @@ section order
 theorem mul_mono {a b c d : associates α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
   a * c ≤ b * d :=
 let ⟨x, hx⟩ := h₁, ⟨y, hy⟩ := h₂ in
-⟨x * y, by simp [hx.symm, hy.symm, mul_comm, mul_assoc, mul_left_comm]⟩
+⟨x * y, by simp [hx, hy, mul_comm, mul_assoc, mul_left_comm]⟩
 
 theorem one_le {a : associates α} : 1 ≤ a :=
-⟨a, one_mul a⟩
+dvd.intro _ (one_mul a)
 
 theorem prod_le_prod {p q : multiset (associates α)} (h : p ≤ q) : p.prod ≤ q.prod :=
 begin
@@ -493,9 +483,9 @@ variables [comm_semiring α]
 theorem dvd_of_mk_le_mk {a b : α} : associates.mk a ≤ associates.mk b → a ∣ b
 | ⟨c', hc'⟩ := (quotient.induction_on c' $ assume c hc,
     let ⟨d, hd⟩ := (quotient.exact hc).symm in
-    ⟨(↑d⁻¹) * c,
-      calc b = (a * c) * ↑d⁻¹ : by rw [← hd, mul_assoc, units.mul_inv, mul_one]
-        ... = a * (↑d⁻¹ * c) : by ac_refl⟩) hc'
+    ⟨(↑d) * c,
+      calc b = (a * c) * ↑d : hd.symm
+        ... = a * (↑d * c) : by ac_refl⟩) hc'
 
 theorem mk_le_mk_of_dvd {a b : α} : a ∣ b → associates.mk a ≤ associates.mk b :=
 assume ⟨c, hc⟩, ⟨associates.mk c, by simp [hc]; refl⟩
@@ -518,7 +508,7 @@ hp.2.2 a b h
 lemma exists_mem_multiset_le_of_prime {s : multiset (associates α)} {p : associates α}
   (hp : prime p) :
   p ≤ s.prod → ∃a∈s, p ≤ a :=
-multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq).1).elim) $
+multiset.induction_on s (assume ⟨d, eq⟩, (hp.ne_one (mul_eq_one_iff.1 eq.symm).1).elim) $
 assume a s ih h,
   have p ≤ a * s.prod, by simpa using h,
   match hp.le_or_le this with
@@ -549,13 +539,8 @@ section integral_domain
 variable [integral_domain α]
 
 instance : partial_order (associates α) :=
-{ le_antisymm := assume a' b',
-    quotient.induction_on₂ a' b' $ assume a b ⟨f₁', h₁⟩ ⟨f₂', h₂⟩,
-    (quotient.induction_on₂ f₁' f₂' $ assume f₁ f₂ h₁ h₂,
-      let ⟨c₁, h₁⟩ := quotient.exact h₁, ⟨c₂, h₂⟩ := quotient.exact h₂ in
-      quotient.sound $ associated_of_dvd_dvd
-        (h₁ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)
-        (h₂ ▸ dvd_mul_of_dvd_left (dvd_mul_right _ _) _)) h₁ h₂
+{ le_antisymm := λ a' b', quotient.induction_on₂ a' b' (λ a b hab hba,
+  quot.sound $ associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba))
   .. associates.preorder }
 
 instance : order_bot (associates α) :=
@@ -565,7 +550,7 @@ instance : order_bot (associates α) :=
 
 instance : order_top (associates α) :=
 { top := 0,
-  le_top := assume a, ⟨0, mul_zero a⟩,
+  le_top := assume a, ⟨0, (mul_zero a).symm⟩,
   .. associates.partial_order }
 
 instance : no_zero_divisors (associates α) :=