Modules as direct limits of finitely generated submodules

We show that every module is the direct limit of its finitely generated submodules.

Main definitions

• Module.fgSystem: the directed system of finitely generated submodules of a module.

• Module.fgSystem.equiv: the isomorphism between a module and the direct limit of its finitely generated submodules.

def Module.fgSystem (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] (N₁ N₂ : { N : Submodule R M // N.FG }) (le : N₁ ≤ N₂) : ↥↑N₁ →ₗ[R] ↥↑N₂

The directed system of finitely generated submodules of a module.

Equations

• Module.fgSystem R M N₁ N₂ le = Submodule.inclusion le

instance Module.fgSystem.instIsDirectedSubtypeSubmoduleFGLe (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : IsDirected { N : Submodule R M // N.FG } fun (x1 x2 : { N : Submodule R M // N.FG }) => x1 ≤ x2

instance Module.fgSystem.instDirectedSystemSubtypeSubmoduleFGMemValCoeLinearMapId (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : DirectedSystem (fun (x2 : { N : Submodule R M // N.FG }) => ↥↑x2) fun (x1 x2 : { N : Submodule R M // N.FG }) (x3 : x1 ≤ x2) (x4 : ↥↑x1) => (Module.fgSystem R M x1 x2 x3) x4

noncomputable def Module.fgSystem.equiv (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] : Module.DirectLimit (fun (i : { N : Submodule R M // N.FG }) => ↥↑i) (Module.fgSystem R M) ≃ₗ[R] M

Every module is the direct limit of its finitely generated submodules.

Equations

• One or more equations did not get rendered due to their size.

theorem Module.fgSystem.equiv_comp_of {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (N : { N : Submodule R M // N.FG }) : ↑(Module.fgSystem.equiv R M) ∘ₗ Module.DirectLimit.of R { N : Submodule R M // N.FG } (fun (i : { N : Submodule R M // N.FG }) => ↥↑i) (Module.fgSystem R M) N = (↑N).subtype