English
If (R,M,A,N) are rings and modules with localization data and f a localized map, then the NoZeroSMulDivisors property transfers to the localized target: NoZeroSMulDivisors A N.
Русский
Если кольца и модули локализованы и f локализованное отображение, свойство NoZeroSMulDivisors переносится на локализованный целевой модуль: NoZeroSMulDivisors A N.
LaTeX
$$$\text{NoZeroSMulDivisors}(A,N)$$$
Lean4
/-- We can clear the denominators of a `Finset`-indexed family of fractions. -/
theorem exist_integer_multiples {ι : Type*} (s : Finset ι) (g : ι → M') : ∃ b : S, ∀ i ∈ s, IsInteger f (b.val • g i) :=
by
classical
choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))
refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩
· exact (∏ j ∈ s.erase i, (sec j).2) • (sec i).1
· simp only [LinearMap.map_smul_of_tower, Submonoid.coe_finset_prod]
rw [← hsec, ← mul_smul, Submonoid.smul_def]
congr
simp only [Submonoid.coe_mul, Submonoid.coe_finset_prod, mul_comm]
rw [← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i), Finset.insert_erase hi]
