Additional results about module objects in Cartesian monoidal categories

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

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

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

• CategoryTheory.Mod.trivialAction M X = { X := X, mod := CategoryTheory.ModObj.trivialAction M.X X }

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

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

@[deprecated CategoryTheory.Mod.trivialAction (since := "2026-04-21")]

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

Alias of CategoryTheory.Mod.trivialAction.

---

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

Equations

• @CategoryTheory.Mod_.trivialAction = @CategoryTheory.Mod.trivialAction