feat(algebra/gcd_monoid): extract gcd from multiset/finset (#17316)

+ `multiset.extract_gcd` / `finset.extract_gcd`: extract the gcd as a common factor from a nonempty multiset/finset in a `normalized_gcd_monoid`, so that the gcd of remaining factors is 1.

+ We prove these by induction, which require the more precise version of the two-element case `_root_.extract_gcd` with `d := gcd a b`.

inspired by #16838



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

src/algebra/gcd_monoid/basic.lean

@@ -63,9 +63,6 @@ divisibility, gcd, lcm, normalize
 
 variables {α : Type*}
 
-
-
-
 /-- Normalization monoid: multiplying with `norm_unit` gives a normal form for associated
 elements. -/
 @[protect_proj] class normalization_monoid (α : Type*)
@@ -559,15 +556,15 @@ begin
 end
 
 lemma extract_gcd {α : Type*} [cancel_comm_monoid_with_zero α] [gcd_monoid α] (x y : α) :
-  ∃ x' y' d : α, x = d * x' ∧ y = d * y' ∧ is_unit (gcd x' y') :=
+  ∃ x' y', x = gcd x y * x' ∧ y = gcd x y * y' ∧ is_unit (gcd x' y') :=
 begin
-  cases eq_or_ne (gcd x y) 0 with h h,
+  by_cases h : gcd x y = 0,
   { obtain ⟨rfl, rfl⟩ := (gcd_eq_zero_iff x y).1 h,
     simp_rw ← associated_one_iff_is_unit,
-    exact ⟨1, 1, 0, (zero_mul 1).symm, (zero_mul 1).symm, gcd_one_left' 1⟩ },
+    exact ⟨1, 1, by rw [h, zero_mul], by rw [h, zero_mul], gcd_one_left' 1⟩ },
   obtain ⟨x', ex⟩ := gcd_dvd_left x y,
   obtain ⟨y', ey⟩ := gcd_dvd_right x y,
-  exact ⟨x', y', gcd x y, ex, ey, is_unit_gcd_of_eq_mul_gcd ex ey h⟩,
+  exact ⟨x', y', ex, ey, is_unit_gcd_of_eq_mul_gcd ex ey h⟩,
 end
 
 end gcd

src/algebra/gcd_monoid/finset.lean

@@ -208,6 +208,25 @@ begin
   apply ((normalize_associated a).mul_left _).gcd_eq_right
 end
 
+lemma extract_gcd' (f g : β → α) (hs : ∃ x, x ∈ s ∧ f x ≠ 0)
+  (hg : ∀ b ∈ s, f b = s.gcd f * g b) : s.gcd g = 1 :=
+((@mul_right_eq_self₀ _ _ (s.gcd f) _).1 $
+  by conv_lhs { rw [← normalize_gcd, ← gcd_mul_left, ← gcd_congr rfl hg] }).resolve_right $
+  by {contrapose! hs, exact gcd_eq_zero_iff.1 hs}
+
+lemma extract_gcd (f : β → α) (hs : s.nonempty) :
+  ∃ g : β → α, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1 :=
+begin
+  classical,
+  by_cases h : ∀ x ∈ s, f x = (0 : α),
+  { refine ⟨λ b, 1, λ b hb, by rw [h b hb, gcd_eq_zero_iff.2 h, mul_one], _⟩,
+    rw [gcd_eq_gcd_image, image_const hs, gcd_singleton, id, normalize_one] },
+  { choose g' hg using @gcd_dvd _ _ _ _ s f,
+    have := λ b hb, _, push_neg at h,
+    refine ⟨λ b, if hb : b ∈ s then g' hb else 0, this, extract_gcd' f _ h this⟩,
+    rw [dif_pos hb, hg hb] },
+end
+
 end gcd
 end finset
 

src/algebra/gcd_monoid/integrally_closed.lean

@@ -22,11 +22,12 @@ lemma is_localization.surj_of_gcd_domain (M : submonoid R) [is_localization M A]
   ∃ a b : R, is_unit (gcd a b) ∧ z * algebra_map R A b = algebra_map R A a :=
 begin
   obtain ⟨x, ⟨y, hy⟩, rfl⟩ := is_localization.mk'_surjective M z,
-  obtain ⟨x', y', d, rfl, rfl, hu⟩ := extract_gcd x y,
+  obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y,
   use [x', y', hu],
   rw [mul_comm, is_localization.mul_mk'_eq_mk'_of_mul],
   convert is_localization.mk'_mul_cancel_left _ _ using 2,
-  { rw [← mul_assoc, mul_comm y'], refl }, { apply_instance },
+  { rw [subtype.coe_mk, hy', ← mul_comm y', mul_assoc], conv_lhs { rw hx' } },
+  { apply_instance },
 end
 
 @[priority 100]

src/algebra/gcd_monoid/multiset.lean

@@ -134,6 +134,17 @@ begin
     simp [h a (mem_cons_self a s), sgcd (λ x hx, h x (mem_cons_of_mem hx))] }
 end
 
+lemma gcd_map_mul (a : α) (s : multiset α) :
+  (s.map ((*) a)).gcd = normalize a * s.gcd :=
+begin
+  refine s.induction_on _ (λ b s ih, _),
+  { simp_rw [map_zero, gcd_zero, mul_zero] },
+  { simp_rw [map_cons, gcd_cons, ← gcd_mul_left], rw ih,
+    apply ((normalize_associated a).mul_right _).gcd_eq_right },
+end
+
+section
+
 variables [decidable_eq α]
 
 @[simp] lemma gcd_dedup (s : multiset α) : (dedup s).gcd = s.gcd :=
@@ -156,6 +167,29 @@ by { rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_add], simp }
   (ndinsert a s).gcd = gcd_monoid.gcd a s.gcd :=
 by { rw [← gcd_dedup, dedup_ext.2, gcd_dedup, gcd_cons], simp }
 
+end
+
+lemma extract_gcd' (s t : multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α))
+  (ht : s = t.map ((*) s.gcd)) : t.gcd = 1 :=
+((@mul_right_eq_self₀ _ _ s.gcd _).1 $ by conv_lhs { rw [← normalize_gcd, ← gcd_map_mul, ← ht] })
+  .resolve_right $ by { contrapose! hs, exact s.gcd_eq_zero_iff.1 hs }
+
+lemma extract_gcd (s : multiset α) (hs : s ≠ 0) :
+  ∃ t : multiset α, s = t.map ((*) s.gcd) ∧ t.gcd = 1 :=
+begin
+  classical,
+  by_cases h : ∀ x ∈ s, x = (0 : α),
+  { use repeat 1 s.card,
+    rw [map_repeat, eq_repeat, mul_one, s.gcd_eq_zero_iff.2 h, ←nsmul_singleton, ←gcd_dedup],
+    rw [dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton],
+    exact ⟨⟨rfl, h⟩, normalize_one⟩ },
+  { choose f hf using @gcd_dvd _ _ _ s,
+    have := _, push_neg at h,
+    refine ⟨s.pmap @f (λ _, id), this, extract_gcd' s _ h this⟩,
+    rw map_pmap, conv_lhs { rw [← s.map_id, ← s.pmap_eq_map _ _ (λ _, id)] },
+    congr' with x hx, rw [id, ← hf hx] },
+end
+
 end gcd
 
 end multiset