English
The closure of the image of the iSup map of submodules under the single-map equals the product of closures.
Русский
Замыкание образа iSup отображений через единичный отображатель равно произведению их замыканий.
LaTeX
$$$ closure( Submodule.setLike.coe (iSup (\! i, (s i).map(LinearMap.single R M i)))) = Set.univ.\pi (i \mapsto closure (s i))$$$
Lean4
/-- If `s i` is a family of submodules, each is in its module,
then the closure of their span in the indexed product of the modules
is the product of their closures.
In case of a finite index type, this statement immediately follows from `Submodule.iSup_map_single`.
However, the statement is true for an infinite index type as well. -/
theorem closure_coe_iSup_map_single (s : ∀ i, Submodule R (M i)) :
closure (↑(⨆ i, (s i).map (LinearMap.single R M i)) : Set (∀ i, M i)) = Set.univ.pi fun i ↦ closure (s i) :=
by
rw [← closure_pi_set]
refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
· exact SetLike.coe_mono <| iSup_map_single_le
· simp only [Set.subset_def, mem_closure_iff]
intro x hx U hU hxU
rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
· simp_all [Finset.sum_pi_single]
· exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _
