Commit 2024-11-14 20:21 579a434e

View on Github →

feat(Algebra/Category/ModuleCat/Presheaf): presheaves of modules are generated by their sections (#18160) We provide a presentation of any presheaf of modules involving coproducts of free presheaves of modules generated by Yoneda presheaves of types.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean

added theorem PresheafOfModules.Elements.fromFreeYoneda_app_apply

added theorem PresheafOfModules.freeYoneda.isDetecting

added theorem PresheafOfModules.freeYoneda.isSeparating

added def PresheafOfModules.freeYoneda

added theorem PresheafOfModules.freeYonedaEquiv_comp

added theorem PresheafOfModules.freeYonedaEquiv_symm_app

added theorem PresheafOfModules.fromFreeYonedaCoproduct_app_mk

added theorem PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct

added theorem PresheafOfModules.ι_fromFreeYonedaCoproduct

added theorem PresheafOfModules.ι_fromFreeYonedaCoproduct_apply