English
Strengthening of a localization result: for a non-top ideal J in a Dedekind domain A and a finite set s, with f(i) ∈ K nonzero at some index, there exists a multiplier a ∈ K such that each a f(i) is integral over A, and for some i ∈ s, a f(i) does not lie in J.
Русский
Усиление локализации: для идеала J ≠ ⊤ в области Дедекида A и конечного множества s, при f(i) ∈ K не равном нулю, существует множитель a ∈ K так, что все a f(i) интеравны над A, и некоторый i ∈ s удовлетворяет a f(i) ∉ J.
LaTeX
$$∃ a ∈ K, (∀ i ∈ s, IsInteger_A(a f(i))) ∧ ∃ i ∈ s, a f(i) ∉ J$$
Lean4
/-- Strengthening of `IsLocalization.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`. -/
theorem exist_integer_multiples_notMem {J : Ideal A} (hJ : J ≠ ⊤) {ι : Type*} (s : Finset ι) (f : ι → K) {j}
(hjs : j ∈ s) (hjf : f j ≠ 0) :
∃ a : K, (∀ i ∈ s, IsLocalization.IsInteger A (a * f i)) ∧ ∃ i ∈ s, a * f i ∉ (J : FractionalIdeal A⁰ K) := by
-- Consider the fractional ideal `I` spanned by the `f`s.
let I : FractionalIdeal A⁰ K := spanFinset A s f
have hI0 : I ≠ 0 :=
spanFinset_ne_zero.mpr
⟨j, hjs, hjf⟩
-- We claim the multiplier `a` we're looking for is in `I⁻¹ \ (J / I)`.
suffices ↑J / I < I⁻¹ by
obtain ⟨_, a, hI, hpI⟩ := SetLike.lt_iff_le_and_exists.mp this
rw [mem_inv_iff hI0] at hI
refine
⟨a, fun 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
refine (mem_div_iff_of_nonzero hI0).mpr fun y hy => Submodule.span_induction ?_ ?_ ?_ ?_ hy
· rintro _ ⟨i, hi, rfl⟩; exact hpI i hi
· rw [mul_zero]; exact Submodule.zero_mem _
· intro x y _ _ hx hy; rw [mul_add]; exact Submodule.add_mem _ hx hy
· intro b x _ hx; rw [mul_smul_comm]; exact Submodule.smul_mem _ b hx
calc
↑J / I = ↑J * I⁻¹ := div_eq_mul_inv (↑J) I
_ < 1 * I⁻¹ := (mul_right_strictMono (inv_ne_zero hI0) ?_)
_ = I⁻¹ := one_mul _
rw [← coeIdeal_top]
-- And multiplying by `I⁻¹` is indeed strictly monotone.
exact strictMono_of_le_iff_le (fun _ _ => (coeIdeal_le_coeIdeal K).symm) (lt_top_iff_ne_top.mpr hJ)
