Additional results about module objects in cartesian monoidal categories

def Mod_.trivialAction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (M : Mon_ C) (X : C) : Mod_ M

Every object is a module over a monoid object via the trivial action.

Equations

• Mod_.trivialAction M X = { X := X, smul := CategoryTheory.ChosenFiniteProducts.snd M.X X, one_smul := ⋯, assoc := ⋯ }

@[simp]

theorem Mod_.trivialAction_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (M : Mon_ C) (X : C) : (trivialAction M X).smul = CategoryTheory.ChosenFiniteProducts.snd M.X X

@[simp]

theorem Mod_.trivialAction_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (M : Mon_ C) (X : C) : (trivialAction M X).X = X

@[reducible]

def Mod_Class.trivialAction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts.snd M X, one_smul := ⋯, mul_smul := ⋯ }