English
There exist a finite subset t of s and an N such that every m ≥ N with setGcd(s) | m lies in the span of t.
Русский
Существует конечное подмножество t ⊆ s и число N, чтобы каждый m ≥ N с gcd(s) делящим m принадлежал подпространству span t.
LaTeX
$$$\\exists t : \\mathrm{Finset}\\;\\mathbb{N},\\; \\exists n : \\mathbb{N},\\; \\uparrow t \\subseteq s \\land \\forall m \\ge n,\\; \\mathrm{setGcd}(s) \\mid m \\Rightarrow m \\in \\mathrm{Ideal.span}(t)$$$
Lean4
theorem exists_mem_span_nat_finset_of_ge :
∃ (t : Finset ℕ) (n : ℕ), ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ Ideal.span t :=
by
by_cases h0 : setGcd s = 0
·
refine
⟨∅, 0, by simp, fun _ _ dvd ↦ by cases zero_dvd_iff.mp (h0 ▸ dvd); exact zero_mem _⟩
-- Write the gcd of `s` as a ℤ-linear combination of a finite subset `t`.
have ⟨t, hts, a, eq⟩ :=
(Submodule.mem_span_image_iff_exists_fun _).mp
(span_singleton_setGcd s ▸ mem_span_singleton_self _)
-- Let `x` be an arbitrary nonzero element in `s`.
have ⟨x, hxs, hx⟩ := exists_ne_zero_of_setGcd_ne_zero h0
let n := (x / setGcd s) * ∑ i, (-a i).toNat * i
refine
⟨insert x t, n, by simpa [Set.insert_subset_iff] using ⟨hxs, hts⟩, fun m ge dvd ↦ ?_⟩
-- For `m ≥ n`, write `m = q * x + (r + n)` with 0 ≤ r < x.
obtain ⟨c, rfl⟩ := exists_add_of_le ge
rw [← c.div_add_mod' x]
set q := c / x
set r := c % x
rw [add_comm, add_assoc]
refine
add_mem (mul_mem_left _ q (subset_span (Finset.mem_insert_self ..)))
(Submodule.span_mono (s := t) (Finset.subset_insert ..) ?_)
-- It suffices to show `r + n` lies in the ℕ-span of `t`.
obtain ⟨rx, hrx⟩ : setGcd s ∣ r :=
(dvd_mod_iff (setGcd_dvd_of_mem hxs)).mpr <|
(Nat.dvd_add_right <|
dvd_mul_of_dvd_right (Finset.dvd_sum fun i _ ↦ dvd_mul_of_dvd_right (setGcd_dvd_of_mem (hts i.2)) _) _).mp
dvd
convert
(sum_mem fun i _ ↦ mul_mem_left _ _ (subset_span i.2) :
-- an explicit ℕ-linear combination of elements of `t` that is equal to `r + n`
∑ i : t, (if 0 ≤ a i then rx else x / setGcd s - rx) * (a i).natAbs * i ∈ span t)
simp_rw [← Int.natCast_inj, hrx, n, Finset.mul_sum, mul_comm _ rx, cast_add, cast_sum, cast_mul, ← eq, Finset.mul_sum,
smul_eq_mul, ← mul_assoc, ← Finset.sum_add_distrib, ← add_mul]
congr! 2 with i
split_ifs with hai
· rw [Int.toNat_eq_zero.mpr (by cutsat), cast_zero, mul_zero, add_zero, Int.natCast_natAbs, abs_eq_self.mpr hai]
· rw [cast_sub, Int.natCast_natAbs, abs_eq_neg_self.mpr (by cutsat), sub_mul, ← Int.eq_natCast_toNat.mpr (by cutsat),
mul_neg (rx : ℤ), sub_neg_eq_add, add_comm]
rw [← Nat.mul_le_mul_left_iff (pos_of_ne_zero h0), ← hrx, Nat.mul_div_cancel' (setGcd_dvd_of_mem hxs)]
exact (c.mod_lt (pos_of_ne_zero hx)).le
