Commit 2025-07-05 08:19 12bf7091

View on Github →

refactor(CategoryTheory/Monoidal/Mod_): refactor Mod_ using MonoidalLeftAction (#25762) Generalize the definition of CategoryTheory.Monoidal.Mod_Class and CategoryTheory.Monoidal.Mod_ to modules in D over a monoid object in C, where C acts monoidally on D. At the same time, we refactor Mod_ in a way similar to the one Mon_ has been refactored in #24646. i.e we favor Mod_Class in the definition and Mod_, and introduce a Prop-class IsMod_Hom to define morphisms of modules.

Estimated changes

modified def Mod_.trivialAction
added def Mod_.Hom.mk''
added def Mod_.Hom.mk'
modified structure Mod_.Hom
modified theorem Mod_.assoc_flip
modified def Mod_.comap
modified def Mod_.comp
modified theorem Mod_.comp_hom'
modified def Mod_.forget
modified theorem Mod_.hom_ext
modified def Mod_.id
modified theorem Mod_.id_hom'
deleted def Mod_.mk'
modified def Mod_.regular
modified structure Mod_
modified theorem Mod_Class.assoc_flip
added theorem Mod_Class.ext
added theorem Mod_Class.mul_smul
added theorem Mod_Class.one_smul