Commit 2026-09-05 01:44 7974e751

View on Github →

feat(Algebra/Category/ModuleCat): refactor Monoidal.lean to use PresheafOfModulesOfCommRing (#43193)

Estimated changes

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

deleted theorem PresheafOfModules.Monoidal.tensorObj_map_tmul

deleted theorem PresheafOfModules.associator_hom_app

deleted theorem PresheafOfModules.associator_inv_app

deleted theorem PresheafOfModules.braiding_hom_app

deleted theorem PresheafOfModules.braiding_inv_app

deleted theorem PresheafOfModules.leftUnitor_hom_app

deleted theorem PresheafOfModules.leftUnitor_inv_app

deleted theorem PresheafOfModules.rightUnitor_hom_app

deleted theorem PresheafOfModules.rightUnitor_inv_app

deleted theorem PresheafOfModules.tensorHom_app

deleted theorem PresheafOfModules.tensorObj_obj

deleted theorem PresheafOfModules.whiskerLeft_app

deleted theorem PresheafOfModules.whiskerRight_app

added theorem PresheafOfModulesOfCommRing.Monoidal.tensorObj_map_tmul

added theorem PresheafOfModulesOfCommRing.associator_hom_app

added theorem PresheafOfModulesOfCommRing.associator_inv_app

added theorem PresheafOfModulesOfCommRing.braiding_hom_app

added theorem PresheafOfModulesOfCommRing.braiding_inv_app

added theorem PresheafOfModulesOfCommRing.leftUnitor_hom_app

added theorem PresheafOfModulesOfCommRing.leftUnitor_inv_app

added theorem PresheafOfModulesOfCommRing.rightUnitor_hom_app

added theorem PresheafOfModulesOfCommRing.rightUnitor_inv_app

added theorem PresheafOfModulesOfCommRing.tensorHom_app

added theorem PresheafOfModulesOfCommRing.tensorObj_obj

added theorem PresheafOfModulesOfCommRing.whiskerLeft_app

added theorem PresheafOfModulesOfCommRing.whiskerRight_app

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

added theorem PresheafOfModulesOfCommRing.naturality_apply