The category of module objects over a monoid object.

structure Mod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Type (max u₁ v₁)

A module object for a monoid object, all internal to some monoidal category.

• X : C
• act : CategoryTheory.MonoidalCategory.tensorObj A.X self.X ⟶ self.X
• one_act : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.one self.X) self.act = (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom
• assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul self.X) self.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.act) self.act)

@[simp]

theorem Mod_.assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (self : Mod_ A) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul self.X) (CategoryTheory.CategoryStruct.comp self.act h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.act) (CategoryTheory.CategoryStruct.comp self.act h))

@[simp]

theorem Mod_.one_act_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (self : Mod_ A) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.one self.X) (CategoryTheory.CategoryStruct.comp self.act h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h

theorem Mod_.assoc_flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ A) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X M.act) M.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul M.X) M.act)

theorem Mod_.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} (x y : Mod_.Hom M N), x.hom = y.hom → x = y

theorem Mod_.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A : Mon_ C} {M N : Mod_ A} (x y : Mod_.Hom M N), x = y ↔ x.hom = y.hom

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

A morphism of module objects.

• hom : M.X ⟶ N.X
• act_hom : CategoryTheory.CategoryStruct.comp M.act self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.hom) N.act

@[simp]

theorem Mod_.Hom.act_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} (self : Mod_.Hom M N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.act (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.hom) (CategoryTheory.CategoryStruct.comp N.act h)

@[simp]

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

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

The identity morphism on a module object.

Equations

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

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

Equations

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

@[simp]

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

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

Composition of module object morphisms.

Equations

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

instance Mod_.instCategoryMod_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} : CategoryTheory.Category.{v₁, max u₁ v₁} (Mod_ A)

Equations

• Mod_.instCategoryMod_ = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

@[simp]

theorem Mod_.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} (M : Mod_ 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] {A : Mon_ C} {M : Mod_ A} {N : Mod_ A} {K : Mod_ A} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

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

@[simp]

theorem Mod_.regular_act {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Mod_.regular A).act = A.mul

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

A monoid object as a module over itself.

Equations

• Mod_.regular A = { X := A.X, act := A.mul, one_act := ⋯, assoc := ⋯ }

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

Equations

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

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

The forgetful functor from module objects to the ambient category.

Equations

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

@[simp]

theorem Mod_.comap_obj_act {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A ⟶ B) (M : Mod_ B) : ((Mod_.comap f).obj M).act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.hom M.X) M.act

@[simp]

theorem Mod_.comap_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A ⟶ B) : ∀ {X Y : Mod_ B} (g : X ⟶ Y), ((Mod_.comap f).map g).hom = g.hom

@[simp]

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

def Mod_.comap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (f : A ⟶ B) : CategoryTheory.Functor (Mod_ B) (Mod_ 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.