Module objects in cartesian monoidal categories

In this file we study module objects in a cartesian monoidal category C action on itself by ⊗.

In particular, for a monoid object M : C action on X : C, we equip Z ⟶ X with a M ⟶ X action for every Z : C.

@[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_mod_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (M : Mon C) (X : C) : ModObj.smul = SemiCartesianMonoidalCategory.snd 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

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

@[instance_reducible]

instance CategoryTheory.Hom.instSMulHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Y : C) : SMul (Y ⟶ M) (Y ⟶ X)

Morphisms Y ⟶ M act on morphisms Y ⟶ X via the internal scalar multiplication.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CategoryTheory.Hom.instVAddHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Y : C) : VAdd (Y ⟶ M) (Y ⟶ X)

Morphisms Y ⟶ M act on morphisms Y ⟶ X via the internal additive action.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Hom.vadd_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X) : m +ᵥ x = CategoryStruct.comp (CartesianMonoidalCategory.lift m x) AddModObj.vadd

theorem CategoryTheory.Hom.smul_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Y : C) (m : Y ⟶ M) (x : Y ⟶ X) : m • x = CategoryStruct.comp (CartesianMonoidalCategory.lift m x) ModObj.smul

@[instance_reducible]

instance CategoryTheory.Hom.mulAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) : MulAction (Z ⟶ M) (Z ⟶ X)

If M is a monoid object acting on X, then morphisms into M act on morphisms into X.

Equations

• CategoryTheory.Hom.mulAction Z = { toSMul := CategoryTheory.Hom.instSMulHom Z, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance CategoryTheory.Hom.addAction {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] (Z : C) : AddAction (Z ⟶ M) (Z ⟶ X)

If M is an additive monoid object acting on X, then morphisms into M act on morphisms into X.

Equations

• CategoryTheory.Hom.addAction Z = { toVAdd := CategoryTheory.Hom.instVAddHom Z, add_vadd := ⋯, zero_vadd := ⋯ }

theorem CategoryTheory.ModObj.comp_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z Z' : C} (g : Z' ⟶ Z) (m : Z ⟶ M) (x : Z ⟶ X) : CategoryStruct.comp g (m • x) = CategoryStruct.comp g m • CategoryStruct.comp g x

@[simp]

theorem CategoryTheory.IsModHom.map_smul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) : CategoryStruct.comp (m • x) f = m • CategoryStruct.comp x f

@[simp]

theorem CategoryTheory.IsAddModHom.map_vadd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) : CategoryStruct.comp (m +ᵥ x) f = m +ᵥ CategoryStruct.comp x f

@[simp]

theorem CategoryTheory.IsModHom.map_smul_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (m • x) (CategoryStruct.comp f h) = CategoryStruct.comp (m • CategoryStruct.comp x f) h

@[simp]

theorem CategoryTheory.IsAddModHom.map_vadd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] {Z : C} (m : Z ⟶ M) (x : Z ⟶ X) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (m +ᵥ x) (CategoryStruct.comp f h) = CategoryStruct.comp (m +ᵥ CategoryStruct.comp x f) h

def CategoryTheory.IsModHom.mulActionHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] (Z : C) : (Z ⟶ X) →ₑ[id] Z ⟶ Y

An M-equivariant morphism induces an equivariant function on hom types.

Equations

• CategoryTheory.IsModHom.mulActionHom f Z = { toFun := fun (x : Z ⟶ X) => CategoryTheory.CategoryStruct.comp x f, map_smul' := ⋯ }

def CategoryTheory.IsAddModHom.addActionHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] (Z : C) : (Z ⟶ X) →ₑ[id] Z ⟶ Y

A φ-equivariant morphism induces an equivariant morphism on hom types.

Equations

• CategoryTheory.IsAddModHom.addActionHom f Z = { toFun := fun (x : Z ⟶ X) => CategoryTheory.CategoryStruct.comp x f, map_vadd' := ⋯ }

@[simp]

theorem CategoryTheory.IsAddModHom.addActionHom_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [AddMonObj M] {X : C} [AddModObj M X] {Y : C} [AddModObj M Y] (f : X ⟶ Y) [IsAddModHom M f] (Z : C) (x✝ : Z ⟶ X) : (addActionHom f Z) x✝ = CategoryStruct.comp x✝ f

@[simp]

theorem CategoryTheory.IsModHom.mulActionHom_apply {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Y : C} [ModObj M Y] (f : X ⟶ Y) [IsModHom M f] (Z : C) (x✝ : Z ⟶ X) : (mulActionHom f Z) x✝ = CategoryStruct.comp x✝ f

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

The morphism (m, x) ↦ (m • x, x).

Equations

• CategoryTheory.ModObj.leftSMul M X = CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.ModObj.smul (CategoryTheory.SemiCartesianMonoidalCategory.snd M X)

@[simp]

theorem CategoryTheory.ModObj.leftSMul_fst {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] : CategoryStruct.comp (leftSMul M X) (SemiCartesianMonoidalCategory.fst X X) = smul

@[simp]

theorem CategoryTheory.ModObj.leftSMul_fst_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (leftSMul M X) (CategoryStruct.comp (SemiCartesianMonoidalCategory.fst X X) h) = CategoryStruct.comp smul h

@[simp]

theorem CategoryTheory.ModObj.leftSMul_snd {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] : CategoryStruct.comp (leftSMul M X) (SemiCartesianMonoidalCategory.snd X X) = SemiCartesianMonoidalCategory.snd M X

@[simp]

theorem CategoryTheory.ModObj.leftSMul_snd_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (leftSMul M X) (CategoryStruct.comp (SemiCartesianMonoidalCategory.snd X X) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.snd M X) h

theorem CategoryTheory.ModObj.lift_leftSMul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) : CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (leftSMul M X) = CartesianMonoidalCategory.lift (m • x) x

theorem CategoryTheory.ModObj.lift_leftSMul_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M) {Z✝ : C} (h : MonoidalCategoryStruct.tensorObj X X ⟶ Z✝) : CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (CategoryStruct.comp (leftSMul M X) h) = CategoryStruct.comp (CartesianMonoidalCategory.lift (m • x) x) h

theorem CategoryTheory.ModObj.lift_leftSMul_eq_lift_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] (Z : C) (x y : Z ⟶ X) (m : Z ⟶ M) : CategoryStruct.comp (CartesianMonoidalCategory.lift m x) (leftSMul M X) = CartesianMonoidalCategory.lift y x ↔ m • x = y

theorem CategoryTheory.ModObj.isIso_leftSMul_iff {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M : C} [MonObj M] {X : C} [ModObj M X] : IsIso (leftSMul M X) ↔ ∀ (Z : C) (x y : Z ⟶ X), ∃! m : Z ⟶ M, m • x = y

The morphism (m, x) ↦ (m • x, x) is an isomorphism if and only if the induced action is pointwise simply transitive.