Commit 2024-05-08 15:35 9d8f6783

View on Github →

feat(Algebra/Category/ModuleCat): the category of presheaves of modules has colimits (#12713)

Estimated changes

Modified Mathlib.lean

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

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

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

added theorem PresheafOfModules.colimitCoconeιApp_naturality

added def PresheafOfModules.evaluationJointlyReflectsColimits

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