Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_

Additional results about module objects in cartesian monoidal categories #

source
@[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
    Instances For
      source
      def Mod_.trivialAction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon_ C) (X : C) :
      Mod_ C M.X

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

      Equations
        Instances For
          source
          @[simp]
          theorem Mod_.trivialAction_mod_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon_ C) (X : C) :
          Mod_Class.smul = CategoryTheory.CartesianMonoidalCategory.snd M.X X
          source
          @[simp]
          theorem Mod_.trivialAction_X {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon_ C) (X : C) :
          (trivialAction M X).X = X