English
The iSup of submodules equals the range of the lsum map with subtype projections; every element of the iSup can be obtained as a sum of finitely supported elements.
Русский
iSup подмодулов равен образу lsum с проекциями подмодулов; любой элемент iSup можно получить как сумма элементов с конечной опорой.
LaTeX
$$$\\iSup p = \\mathrm{range}(\\mathrm{DFinsupp.lsum}\\; \\mathbb{N}\\; (p_i).subtype)$$$
Lean4
/-- The supremum of a family of submodules is equal to the range of `DFinsupp.lsum`; that is
every element in the `iSup` can be produced from taking a finite number of non-zero elements
of `p i`, coercing them to `N`, and summing them. -/
theorem iSup_eq_range_dfinsupp_lsum (p : ι → Submodule R N) :
iSup p = LinearMap.range (DFinsupp.lsum ℕ fun i => (p i).subtype) :=
by
apply le_antisymm
· apply iSup_le _
intro i y hy
simp only [LinearMap.mem_range, lsum_apply_apply]
exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
· rintro x ⟨v, rfl⟩
exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2
