feat(ring_theory/localization): Clearing denominators (#10668)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

src/ring_theory/localization.lean

@@ -236,6 +236,49 @@ lemma exist_integer_multiples_of_finset (s : finset S) :
   ∃ (b : M), ∀ a ∈ s, is_integer R ((b : R) • a) :=
 exist_integer_multiples M s id
 
+/-- A choice of a common multiple of the denominators of a `finset`-indexed family of fractions. -/
+noncomputable
+def common_denom {ι : Type*} (s : finset ι) (f : ι → S) : M :=
+(exist_integer_multiples M s f).some
+
+/-- The numerator of a fraction after clearing the denominators
+of a `finset`-indexed family of fractions. -/
+noncomputable
+def integer_multiple {ι : Type*} (s : finset ι) (f : ι → S) (i : s) : R :=
+((exist_integer_multiples M s f).some_spec i i.prop).some
+
+@[simp]
+lemma map_integer_multiple {ι : Type*} (s : finset ι) (f : ι → S) (i : s) :
+  algebra_map R S (integer_multiple M s f i) = common_denom M s f • f i :=
+((exist_integer_multiples M s f).some_spec _ i.prop).some_spec
+
+/-- A choice of a common multiple of the denominators of a finite set of fractions. -/
+noncomputable
+def common_denom_of_finset (s : finset S) : M :=
+common_denom M s id
+
+/-- The finset of numerators after clearing the denominators of a finite set of fractions. -/
+noncomputable
+def finset_integer_multiple [decidable_eq R] (s : finset S) : finset R :=
+s.attach.image (λ t, integer_multiple M s id t)
+
+open_locale pointwise
+
+lemma finset_integer_multiple_image [decidable_eq R] (s : finset S) :
+  algebra_map R S '' (finset_integer_multiple M s) =
+    common_denom_of_finset M s • s :=
+begin
+  delta finset_integer_multiple common_denom,
+  rw finset.coe_image,
+  ext,
+  split,
+  { rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩,
+    rw map_integer_multiple,
+    exact set.mem_image_of_mem _ x.prop },
+  { rintro ⟨x, hx, rfl⟩,
+    exact ⟨_, ⟨⟨x, hx⟩, s.mem_attach _, rfl⟩, map_integer_multiple M s id _⟩ }
+end
+
 variables {R M}
 
 lemma map_right_cancel {x y} {c : M} (h : algebra_map R S (c * x) = algebra_map R S (c * y)) :