A module as the filtered colimit of its finitely generated submodules

Mathlib has both halves of this statement and does not join them. Module.fgSystem.equiv identifies a module with the direct limit of its finitely generated submodules, as a linear equivalence; ModuleCat.directLimitIsColimit exhibits an unbundled direct limit as a categorical colimit. This file is the composite: the cocone whose vertex is the module itself, and whose legs are the inclusions of its finitely generated submodules, is a colimit in ModuleCat R.

The categorical form is what a sheaf-theoretic consumer needs. Approximating a quasi-coherent sheaf by its coherent subsheaves is a colimit statement about a diagram of subobjects, and the comparison maps it has to produce are cocone legs; Module.fgSystem.equiv alone cannot supply those.

Main definitions

• ModuleCat.fgSubmoduleDiagram: the diagram of finitely generated submodules.
• ModuleCat.fgSubmoduleCocone: that diagram's cocone with vertex the module itself.

Main results

• ModuleCat.fgSubmoduleCoconeIsColimit: the cocone is a colimit.

Implementation notes

DecidableEq (Submodule R M) is carried rather than obtained from Classical, because Module.fgSystem.equiv and ModuleCat.directLimitDiagram both carry it; introducing choice here would make this statement harder to use than the two it is built from, not easier.

References

• Mathlib's Algebra/Colimit/Finiteness.lean and Algebra/Category/ModuleCat/Limits.lean.

@[reducible, inline]

noncomputable abbrev ModuleCat.fgSubmoduleDiagram (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Functor { N : Submodule R M // N.FG } (ModuleCat R)

The diagram of finitely generated submodules of M, valued in ModuleCat R.

Equations

• ModuleCat.fgSubmoduleDiagram R M = ModuleCat.directLimitDiagram (fun (N : { N : Submodule R M // N.FG }) => ↥↑N) (Module.fgSystem R M)

noncomputable def ModuleCat.fgSubmoduleCocone (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] : CategoryTheory.Limits.Cocone (fgSubmoduleDiagram R M)

The cocone on fgSubmoduleDiagram whose vertex is M itself, with the inclusion of each finitely generated submodule as its leg.

Equations

• ModuleCat.fgSubmoduleCocone R M = { pt := ModuleCat.of R M, ι := { app := fun (N : { N : Submodule R M // N.FG }) => ModuleCat.ofHom (↑N).subtype, naturality := ⋯ } }

@[simp]

theorem ModuleCat.fgSubmoduleCocone_pt_carrier (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] : ↑(fgSubmoduleCocone R M).pt = M

@[simp]

theorem ModuleCat.fgSubmoduleCocone_ι_app (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] (N : { N : Submodule R M // N.FG }) : (fgSubmoduleCocone R M).ι.app N = ofHom (↑N).subtype

noncomputable def ModuleCat.fgSubmoduleCoconeIsColimit (R : Type u) [CommRing R] (M : Type u) [AddCommGroup M] [Module R M] [DecidableEq (Submodule R M)] : CategoryTheory.Limits.IsColimit (fgSubmoduleCocone R M)

Every module is the filtered colimit of its finitely generated submodules.

Module.fgSystem.equiv is the same statement as a linear equivalence with a direct limit; this transports it across ModuleCat.directLimitIsColimit, and Module.fgSystem.equiv_comp_of is exactly the compatibility with the cocone legs that the transport needs.

Equations

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