Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Mod_

Additional results about module objects in Cartesian monoidal categories #

@[reducible]

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

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

Equations

ModObj.trivialAction M X = { smul := CategoryTheory.CartesianMonoidalCategory.snd M X, one_smul' := ⋯, mul_smul' := ⋯ }

Instances For

@[deprecated ModObj.trivialAction (since := "2025-09-14")]

def Mod_Class.trivialAction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : C) [MonObj M] (X : C) :

Alias of ModObj.trivialAction.

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

Equations

@Mod_Class.trivialAction = @ModObj.trivialAction

Instances For

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

Mod_.trivialAction M X = { X := X, mod := ModObj.trivialAction M.X X }

Instances For

@[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

@[simp]

theorem Mod_.trivialAction_mod_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (M : Mon_ C) (X : C) :

ModObj.smul = CategoryTheory.CartesianMonoidalCategory.snd M.X X