Commit 2024-06-06 22:06 590bb467

View on Github →

feat: the pushforward of (pre)sheaves of modules (#13463)

Estimated changes

Modified Mathlib.lean

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

added theorem PresheafOfModules.pushforward_map_app_apply

added theorem PresheafOfModules.pushforward_obj_map_apply

added theorem PresheafOfModules.pushforward_obj_obj

added def PresheafOfModules.pushforward₀

added def PresheafOfModules.pushforward₀CompToPresheaf

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