The category of module objects over a monoid object.

class Mod_Class {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (M : C) [Mon_Class 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 : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X

  The action map

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

  The identity acts trivially.

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

  The action map is compatible with multiplication.

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

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

def Mon_Class.termγ : Lean.ParserDescr

The action map

Equations

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

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

The action map

Equations

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

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

The action map

Equations

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

@[simp]

theorem Mod_Class.one_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [Mon_Class M] (X : D) [Mod_Class M X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) smul = (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom

@[simp]

theorem Mod_Class.one_smul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [Mon_Class M] (X : D) [Mod_Class M X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.one X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h

@[simp]

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

@[simp]

theorem Mod_Class.mul_smul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {M : C} [Mon_Class M] (X : D) [Mod_Class M X] {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft Mon_Class.mul X) (CategoryTheory.CategoryStruct.comp smul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M smul) (CategoryTheory.CategoryStruct.comp smul h))

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

@[reducible, inline]

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

The action of a monoid object on itself.

Equations

• Mod_Class.regular M = { smul := Mon_Class.mul, one_smul' := ⋯, mul_smul' := ⋯ }

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

class IsMod_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class 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 : CategoryTheory.CategoryStruct.comp Mod_Class.smul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f) Mod_Class.smul

@[simp]

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

instance instIsMod_HomId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M : D} [Mod_Class A M] : IsMod_Hom A (CategoryTheory.CategoryStruct.id M)

instance instIsMod_HomComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N O : D} [Mod_Class A M] [Mod_Class A N] [Mod_Class A O] (f : M ⟶ N) (g : N ⟶ O) [IsMod_Hom A f] [IsMod_Hom A g] : IsMod_Hom A (CategoryTheory.CategoryStruct.comp f g)

instance instIsMod_HomInvOfHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class A] {M N : D} [Mod_Class A M] [Mod_Class A N] (f : M ≅ N) [IsMod_Hom A f.hom] : IsMod_Hom A f.inv

structure Mod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (A : C) [Mon_Class 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 : Mod_Class A self.X

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

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

A morphism of module objects.

• hom : M.X ⟶ N.X

  The underlying morphism

• isMod_Hom : IsMod_Hom A self.hom

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

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

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

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

Equations

• Mod_.Hom.mk' f smul_hom = { hom := f, isMod_Hom := ⋯ }

@[simp]

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

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

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

Equations

• Mod_.Hom.mk'' f smul_hom = { hom := f, isMod_Hom := ⋯ }

@[simp]

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

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

The identity morphism on a module object.

Equations

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

@[simp]

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

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

Equations

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

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

Composition of module object morphisms.

Equations

• Mod_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, isMod_Hom := ⋯ }

@[simp]

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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

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

A monoid object as a module over itself.

Equations

• Mod_.regular A = { X := A, mod := Mod_Class.regular A }

@[simp]

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

@[simp]

theorem Mod_.regular_mod_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : C) [Mon_Class A] : Mod_Class.smul = Mon_Class.mul

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

Equations

• Mod_.instInhabited A = { default := Mod_.regular A }

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

The forgetful functor from module objects to the ambient category.

Equations

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

@[simp]

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

@[simp]

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

def Mod_.scalarRestriction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M : D) [Mod_Class B M] : Mod_Class 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 Mod_.scalarRestriction_smul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M : D) [Mod_Class B M] : Mod_Class.smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f M) Mod_Class.smul

theorem Mod_.scalarRestriction_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] (M N : D) [Mod_Class B M] [Mod_Class B N] (g : M ⟶ N) [IsMod_Hom B g] : IsMod_Hom 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 Mod_.comap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] : CategoryTheory.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 Mod_.comap_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] {M N : Mod_ D B} (g : M ⟶ N) : ((comap f).map g).hom = g.hom

@[simp]

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

@[simp]

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