feat(ring_theory/dedekind_domain): strengthen `exist_integer_multiple…

…s` (#12184)

Let `J ≠ ⊤` be an ideal in a Dedekind domain `A`, and `f ≠ 0` a finite collection of elements of `K = Frac(A)`, then we can multiply the elements of `f` by some `a : K` to find a collection of elements of `A` that is not completely contained in `J`.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/ring_theory/dedekind_domain/ideal.lean

@@ -688,6 +688,49 @@ lemma ideal.exists_mem_pow_not_mem_pow_succ (I : ideal A) (hI0 : I ≠ ⊥) (hI1
   ∃ x ∈ I^e, x ∉ I^(e+1) :=
 set_like.exists_of_lt (I.strict_anti_pow hI0 hI1 e.lt_succ_self)
 
+open fractional_ideal
+variables {A K}
+
+/-- Strengthening of `is_localization.exist_integer_multiples`:
+Let `J ≠ ⊤` be an ideal in a Dedekind domain `A`, and `f ≠ 0` a finite collection
+of elements of `K = Frac(A)`, then we can multiply the elements of `f` by some `a : K`
+to find a collection of elements of `A` that is not completely contained in `J`. -/
+lemma ideal.exist_integer_multiples_not_mem
+  {J : ideal A} (hJ : J ≠ ⊤) {ι : Type*} (s : finset ι) (f : ι → K)
+  {j} (hjs : j ∈ s) (hjf : f j ≠ 0) :
+  ∃ a : K, (∀ i ∈ s, is_localization.is_integer A (a * f i)) ∧
+    ∃ i ∈ s, (a * f i) ∉ (J : fractional_ideal A⁰ K) :=
+begin
+  -- Consider the fractional ideal `I` spanned by the `f`s.
+  let I : fractional_ideal A⁰ K := fractional_ideal.span_finset A s f,
+  have hI0 : I ≠ 0 := fractional_ideal.span_finset_ne_zero.mpr ⟨j, hjs, hjf⟩,
+  -- We claim the multiplier `a` we're looking for is in `I⁻¹ \ (J / I)`.
+  suffices : ↑J / I < I⁻¹,
+  { obtain ⟨_, a, hI, hpI⟩ := set_like.lt_iff_le_and_exists.mp this,
+    rw mem_inv_iff hI0 at hI,
+    refine ⟨a, λ i hi, _, _⟩,
+    -- By definition, `a ∈ I⁻¹` multiplies elements of `I` into elements of `1`,
+    -- in other words, `a * f i` is an integer.
+    { exact (mem_one_iff _).mp (hI (f i)
+        (submodule.subset_span (set.mem_image_of_mem f hi))) },
+    { contrapose! hpI,
+      -- And if all `a`-multiples of `I` are an element of `J`,
+      -- then `a` is actually an element of `J / I`, contradiction.
+      refine (mem_div_iff_of_nonzero hI0).mpr (λ y hy, submodule.span_induction hy _ _ _ _),
+      { rintros _ ⟨i, hi, rfl⟩, exact hpI i hi },
+      { rw mul_zero, exact submodule.zero_mem _ },
+      { intros x y hx hy, rw mul_add, exact submodule.add_mem _ hx hy },
+      { intros b x hx, rw mul_smul_comm, exact submodule.smul_mem _ b hx } } },
+  -- To show the inclusion of `J / I` into `I⁻¹ = 1 / I`, note that `J < I`.
+  calc ↑J / I = ↑J * I⁻¹ : div_eq_mul_inv ↑J I
+          ... < 1 * I⁻¹ : mul_right_strict_mono (inv_ne_zero hI0) _
+          ... = I⁻¹ : one_mul _,
+  { rw [← coe_ideal_top],
+    -- And multiplying by `I⁻¹` is indeed strictly monotone.
+    exact strict_mono_of_le_iff_le (λ _ _, (coe_ideal_le_coe_ideal K).symm)
+      (lt_top_iff_ne_top.mpr hJ) },
+end
+
 end is_dedekind_domain
 
 section is_dedekind_domain

src/ring_theory/fractional_ideal.lean

@@ -983,6 +983,31 @@ variables [algebra R₁ K] [is_fraction_ring R₁ K]
 
 open_locale classical
 
+variables (R₁)
+
+/-- `fractional_ideal.span_finset R₁ s f` is the fractional ideal of `R₁` generated by `f '' s`. -/
+@[simps] def span_finset {ι : Type*} (s : finset ι) (f : ι → K) :
+  fractional_ideal R₁⁰ K :=
+⟨submodule.span R₁ (f '' s), begin
+  obtain ⟨a', ha'⟩ := is_localization.exist_integer_multiples R₁⁰ s f,
+  refine ⟨a', a'.2, λ x hx, submodule.span_induction hx _ _ _ _⟩,
+  { rintro _ ⟨i, hi, rfl⟩, exact ha' i hi },
+  { rw smul_zero, exact is_localization.is_integer_zero },
+  { intros x y hx hy, rw smul_add, exact is_localization.is_integer_add hx hy },
+  { intros c x hx, rw smul_comm, exact is_localization.is_integer_smul hx }
+end⟩
+
+variables {R₁}
+
+@[simp] lemma span_finset_eq_zero {ι : Type*} {s : finset ι} {f : ι → K} :
+  span_finset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0 :=
+by simp only [← coe_to_submodule_injective.eq_iff, span_finset_coe, coe_zero, submodule.span_eq_bot,
+  set.mem_image, finset.mem_coe, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+
+lemma span_finset_ne_zero {ι : Type*} {s : finset ι} {f : ι → K} :
+  span_finset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0 :=
+by simp
+
 open submodule.is_principal
 
 include loc