mathlib

mathlib copied to clipboard

I defined the category of modules following this link. This may or may not be useful to define sheaf of modules.

---

I think BundledModule is a confusing name, because Module is already "bundled" relative to module.

Perhaps RingModulePair?

Is there a general way to formalize grothendieck construction in mathlib now?

It's possible to use category_theory.grothendieck because R ↦ Module R is a strict functor from (Comm)Ring to Cat. (I think it's also possible to define PresheafedSpace using this strict Grothendieck construction) The generalization to oplax functors is in this branch but not yet PR'd.