English
There exists a linear equivalence between the direct limit of the system of finitely generated submodules of M and M itself.
Русский
Существует линейное эквивалентное отображение между прямым пределом системы Fargo и самим модулем M.
LaTeX
$$$\\mathrm{DirectLimit}(\\mathrm{fgSystem}\\, R\\, M) \\simeq_{\\text{lin}} M$$$
Lean4
/-- Every module is the direct limit of its finitely generated submodules. -/
noncomputable def equiv : DirectLimit _ (fgSystem R M) ≃ₗ[R] M :=
.ofBijective (lift _ _ _ _ (fun _ ↦ Submodule.subtype _) fun _ _ _ _ ↦ rfl)
⟨lift_injective _ _ fun _ ↦ Subtype.val_injective, fun x ↦
⟨of _ _ _ _ ⟨_, fg_span_singleton x⟩ ⟨x, subset_span <| by rfl⟩, lift_of ..⟩⟩
