The category of module objects over a monoid object.

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

Given an action of a monoidal category C on a category D, an action of an additive monoid object M in C on an object X in D is the data of a map vadd : M ⊙ₗ X ⟶ X that satisfies zero-additivity and associativity with addition.

See AddAction for the non-categorical version.

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

  The action map

• zero_vadd : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft AddMonObj.zero X) vadd = (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

  The zero acts trivially.

• add_vadd : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft AddMonObj.add X) vadd = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M vadd) vadd)

  The action map is compatible with addition.

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.AddModObj.add_vadd_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✝⁴ : AddMonObj M} (X : D) [self : AddModObj M X] {Z : D} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft AddMonObj.add X) (CategoryStruct.comp vadd h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M vadd) (CategoryStruct.comp vadd h))

The action map is compatible with addition.

@[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.AddModObj.zero_vadd_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✝⁴ : AddMonObj M} (X : D) [self : AddModObj M X] {Z : D} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft AddMonObj.zero X) (CategoryStruct.comp vadd h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h

The zero 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.AddMonObj.termδ : Lean.ParserDescr

The action map

Equations

• CategoryTheory.AddMonObj.termδ = Lean.ParserDescr.node `CategoryTheory.AddMonObj.termδ 1024 (Lean.ParserDescr.symbol "δ")

def CategoryTheory.AddMonObj.«termδ[_]» : Lean.ParserDescr

The action map

Equations

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

def CategoryTheory.AddMonObj.«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

• 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)

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

@[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 := ⋯ }

@[reducible, inline]

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

The action of an additive monoid object on itself.

Equations

• CategoryTheory.AddModObj.regular M = { vadd := CategoryTheory.AddMonObj.add, zero_vadd := ⋯, add_vadd := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.AddModObj.vadd_eq_add {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] : vadd = AddMonObj.add

@[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 := ⋯ }

@[implicit_reducible]

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

Equations

• CategoryTheory.AddModObj.instTensorAddUnit X = { vadd := (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom, zero_vadd := ⋯, add_vadd := ⋯ }

@[simp]

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

@[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.AddModObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {X : C} (h₁ h₂ : AddModObj M X) (H : vadd = vadd) : h₁ = h₂

theorem CategoryTheory.AddModObj.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] {X : C} {h₁ h₂ : AddModObj M X} : h₁ = h₂ ↔ vadd = vadd

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

@[implicit_reducible]

def CategoryTheory.ModObj.ofIso {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} {N : C} [MonObj N] (e₁ : M ≅ N) [IsMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [ModObj M X] : ModObj N Y

Transfer a MulActionObj along isomorphisms.

Equations

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

@[implicit_reducible]

def CategoryTheory.AddModObj.ofIso {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {M : C} [AddMonObj M] {X : D} {N : C} [AddMonObj N] (e₁ : M ≅ N) [IsAddMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [AddModObj M X] : AddModObj N Y

Transfer an AddActionObj along isomorphisms.

Equations

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

theorem CategoryTheory.AddModObj.ofIso_vadd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {M : C} [AddMonObj M] {X : D} {N : C} [AddMonObj N] (e₁ : M ≅ N) [IsAddMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [AddModObj M X] : vadd = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv) (CategoryStruct.comp vadd e₂.hom)

theorem CategoryTheory.ModObj.ofIso_smul {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} {N : C} [MonObj N] (e₁ : M ≅ N) [IsMonHom e₁.hom] {Y : D} (e₂ : X ≅ Y) [ModObj M X] : smul = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHom e₁.inv e₂.inv) (CategoryStruct.comp smul e₂.hom)

@[simp]

theorem CategoryTheory.ModObj.one_smul_self {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] (X : C) [ModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.one X) smul = (MonoidalCategoryStruct.leftUnitor X).hom

@[simp]

theorem CategoryTheory.AddModObj.zero_vadd_self {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] (X : C) [AddModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.zero X) vadd = (MonoidalCategoryStruct.leftUnitor X).hom

@[simp]

theorem CategoryTheory.ModObj.one_smul_self_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] (X : C) [ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.one X) (CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h

@[simp]

theorem CategoryTheory.AddModObj.zero_vadd_self_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] (X : C) [AddModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.zero X) (CategoryStruct.comp vadd h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor X).hom h

@[simp]

theorem CategoryTheory.ModObj.mul_smul_self {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] (X : C) [ModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.mul X) smul = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M smul) smul)

@[simp]

theorem CategoryTheory.AddModObj.add_vadd_self {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] (X : C) [AddModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add X) vadd = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M vadd) vadd)

@[simp]

theorem CategoryTheory.ModObj.mul_smul_self_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [MonObj M] (X : C) [ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.mul X) (CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M smul) (CategoryStruct.comp smul h))

@[simp]

theorem CategoryTheory.AddModObj.add_vadd_self_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (M : C) [AddMonObj M] (X : C) [AddModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add X) (CategoryStruct.comp vadd h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M vadd) (CategoryStruct.comp vadd h))

theorem CategoryTheory.ModObj.mul_smul_self_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] (X : C) [ModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M smul) smul = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.mul X) smul)

theorem CategoryTheory.AddModObj.add_vadd_self_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] (X : C) [AddModObj M X] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M vadd) vadd = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add X) vadd)

theorem CategoryTheory.ModObj.mul_smul_self_flip_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [MonObj M] (X : C) [ModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M smul) (CategoryStruct.comp smul h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.mul X) (CategoryStruct.comp smul h))

theorem CategoryTheory.AddModObj.add_vadd_self_flip_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : C} [AddMonObj M] (X : C) [AddModObj M X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M vadd) (CategoryStruct.comp vadd h) = CategoryStruct.comp (MonoidalCategoryStruct.associator M M X).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.add X) (CategoryStruct.comp vadd h))

class CategoryTheory.IsAddModHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {M' N' : D} (A : C) [AddMonObj A] [AddModObj A M'] [AddModObj A N'] (f : M' ⟶ N') : Prop

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

• vadd_hom : CategoryStruct.comp AddModObj.vadd f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) AddModObj.vadd

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.IsAddModHom.vadd_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} {M' N' : D} {A : C} {inst✝⁴ : AddMonObj A} {inst✝⁵ : AddModObj A M'} {inst✝⁶ : AddModObj A N'} {f : M' ⟶ N'} [self : IsAddModHom A f] {Z : D} (h : N' ⟶ Z) : CategoryStruct.comp AddModObj.vadd (CategoryStruct.comp f h) = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) (CategoryStruct.comp AddModObj.vadd h)

@[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.instIsAddModHomId {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [AddMonObj A] {M : D} [AddModObj A M] : IsAddModHom 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.instIsAddModHomComp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [AddMonObj A] {M N O : D} [AddModObj A M] [AddModObj A N] [AddModObj A O] (f : M ⟶ N) (g : N ⟶ O) [IsAddModHom A f] [IsAddModHom A g] : IsAddModHom 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

instance CategoryTheory.instIsAddModHomNegOfHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [AddMonObj A] {M N : D} [AddModObj A M] [AddModObj A N] (f : M ≅ N) [IsAddModHom A f.hom] : IsAddModHom A f.inv

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

An additive module object for an additive monoid object in a monoidal category acting on the ambient category.

• X : D

  The underlying object in the ambient category

• addMod : AddModObj A self.X

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

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

A morphism of additive module objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• isAddModHom : IsAddModHom A self.hom

theorem CategoryTheory.AddMod.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✝⁴ : AddMonObj A} {M N : AddMod D A} {x y : M.Hom N} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.AddMod.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✝⁴ : AddMonObj A} {M N : AddMod D A} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

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)

theorem CategoryTheory.AddMod.assoc_flip {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] (M : AddMod D A) : CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A AddModObj.vadd) AddModObj.vadd = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv (CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft AddMonObj.add M.X) AddModObj.vadd)

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 {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

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

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 := ⋯ }

def CategoryTheory.AddMod.Hom.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] {M N : AddMod D A} (f : M.X ⟶ N.X) (vadd_hom : CategoryStruct.comp AddModObj.vadd f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) AddModObj.vadd := by cat_disch) : M.Hom N

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

Equations

• CategoryTheory.AddMod.Hom.mk' f smul_hom = { hom := f, isAddModHom := ⋯ }

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

@[simp]

theorem CategoryTheory.AddMod.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} [AddMonObj A] {M N : AddMod D A} (f : M.X ⟶ N.X) (vadd_hom : CategoryStruct.comp AddModObj.vadd f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) AddModObj.vadd := by cat_disch) : (mk' f vadd_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 := ⋯ }

def CategoryTheory.AddMod.Hom.mk'' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] {M N : D} [AddModObj A M] [AddModObj A N] (f : M ⟶ N) (vadd_hom : CategoryStruct.comp AddModObj.vadd f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) AddModObj.vadd := by cat_disch) : { X := M, addMod := inst✝ }.Hom { X := N, addMod := inst✝¹ }

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

Equations

• CategoryTheory.AddMod.Hom.mk'' f smul_hom = { hom := f, isAddModHom := ⋯ }

@[simp]

theorem CategoryTheory.AddMod.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} [AddMonObj A] {M N : D} [AddModObj A M] [AddModObj A N] (f : M ⟶ N) (vadd_hom : CategoryStruct.comp AddModObj.vadd f = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) AddModObj.vadd := by cat_disch) : (mk'' f vadd_hom).hom = f

@[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 := ⋯ }

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

The identity morphism on an additive module object.

Equations

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

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

@[simp]

theorem CategoryTheory.AddMod.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] (M : AddMod 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 }

@[implicit_reducible]

instance CategoryTheory.AddMod.homInhabited {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] (M : AddMod 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 := ⋯ }

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

Composition of additive module object morphisms.

Equations

• CategoryTheory.AddMod.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isAddModHom := ⋯ }

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

@[simp]

theorem CategoryTheory.AddMod.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] {M N O : AddMod 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.

@[implicit_reducible]

instance CategoryTheory.AddMod.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] : Category.{v₂, max u₂ v₂} (AddMod 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.AddMod.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] {M N : AddMod 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

theorem CategoryTheory.AddMod.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} [AddMonObj A] {M N : AddMod 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.AddMod.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] (M : AddMod 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

@[simp]

theorem CategoryTheory.AddMod.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A : C} [AddMonObj A] {M N K : AddMod 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 }

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

An additive monoid object as an additive module over itself.

Equations

• CategoryTheory.AddMod.regular A = { X := A, addMod := CategoryTheory.AddModObj.regular A }

@[simp]

theorem CategoryTheory.Mod.regular_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : (regular A).X = 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.AddMod.regular_addMod_vadd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [AddMonObj A] : AddModObj.vadd = AddMonObj.add

@[simp]

theorem CategoryTheory.AddMod.regular_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [AddMonObj 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 }

@[implicit_reducible]

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

Equations

• CategoryTheory.AddMod.instInhabited A = { default := CategoryTheory.AddMod.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 := ⋯ }

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

The forgetful functor from additive module objects to the ambient category.

Equations

• CategoryTheory.AddMod.forget A = { obj := fun (A_1 : CategoryTheory.AddMod D A) => A_1.X, map := fun {X Y : CategoryTheory.AddMod 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.AddMod.forget_obj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] (A : C) [AddMonObj A] (A✝ : AddMod D A) : (forget A).obj A✝ = A✝.X

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

@[simp]

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

@[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 ⊵ₗ M ≫ γ[B, M].

Equations

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

@[implicit_reducible]

def CategoryTheory.AddMod.scalarRestriction {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] (M : D) [AddModObj B M] : AddModObj A M

When M is a B-additive module in D and f : A ⟶ B is a morphism of internal additive monoid objects, M inherits an A-additive module structure via "restriction of scalars", i.e δ[A, M] = f ⊵ₗ 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

@[simp]

theorem CategoryTheory.AddMod.scalarRestriction_vadd {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] (M : D) [AddModObj B M] : AddModObj.vadd = CategoryStruct.comp (MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M) AddModObj.vadd

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

theorem CategoryTheory.AddMod.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} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] (M N : D) [AddModObj B M] [AddModObj B N] (g : M ⟶ N) [IsAddModHom B g] : IsAddModHom A g

If g : M ⟶ N is a B-linear morphism of B-modules, then it induces an A-linear morphism when M and N have an A-module structure obtained by restricting scalars along an additive 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.

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

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

Equations

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

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

@[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.AddMod.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} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] (M : AddMod D B) : ((comap f).obj M).X = M.X

@[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.AddMod.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} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] {M N : AddMod D B} (g : M ⟶ N) : ((comap f).map g).hom = g.hom

@[simp]

theorem CategoryTheory.AddMod.comap_obj_addMod {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory.MonoidalLeftAction C D] {A B : C} [AddMonObj A] [AddMonObj B] (f : A ⟶ B) [IsAddMonHom f] (M : AddMod D B) : ((comap f).obj M).addMod = 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 ⊵ₗ 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 morphism 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