Def SheafOfModules.evaluation

Modification history

2026-03-06 08:34
Mathlib/Algebra/Category/ModuleCat/Sheaf.lean
refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …
Modified SheafOfModules.evaluationView on Github →
2024-04-30 15:37
Mathlib/Algebra/Category/ModuleCat/Sheaf.lean
feat(Algebra/Category/ModuleCat): the category of sheaves of modules has limits (#12269)
Added SheafOfModules.evaluationView on Github →