Commit 2026-06-30 14:08 240b4d26

View on Github →

feat(Algebra/Category/ModuleCat): submodules of presheaves of modules (#41159) We define submodules of presheaves of modules as restriction-stable families of Submodules and construct the associated presheaf of modules.

Estimated changes

Modified Mathlib.lean

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

added theorem PresheafOfModules.restrictₛₗ_apply

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

added theorem PresheafOfModules.Submodule.ext

added theorem PresheafOfModules.Submodule.homOfLE_ι

added theorem PresheafOfModules.Submodule.le_iff

added theorem PresheafOfModules.Submodule.map_mem

added theorem PresheafOfModules.Submodule.toPresheafOfModules_map_apply

added structure PresheafOfModules.Submodule

Modified Mathlib/Algebra/Module/Submodule/Map.lean

modified theorem Submodule.comap_finsetInf

modified theorem Submodule.comap_iInf