Additional results about module objects in cartesian monoidal categories #
@[reducible]
def
Mod_Class.trivialAction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(M : C)
[Mon_Class M]
(X : C)
:
Mod_Class M X
Every object is a module over a monoid object via the trivial action.
Equations
- Mod_Class.trivialAction M X = { smul := CategoryTheory.CartesianMonoidalCategory.snd M X, one_smul' := ⋯, mul_smul' := ⋯ }
Instances For
def
Mod_.trivialAction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(M : Mon_ C)
(X : C)
:
Every object is a module over a monoid object via the trivial action.
Equations
- Mod_.trivialAction M X = { X := X, mod := Mod_Class.trivialAction M.X X }
Instances For
@[simp]
theorem
Mod_.trivialAction_mod_smul
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(M : Mon_ C)
(X : C)
:
@[simp]
theorem
Mod_.trivialAction_X
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(M : Mon_ C)
(X : C)
: