English
A semilocal module over a semiring is finite if all maximal localizations are finite.
Русский
Полупродукт над полупривязным кольцом конечно порожден, если все максимальные локализации конечны.
LaTeX
$$$\\text{Module.Finite}(R) \\iff \\forall P \\, [P.IsMaximal], \\text{Module.Finite}(R_p)$$$
Lean4
/-- A module `M` over a semilocal ring `R` is finite if
its localization at every maximal ideal is finite. -/
theorem of_isLocalized_maximal (H : ∀ (P : Ideal R) [P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)) : Module.Finite R M :=
by
classical
have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_
rw [eq_top_iff, ← hs ⟨P, hP⟩, Submodule.localized'_span, Submodule.span_le]
intro x hx
lift x to s ⟨P, hP⟩ using hx
rw [SetLike.mem_coe, ← IsLocalization.smul_mem_iff (s := (frac ⟨P, hP⟩ x).2), hfrac]
exact Submodule.subset_span ⟨_, by simpa using ⟨_, _, x.2, rfl⟩, rfl⟩
