English
A module M is the direct limit of its finitely generated submodules; there is a canonical linear equivalence between the direct limit of the directed system of FG-submodules and M.
Русский
Модуль M является прямым пределом своих конечно-порождаемых подмодулей; существует каноническое линейное экрививное соответствие между прямым пределом FG-подмодулов и M.
LaTeX
$$$M \\cong_{\\text{linear}} \\varinjlim_{P\\FG} P, \\qquad P\\text{ FG}.$$$
Lean4
/-- Any module is the direct limit of its finitely generated submodules -/
noncomputable def directLimit [DecidableEq { P : Submodule R M // P.FG }] :
Module.DirectLimit (ι := { P : Submodule R M // P.FG }) (G := fun P ↦ P.val)
(fun ⦃P Q⦄ (h : P ≤ Q) ↦ Submodule.inclusion h) ≃ₗ[R]
M :=
LinearEquiv.ofBijective (Module.DirectLimit.lift _ _ _ _ (fun P ↦ P.val.subtype) (fun _ _ _ _ ↦ rfl))
⟨Module.DirectLimit.lift_injective _ _ (fun P ↦ Submodule.injective_subtype P.val), fun x ↦
⟨Module.DirectLimit.of _ { P : Submodule R M // P.FG } _ _ ⟨Submodule.span R { x }, Submodule.fg_span_singleton x⟩
⟨x, Submodule.mem_span_singleton_self x⟩,
by simp⟩⟩
