English
If each p(i) is finitely generated, then the pi-submodule Submodule.pi univ p is finitely generated.
Русский
Если каждый p(i) FG, то подпроизведение p через произведение (pi) FG.
LaTeX
$$$\forall i, (p(i)).FG \Rightarrow (\mathrm{Submodule.pi} \; \mathrm{Set.univ} \; p).FG$$$
Lean4
theorem fg_pi {ι : Type*} {M : ι → Type*} [Finite ι] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
{p : ∀ i, Submodule R (M i)} (hsb : ∀ i, (p i).FG) : (Submodule.pi Set.univ p).FG := by
classical
simp_rw [fg_def] at hsb ⊢
choose t htf hts using hsb
refine
⟨⋃ i, (LinearMap.single R _ i) '' t i, Set.finite_iUnion fun i => (htf i).image _, ?_⟩
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 changed `span_image` into `span_image _`
simp_rw [span_iUnion, span_image _, hts, Submodule.iSup_map_single]
