English
If there exists a finite set t ⊆ R such that the hypotheses hold for all g ∈ t, and each localized module is finite, then M is finite over R.
Русский
Если существует конечный набор t ⊆ R и для каждого g ∈ t выполнены условия, и каждый локализованный модуль конечен, то M конечен над R.
LaTeX
$$$\\forall t,\\text{ finite},\\ (\\forall g \\in t),\\ Module.Finite (Localization.Away g.val) (LocalizedModule (Submonoid.powers g.val) M) \\Rightarrow \\text{Module.Finite}(R,M)$$$
Lean4
/-- If there exists a finite set `{ r }` of `R` such that `Mᵣ` is `Rᵣ`-finite for each `r`,
then `M` is a finite `R`-module.
See `of_localizationSpan` for a version without the finite set assumption.
-/
theorem of_localizationSpan_finite (t : Finset R) (ht : Ideal.span (t : Set R) = ⊤)
(H : ∀ (g : t), Module.Finite (Localization.Away g.val) (LocalizedModule (Submonoid.powers g.val) M)) :
Module.Finite R M :=
let f (g : t) : M →ₗ[R] LocalizedModule (Submonoid.powers g.val) M :=
LocalizedModule.mkLinearMap (Submonoid.powers g.val) M
of_localizationSpan_finite' t ht f H
