Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_

Additional results about module objects in Cartesian monoidal categories #

source
🔸 coverage
@[reducible]
def CategoryTheory.ModObj.trivialAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] (X : C) :
ModObj M X

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

Instances For
    source
    🔸 coverage
    def CategoryTheory.Mod_.trivialAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
    Mod_ C M.X

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

    Instances For
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.Mod_.trivialAction_X {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
      (trivialAction M X).X = X
      source
      📐 coverage
      @[simp]
      theorem CategoryTheory.Mod_.trivialAction_mod_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) :
      ModObj.smul = SemiCartesianMonoidalCategory.snd M.X X