English
Let R be a ring, V an R-module, and ι a finite index set. If S: ι → Submodule R V is such that each S(i) is finitely generated as an R-module, then the supremum (sum) of all S(i) is finitely generated; i.e. ⨆ i, S(i) is Module-Finite over R.
Русский
Пусть R—кольцо, V — модуль над R, и ι конечный индекс. Если S: ι → Submodule R V таково, что каждый S(i) является конечнопорождённым R-модулем, тогда их суммарная подмодуля (верхняя граница) ⨆ i, S(i) также является конечнопорождённой над R.
LaTeX
$$$[\\operatorname{Finite}(\\iota)] \\wedge (\\forall i:\\iota,\\ \\text{Module.Finite}_R(S(i))) \\Rightarrow \\text{Module.Finite}_R\\bigl(\\bigvee_{i:\\iota} S(i)\\bigr).$$$
Lean4
/-- The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite
sort is finite-dimensional. -/
instance finite_iSup {ι : Sort*} [Finite ι] (S : ι → Submodule R V) [∀ i, Module.Finite R (S i)] :
Module.Finite R ↑(⨆ i, S i) := by
cases nonempty_fintype (PLift ι)
rw [← iSup_plift_down, ← Finset.sup_univ_eq_iSup]
exact Submodule.finite_finset_sup _ _
