Documentation

Mathlib.Algebra.Category.FGModuleCat.Limits

forget₂ (FGModuleCat K) (ModuleCat K) creates all finite limits. #

And hence FGModuleCat K has all finite limits.

Future work #

After generalising FGModuleCat to allow the ring and the module to live in different universes, generalize this construction so we can take limits over smaller diagrams, as is done for the other algebraic categories.

Analogous constructions for Noetherian modules.