Commit 2026-04-04 12:29 6b4acdbd

View on Github →

feat(Algebra/Category/ModuleCat): the category of presheaves of modules is symmetric (#37370) (When the presheaf of rings is commutative.)

Estimated changes

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

added theorem PresheafOfModules.associator_hom_app

added theorem PresheafOfModules.associator_inv_app

added theorem PresheafOfModules.braiding_hom_app

added theorem PresheafOfModules.braiding_inv_app

added theorem PresheafOfModules.leftUnitor_hom_app

added theorem PresheafOfModules.leftUnitor_inv_app

added theorem PresheafOfModules.rightUnitor_hom_app

added theorem PresheafOfModules.rightUnitor_inv_app

added theorem PresheafOfModules.tensorHom_app

added theorem PresheafOfModules.tensorObj_obj

added theorem PresheafOfModules.whiskerLeft_app

added theorem PresheafOfModules.whiskerRight_app