feat(ring_theory/euclidean_domain): generalize lemmas to PIDs (#10324)

This moves the existing lemmas to the `euclidean_domain` namespace.

src/data/polynomial/field_division.lean

@@ -267,7 +267,7 @@ root_gcd_iff_root_left_right
 
 theorem is_coprime_map [field k] (f : R →+* k) :
   is_coprime (p.map f) (q.map f) ↔ is_coprime p q :=
-by rw [← gcd_is_unit_iff, ← gcd_is_unit_iff, gcd_map, is_unit_map]
+by rw [← euclidean_domain.gcd_is_unit_iff, ← euclidean_domain.gcd_is_unit_iff, gcd_map, is_unit_map]
 
 @[simp] lemma map_eq_zero [semiring S] [nontrivial S] (f : R →+* S) :
   p.map f = 0 ↔ p = 0 :=
@@ -413,7 +413,7 @@ lemma is_coprime_of_is_root_of_eval_derivative_ne_zero {K : Type*} [field K]
   (f : polynomial K) (a : K) (hf' : f.derivative.eval a ≠ 0) :
   is_coprime (X - C a : polynomial K) (f /ₘ (X - C a)) :=
 begin
-  refine or.resolve_left (dvd_or_coprime (X - C a) (f /ₘ (X - C a))
+  refine or.resolve_left (euclidean_domain.dvd_or_coprime (X - C a) (f /ₘ (X - C a))
     (irreducible_of_degree_eq_one (polynomial.degree_X_sub_C a))) _,
   contrapose! hf' with h,
   have key : (X - C a) * (f /ₘ (X - C a)) = f - (f %ₘ (X - C a)),

src/field_theory/separable.lean

@@ -448,7 +448,7 @@ variables {F : Type u} [field F] {K : Type v} [field K]
 theorem separable_iff_derivative_ne_zero {f : polynomial F} (hf : irreducible f) :
   f.separable ↔ f.derivative ≠ 0 :=
 ⟨λ h1 h2, hf.not_unit $ is_coprime_zero_right.1 $ h2 ▸ h1,
-λ h, is_coprime_of_dvd (mt and.right h) $ λ g hg1 hg2 ⟨p, hg3⟩ hg4,
+λ h, euclidean_domain.is_coprime_of_dvd (mt and.right h) $ λ g hg1 hg2 ⟨p, hg3⟩ hg4,
 let ⟨u, hu⟩ := (hf.is_unit_or_is_unit hg3).resolve_left hg1 in
 have f ∣ f.derivative, by { conv_lhs { rw [hg3, ← hu] }, rwa units.mul_right_dvd },
 not_lt_of_le (nat_degree_le_of_dvd this h) $ nat_degree_derivative_lt h⟩

src/ring_theory/euclidean_domain.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro, Chris Hughes
 import algebra.gcd_monoid.basic
 import ring_theory.coprime.basic
 import ring_theory.ideal.basic
+import ring_theory.principal_ideal_domain
 
 /-!
 # Lemmas about Euclidean domains
@@ -27,8 +28,6 @@ section gcd_monoid
 
 variables {R : Type*} [euclidean_domain R] [gcd_monoid R]
 
-open gcd_monoid
-
 lemma left_div_gcd_ne_zero {p q : R} (hp : p ≠ 0) :
   p / gcd_monoid.gcd p q ≠ 0 :=
 begin
@@ -49,50 +48,50 @@ end
 
 end gcd_monoid
 
+namespace euclidean_domain
+
+/-- Create a `gcd_monoid` whose `gcd_monoid.gcd` matches `euclidean_domain.gcd`. -/
+def gcd_monoid (R) [euclidean_domain R] : gcd_monoid R :=
+{ gcd := gcd,
+  lcm := lcm,
+  gcd_dvd_left := gcd_dvd_left,
+  gcd_dvd_right := gcd_dvd_right,
+  dvd_gcd := λ a b c, dvd_gcd,
+  gcd_mul_lcm := λ a b, by rw euclidean_domain.gcd_mul_lcm,
+  lcm_zero_left := lcm_zero_left,
+  lcm_zero_right := lcm_zero_right }
+
 variables {α : Type*} [euclidean_domain α] [decidable_eq α]
 
 theorem span_gcd {α} [euclidean_domain α] (x y : α) :
   span ({gcd x y} : set α) = span ({x, y} : set α) :=
 begin
-  apply le_antisymm,
-  { refine span_le.2 (λ x, _),
-    simp only [set.mem_singleton_iff, set_like.mem_coe, mem_span_pair],
-    rintro rfl,
-    exact ⟨gcd_a x y, gcd_b x y, by simp [gcd_eq_gcd_ab, mul_comm]⟩ },
-  { assume z ,
-    simp [mem_span_singleton, euclidean_domain.gcd_dvd_left, mem_span_pair,
-      @eq_comm _ _ z] {contextual := tt},
-    exact λ a b _, dvd_add ((gcd_dvd_left x y).mul_left _)
-      ((gcd_dvd_right x y).mul_left _) }
+  letI := euclidean_domain.gcd_monoid α,
+  exact span_gcd x y,
 end
--- this should be proved for PIDs?
+
 theorem gcd_is_unit_iff {α} [euclidean_domain α] {x y : α} :
   is_unit (gcd x y) ↔ is_coprime x y :=
-⟨λ h, let ⟨b, hb⟩ := is_unit_iff_exists_inv'.1 h in ⟨b * gcd_a x y, b * gcd_b x y,
-  by rw [← hb, gcd_eq_gcd_ab, mul_comm x, mul_comm y, mul_add, mul_assoc, mul_assoc]⟩,
-λ ⟨a, b, h⟩, is_unit_iff_dvd_one.2 $ h ▸ dvd_add ((gcd_dvd_left x y).mul_left _)
-  ((gcd_dvd_right x y).mul_left _)⟩
+begin
+  letI := euclidean_domain.gcd_monoid α,
+  exact gcd_is_unit_iff x y,
+end
 
 -- this should be proved for UFDs surely?
 theorem is_coprime_of_dvd {α} [euclidean_domain α] {x y : α}
   (z : ¬ (x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬ z ∣ y) :
   is_coprime x y :=
 begin
-  rw [← gcd_is_unit_iff],
-  by_contra h,
-  refine H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _),
-  rwa [ne, euclidean_domain.gcd_eq_zero_iff]
+  letI := euclidean_domain.gcd_monoid α,
+  exact is_coprime_of_dvd x y z H,
 end
 
 -- this should be proved for UFDs surely?
 theorem dvd_or_coprime {α} [euclidean_domain α] (x y : α)
   (h : irreducible x) : x ∣ y ∨ is_coprime x y :=
 begin
-  refine or_iff_not_imp_left.2 (λ h', _),
-  apply is_coprime_of_dvd,
-  { unfreezingI { rintro ⟨rfl, rfl⟩ }, simpa using h },
-  { unfreezingI { rintro z nu nz ⟨w, rfl⟩ dy },
-    refine h' (dvd_trans _ dy),
-    simpa using mul_dvd_mul_left z (is_unit_iff_dvd_one.1 $
-      (of_irreducible_mul h).resolve_left nu) }
+  letI := euclidean_domain.gcd_monoid α,
+  exact dvd_or_coprime x y h,
 end
+
+end euclidean_domain

src/ring_theory/principal_ideal_domain.lean

@@ -289,3 +289,57 @@ lemma is_principal_ideal_ring.of_surjective [is_principal_ideal_ring R]
 ⟨λ I, ideal.is_principal.of_comap f hf I⟩
 
 end surjective
+
+section
+open ideal
+variables [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [gcd_monoid R]
+
+theorem span_gcd (x y : R) : span ({gcd x y} : set R) = span ({x, y} : set R) :=
+begin
+  obtain ⟨d, hd⟩ := is_principal_ideal_ring.principal (span ({x, y} : set R)),
+  rw submodule_span_eq at hd,
+  rw [hd],
+  suffices : associated d (gcd x y),
+  { obtain ⟨D, HD⟩ := this,
+    rw ←HD,
+    exact (span_singleton_mul_right_unit D.is_unit _) },
+  apply associated_of_dvd_dvd,
+  { rw dvd_gcd_iff,
+    split; rw [←ideal.mem_span_singleton, ←hd, mem_span_pair],
+    { use [1, 0],
+      rw [one_mul, zero_mul, add_zero] },
+    { use [0, 1],
+      rw [one_mul, zero_mul, zero_add] } },
+  { obtain ⟨r, s, rfl⟩ : ∃ r s, r * x + s * y = d,
+    { rw [←mem_span_pair, hd, ideal.mem_span_singleton] },
+    apply dvd_add; apply dvd_mul_of_dvd_right,
+    exacts [gcd_dvd_left x y, gcd_dvd_right x y] },
+end
+
+theorem gcd_is_unit_iff (x y : R) : is_unit (gcd x y) ↔ is_coprime x y :=
+by rw [is_coprime, ←mem_span_pair, ←span_gcd, ←span_singleton_eq_top, eq_top_iff_one]
+
+-- this should be proved for UFDs surely?
+theorem is_coprime_of_dvd (x y : R)
+  (z : ¬ (x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬ z ∣ y) :
+  is_coprime x y :=
+begin
+  rw [← gcd_is_unit_iff],
+  by_contra h,
+  refine H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _),
+  rwa [ne, gcd_eq_zero_iff]
+end
+
+-- this should be proved for UFDs surely?
+theorem dvd_or_coprime (x y : R) (h : irreducible x) : x ∣ y ∨ is_coprime x y :=
+begin
+  refine or_iff_not_imp_left.2 (λ h', _),
+  apply is_coprime_of_dvd,
+  { unfreezingI { rintro ⟨rfl, rfl⟩ }, simpa using h },
+  { unfreezingI { rintro z nu nz ⟨w, rfl⟩ dy },
+    refine h' (dvd_trans _ dy),
+    simpa using mul_dvd_mul_left z (is_unit_iff_dvd_one.1 $
+      (of_irreducible_mul h).resolve_left nu) }
+end
+
+end