Commit 2024-04-12 03:02 0129c03d

View on Github →

feat: construction of a presheaf of modules from a family of modules over various rings (#6845) This PR provides constructors for presheaves of modules over a presheaf of rings R using families of (bundled or unbundled) modules over R.obj X for all X.

Estimated changes

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

added theorem BundledCorePresheafOfModules.restrictionApp_toPresheafOfModules

added theorem BundledCorePresheafOfModules.toPresheafOfModules_obj

added theorem BundledCorePresheafOfModules.toPresheafOfModules_presheaf_map_apply

added structure BundledCorePresheafOfModules

added def CorePresheafOfModules.presheaf

added def CorePresheafOfModules.toPresheafOfModules

added theorem CorePresheafOfModules.toPresheafOfModules_obj

added theorem CorePresheafOfModules.toPresheafOfModules_presheaf_map_apply

added structure CorePresheafOfModules

added def PresheafOfModules.Hom.mk'

added theorem PresheafOfModules.Hom.mk'_app

added def PresheafOfModules.evaluation

added theorem PresheafOfModules.naturality_apply

added theorem PresheafOfModules.restrictionApp_apply

added theorem PresheafOfModules.restriction_app_comp

added theorem PresheafOfModules.restriction_app_id