Commit 2024-04-20 20:51 5d9cf93c

View on Github →

feat(Algebra/Category/ModuleCat): the category of presheaves of modules has limits (#12264)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

added theorem ModuleCat.restrictScalarsComp'App_hom_naturality

added theorem ModuleCat.restrictScalarsComp'App_inv_naturality

added theorem ModuleCat.restrictScalarsId'App_hom_naturality

added theorem ModuleCat.restrictScalarsId'App_inv_naturality

Modified Mathlib/Algebra/Category/ModuleCat/Limits.lean

deleted theorem ModuleCat.hasLimit

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

added theorem PresheafOfModules.restrictionApp_comp

added theorem PresheafOfModules.restrictionApp_id

added theorem PresheafOfModules.restrictionApp_naturality

deleted theorem PresheafOfModules.restriction_app_comp

deleted theorem PresheafOfModules.restriction_app_id

modified def PresheafOfModules.toPresheaf

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

added def PresheafOfModules.evaluationJointlyReflectsLimits

added theorem PresheafOfModules.limitConeπApp_naturality

Modified Mathlib/Algebra/Homology/ModuleCat.lean

modified theorem ModuleCat.homology'_ext