English
If M is finite as an R-module, then the localized module M_p is finite over R_p; localization preserves module finiteness.
Русский
Если M конечно как модуль над R, то локализованный модуль M_p конечно над R_p; локализация сохраняет конечность модуля.
LaTeX
$$$\\text{Module.Finite}(R,M)\\Rightarrow \\text{Module.Finite}(R_p,M_p)$$$
Lean4
theorem of_isLocalizedModule [Module.Finite R M] : Module.Finite Rₚ Mₚ := by
classical
obtain ⟨T, hT⟩ := ‹Module.Finite R M›
use T.image f
rw [eq_top_iff]
rintro x -
obtain ⟨⟨y, m⟩, (hyx : IsLocalizedModule.mk' f y m = x)⟩ := IsLocalizedModule.mk'_surjective S f x
have hy : y ∈ Submodule.span R T := by rw [hT]; trivial
have : f y ∈ Submodule.map f (Submodule.span R T) := Submodule.mem_map_of_mem hy
rw [Submodule.map_span] at this
have H : Submodule.span R (f '' T) ≤ (Submodule.span Rₚ (f '' T)).restrictScalars R := by rw [Submodule.span_le];
exact Submodule.subset_span
convert (Submodule.span Rₚ (f '' T)).smul_mem (IsLocalization.mk' Rₚ (1 : R) m) (H this) using 0
· rw [← hyx, ← IsLocalizedModule.mk'_one S, IsLocalizedModule.mk'_smul_mk']
simp
