Commit 2024-06-04 08:15 724afa63

View on Github →

feat: the free (pre)sheaf of modules of rank 1 (#13461)

Estimated changes

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

added def PresheafOfModules.sections

added def PresheafOfModules.sectionsMk

added theorem PresheafOfModules.sections_ext

added def PresheafOfModules.unitCore

added def PresheafOfModules.unitHomEquiv

added theorem PresheafOfModules.unit_map_one

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

added def SheafOfModules.fullyFaithfulForget

added def SheafOfModules.unit

added def SheafOfModules.unitHomEquiv

added theorem SheafOfModules.unitHomEquiv_apply_coe