The category of module objects over a monoid object.

class CategoryTheory.ModObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (M : C) [MonObj M] (X : D) : Type v₂

Given an action of a monoidal category C on a category D, an action of a monoid object M in C on an object X in D is the data of a map smul : M ⊙ₗ X ⟶ X that satisfies unitality and associativity with multiplication.

See MulAction for the non-categorical version.

• smul : MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X

  The action map

• one_smul : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.one X) smul = (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

  The identity acts trivially.

• mul_smul : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X) smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul)

  The action map is compatible with multiplication.

@[simp]

theorem CategoryTheory.ModObj.one_smul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : MonObj M} (X : D) [self : ModObj M X] {Z : D} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.one X) (CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h

The identity acts trivially.

@[simp]

theorem CategoryTheory.ModObj.mul_smul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {M : C} {inst✝⁴ : MonObj M} (X : D) [self : ModObj M X] {Z : D} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X) (CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) (CategoryStruct.comp smul h))

The action map is compatible with multiplication.

def CategoryTheory.MonObj.termγ : Lean.ParserDescr

The action map

Equations

• CategoryTheory.MonObj.termγ = Lean.ParserDescr.node `CategoryTheory.MonObj.termγ 1024 (Lean.ParserDescr.symbol "γ")

def CategoryTheory.MonObj.«termγ[_]» : Lean.ParserDescr

The action map

Equations

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

def CategoryTheory.MonObj.«termγ[_,_]» : Lean.ParserDescr

The action map

Equations

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

theorem CategoryTheory.ModObj.assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {M : C} [MonObj M] (X : D) [ModObj M X] : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).inv (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul X) smul)

@[reducible, inline]

abbrev CategoryTheory.ModObj.regular {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] : ModObj M M

The action of a monoid object on itself.

Equations

• CategoryTheory.ModObj.regular M = { smul := CategoryTheory.MonObj.mul, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem CategoryTheory.ModObj.smul_eq_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] : smul = MonObj.mul

@[implicit_reducible]

instance CategoryTheory.ModObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (X : D) : ModObj (MonoidalCategoryStruct.tensorUnit C) X

If C acts monoidally on D, then every object of D is canonically a module over the trivial monoid.

Equations

• CategoryTheory.ModObj.instTensorUnit X = { smul := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, one_smul := ⋯, mul_smul := ⋯ }

@[simp]

theorem CategoryTheory.ModObj.smul_def {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (X : D) : smul = (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

theorem CategoryTheory.ModObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {X : C} (h₁ h₂ : ModObj M X) (H : smul = smul) : h₁ = h₂

theorem CategoryTheory.ModObj.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] {X : C} {h₁ h₂ : ModObj M X} : h₁ = h₂ ↔ smul = smul

class CategoryTheory.IsModHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ⟶ N) : Prop

A morphism in D is a morphism of A-module objects if it commutes with the action maps

• smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul

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

def CategoryTheory.IsMod_Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ⟶ N) : Prop

Alias of CategoryTheory.IsModHom.

---

A morphism in D is a morphism of A-module objects if it commutes with the action maps

Equations

• @CategoryTheory.IsMod_Hom = @CategoryTheory.IsModHom

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

theorem CategoryTheory.IsMod_Hom.smul_hom {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : D} {inst✝⁵ : ModObj A M} {inst✝⁶ : ModObj A N} {f : M ⟶ N} [self : IsModHom A f] : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul

Alias of CategoryTheory.IsModHom.smul_hom.

@[simp]

theorem CategoryTheory.IsModHom.smul_hom_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : D} {inst✝⁵ : ModObj A M} {inst✝⁶ : ModObj A N} {f : M ⟶ N} [self : IsModHom A f] {Z : D} (h : N ⟶ Z) : CategoryStruct.comp ModObj.smul (CategoryStruct.comp f h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) (CategoryStruct.comp ModObj.smul h)

instance CategoryTheory.instIsModHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {M : D} [ModObj A M] : IsModHom A (CategoryStruct.id M)

instance CategoryTheory.instIsModHomComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {M N O : D} [ModObj A M] [ModObj A N] [ModObj A O] (f : M ⟶ N) (g : N ⟶ O) [IsModHom A f] [IsModHom A g] : IsModHom A (CategoryStruct.comp f g)

instance CategoryTheory.instIsModHomInvOfHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ≅ N) [IsModHom A f.hom] : IsModHom A f.inv

structure CategoryTheory.Mod {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] : Type (max u₂ v₂)

A module object for a monoid object in a monoidal category acting on the ambient category.

• X : D

  The underlying object in the ambient category

• mod : ModObj A self.X

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

def CategoryTheory.Mod_ {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (D : Type u₂) [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] : Type (max u₂ v₂)

Alias of CategoryTheory.Mod.

---

A module object for a monoid object in a monoidal category acting on the ambient category.

Equations

• @CategoryTheory.Mod_ = @CategoryTheory.Mod

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

def CategoryTheory.Mod_.mod {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (self : Mod D A) : ModObj A self.X

Alias of CategoryTheory.Mod.mod.

Equations

• @CategoryTheory.Mod_.mod = @CategoryTheory.Mod.mod

theorem CategoryTheory.Mod.assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A ModObj.smul) ModObj.smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul M.X) ModObj.smul)

structure CategoryTheory.Mod.Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M N : Mod D A) : Type v₂

A morphism of module objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• isModHom : IsModHom A self.hom

theorem CategoryTheory.Mod.Hom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : Mod D A} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Mod.Hom.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {D : Type u₂} {inst✝² : Category.{v₂, u₂} D} {inst✝³ : MonoidalCategory.MonoidalLeftAction C D} {A : C} {inst✝⁴ : MonObj A} {M N : Mod D A} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

def CategoryTheory.Mod.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} (f : M.X ⟶ N.X) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : M.Hom N

An alternative constructor for Hom, taking a morphism without a [IsModHom] instance, as well as the relevant equality to put such an instance.

Equations

• CategoryTheory.Mod.Hom.mk' f smul_hom = { hom := f, isModHom := ⋯ }

@[simp]

theorem CategoryTheory.Mod.Hom.mk'_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} (f : M.X ⟶ N.X) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : (mk' f smul_hom).hom = f

def CategoryTheory.Mod.Hom.mk'' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ⟶ N) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : { X := M, mod := inst✝ }.Hom { X := N, mod := inst✝¹ }

An alternative constructor for Hom, taking a morphism without a [IsModHom] instance, between objects with a ModObj instance (rather than bundled as Mod), as well as the relevant equality to put such an instance.

Equations

• CategoryTheory.Mod.Hom.mk'' f smul_hom = { hom := f, isModHom := ⋯ }

@[simp]

theorem CategoryTheory.Mod.Hom.mk''_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ⟶ N) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : (mk'' f smul_hom).hom = f

def CategoryTheory.Mod.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : M.Hom M

The identity morphism on a module object.

Equations

• M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isModHom := ⋯ }

@[simp]

theorem CategoryTheory.Mod.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : M.id.hom = CategoryStruct.id M.X

@[implicit_reducible]

instance CategoryTheory.Mod.homInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : Inhabited (M.Hom M)

Equations

• M.homInhabited = { default := M.id }

def CategoryTheory.Mod.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N O : Mod D A} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Composition of module object morphisms.

Equations

• CategoryTheory.Mod.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isModHom := ⋯ }

@[simp]

theorem CategoryTheory.Mod.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N O : Mod D A} (f : M.Hom N) (g : N.Hom O) : (comp f g).hom = CategoryStruct.comp f.hom g.hom

@[implicit_reducible]

instance CategoryTheory.Mod.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] : Category.{v₂, max u₂ v₂} (Mod D A)

Equations

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

theorem CategoryTheory.Mod.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} (f₁ f₂ : M ⟶ N) (h : f₁.hom = f₂.hom) : f₁ = f₂

theorem CategoryTheory.Mod.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} {f₁ f₂ : M ⟶ N} : f₁ = f₂ ↔ f₁.hom = f₂.hom

@[simp]

theorem CategoryTheory.Mod.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

@[simp]

theorem CategoryTheory.Mod.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N K : Mod D A} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

def CategoryTheory.Mod.regular {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : Mod C A

A monoid object as a module over itself.

Equations

• CategoryTheory.Mod.regular A = { X := A, mod := CategoryTheory.ModObj.regular A }

@[simp]

theorem CategoryTheory.Mod.regular_mod_smul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : ModObj.smul = MonObj.mul

@[simp]

theorem CategoryTheory.Mod.regular_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : (regular A).X = A

@[implicit_reducible]

instance CategoryTheory.Mod.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : Inhabited (Mod C A)

Equations

• CategoryTheory.Mod.instInhabited A = { default := CategoryTheory.Mod.regular A }

def CategoryTheory.Mod.forget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] : Functor (Mod D A) D

The forgetful functor from module objects to the ambient category.

Equations

• CategoryTheory.Mod.forget A = { obj := fun (A_1 : CategoryTheory.Mod D A) => A_1.X, map := fun {X Y : CategoryTheory.Mod D A} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Mod.forget_map {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] {X✝ Y✝ : Mod D A} (f : X✝ ⟶ Y✝) : (forget A).map f = f.hom

@[simp]

theorem CategoryTheory.Mod.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] (A✝ : Mod D A) : (forget A).obj A✝ = A✝.X

@[implicit_reducible]

def CategoryTheory.Mod.scalarRestriction {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M : D) [ModObj B M] : ModObj A M

When M is a B-module in D and f : A ⟶ B is a morphism of internal monoid objects, M inherits an A-module structure via "restriction of scalars", i.e γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M].

Equations

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

@[simp]

theorem CategoryTheory.Mod.scalarRestriction_smul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M : D) [ModObj B M] : ModObj.smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M) ModObj.smul

theorem CategoryTheory.Mod.scalarRestriction_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M N : D) [ModObj B M] [ModObj B N] (g : M ⟶ N) [IsModHom B g] : IsModHom A g

If g : M ⟶ N is a B-linear morphisms of B-modules, then it induces an A-linear morphism when M and N have an A-module structure obtained by restricting scalars along a monoid morphism A ⟶ B.

def CategoryTheory.Mod.comap {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] : Functor (Mod D B) (Mod D A)

A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.

Equations

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

@[simp]

theorem CategoryTheory.Mod.comap_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M : Mod D B) : ((comap f).obj M).X = M.X

@[simp]

theorem CategoryTheory.Mod.comap_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] {M N : Mod D B} (g : M ⟶ N) : ((comap f).map g).hom = g.hom

@[simp]

theorem CategoryTheory.Mod.comap_obj_mod {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M : Mod D B) : ((comap f).obj M).mod = scalarRestriction f M.X

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

theorem CategoryTheory.Mod_.assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A ModObj.smul) ModObj.smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft MonObj.mul M.X) ModObj.smul)

Alias of CategoryTheory.Mod.assoc_flip.

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

def CategoryTheory.Mod_.Hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M N : Mod D A) : Type v₂

Alias of CategoryTheory.Mod.Hom.

---

A morphism of module objects.

Equations

• @CategoryTheory.Mod_.Hom = @CategoryTheory.Mod.Hom

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

def CategoryTheory.Mod_.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} (f : M.X ⟶ N.X) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : M.Hom N

Alias of CategoryTheory.Mod.Hom.mk'.

---

An alternative constructor for Hom, taking a morphism without a [IsModHom] instance, as well as the relevant equality to put such an instance.

Equations

• @CategoryTheory.Mod_.Hom.mk' = @CategoryTheory.Mod.Hom.mk'

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

def CategoryTheory.Mod_.Hom.mk'' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : D} [ModObj A M] [ModObj A N] (f : M ⟶ N) (smul_hom : CategoryStruct.comp ModObj.smul f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) ModObj.smul := by cat_disch) : { X := M, mod := inst✝ }.Hom { X := N, mod := inst✝¹ }

Alias of CategoryTheory.Mod.Hom.mk''.

---

An alternative constructor for Hom, taking a morphism without a [IsModHom] instance, between objects with a ModObj instance (rather than bundled as Mod), as well as the relevant equality to put such an instance.

Equations

• @CategoryTheory.Mod_.Hom.mk'' = @CategoryTheory.Mod.Hom.mk''

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

def CategoryTheory.Mod_.id {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : M.Hom M

Alias of CategoryTheory.Mod.id.

---

The identity morphism on a module object.

Equations

• @CategoryTheory.Mod_.id = @CategoryTheory.Mod.id

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

def CategoryTheory.Mod_.comp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N O : Mod D A} (f : M.Hom N) (g : N.Hom O) : M.Hom O

Alias of CategoryTheory.Mod.comp.

---

Composition of module object morphisms.

Equations

• @CategoryTheory.Mod_.comp = @CategoryTheory.Mod.comp

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

theorem CategoryTheory.Mod_.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N : Mod D A} (f₁ f₂ : M ⟶ N) (h : f₁.hom = f₂.hom) : f₁ = f₂

Alias of CategoryTheory.Mod.hom_ext.

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

theorem CategoryTheory.Mod_.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] (M : Mod D A) : (CategoryStruct.id M).hom = CategoryStruct.id M.X

Alias of CategoryTheory.Mod.id_hom'.

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

theorem CategoryTheory.Mod_.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [MonObj A] {M N K : Mod D A} (f : M ⟶ N) (g : N ⟶ K) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

Alias of CategoryTheory.Mod.comp_hom'.

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

def CategoryTheory.Mod_.regular {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : Mod C A

Alias of CategoryTheory.Mod.regular.

---

A monoid object as a module over itself.

Equations

• @CategoryTheory.Mod_.regular = @CategoryTheory.Mod.regular

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

def CategoryTheory.Mod_.forget {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [MonObj A] : Functor (Mod D A) D

Alias of CategoryTheory.Mod.forget.

---

The forgetful functor from module objects to the ambient category.

Equations

• @CategoryTheory.Mod_.forget = @CategoryTheory.Mod.forget

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

def CategoryTheory.Mod_.scalarRestriction {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M : D) [ModObj B M] : ModObj A M

Alias of CategoryTheory.Mod.scalarRestriction.

---

When M is a B-module in D and f : A ⟶ B is a morphism of internal monoid objects, M inherits an A-module structure via "restriction of scalars", i.e γ[A, M] = f.hom ⊵ₗ M ≫ γ[B, M].

Equations

• @CategoryTheory.Mod_.scalarRestriction = @CategoryTheory.Mod.scalarRestriction

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

theorem CategoryTheory.Mod_.scalarRestriction_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] (M N : D) [ModObj B M] [ModObj B N] (g : M ⟶ N) [IsModHom B g] : IsModHom A g

Alias of CategoryTheory.Mod.scalarRestriction_hom.

---

If g : M ⟶ N is a B-linear morphisms of B-modules, then it induces an A-linear morphism when M and N have an A-module structure obtained by restricting scalars along a monoid morphism A ⟶ B.

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

def CategoryTheory.Mod_.comap {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] : Functor (Mod D B) (Mod D A)

Alias of CategoryTheory.Mod.comap.

---

A morphism of monoid objects induces a "restriction" or "comap" functor between the categories of module objects.

Equations

• @CategoryTheory.Mod_.comap = @CategoryTheory.Mod.comap