Commit 2024-04-18 05:39 9c3efae3

View on Github →

feat: the category of sheaves of modules (#11479) This PR defines the category SheafOfModules R when R is a sheaf of rings on a category C equipped with a Grothendieck topology J.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

added structure SheafOfModules.Hom

added theorem SheafOfModules.comp_val

added def SheafOfModules.forget

added theorem SheafOfModules.hom_ext

added theorem SheafOfModules.id_val

added structure SheafOfModules