English
There exists a linear bijection between the direct sum of the p_i and N, given independence and top generation.
Русский
Существует линейное биективное соответствие между прямой суммой p_i и N при независимости и порождении сверху.
LaTeX
$$noncomputable def linearEquiv (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) : (Π₀ i, p i) ≃ₗ[R] N$$
Lean4
/-- If `(pᵢ)ᵢ` is a family of independent submodules that generates the whole module `N`, then
`N` is isomorphic to the direct sum of the submodules. -/
@[simps! apply]
noncomputable def linearEquiv {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) :
(Π₀ i, p i) ≃ₗ[R] N :=
.ofBijective _
⟨ind.dfinsupp_lsum_injective, by rwa [← LinearMap.range_eq_top, ← Submodule.iSup_eq_range_dfinsupp_lsum]⟩
