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.

Equations
    Instances For
      source
      🔸 coverage
      @[deprecated CategoryTheory.ModObj.trivialAction (since := "2025-09-14")]
      def CategoryTheory.Mod_Class.trivialAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : C) [MonObj M] (X : C) :
      ModObj M X

      Alias of CategoryTheory.ModObj.trivialAction.

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

      Equations
        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.

          Equations
            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