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

X : C
act : CategoryTheory.MonoidalCategory.tensorObj A.X s.X ⟶ s.X
one_act : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.one (CategoryTheory.CategoryStruct.id s.X)) s.act = (CategoryTheory.MonoidalCategory.leftUnitor s.X).hom
assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.mul (CategoryTheory.CategoryStruct.id s.X)) s.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X s.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) s.act) s.act)

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

Instances For

@[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.tensorHom A.mul (CategoryTheory.CategoryStruct.id 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.tensorHom (CategoryTheory.CategoryStruct.id A.X) self.act) (CategoryTheory.CategoryStruct.comp self.act h))

source

@[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.tensorHom A.one (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.act h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h

source

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.tensorHom (CategoryTheory.CategoryStruct.id A.X) M.act) M.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X M.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.mul (CategoryTheory.CategoryStruct.id M.X)) M.act)

source

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

source

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

source

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₁

hom : M.X ⟶ N.X
act_hom : CategoryTheory.CategoryStruct.comp M.act s.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) s.hom) N.act

A morphism of module objects.

Instances For

source

@[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.tensorHom (CategoryTheory.CategoryStruct.id A.X) self.hom) (CategoryTheory.CategoryStruct.comp N.act h)

source

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

source

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.

Instances For

source

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)

source

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

source

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.

Instances For

source

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)

source

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₂

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

Inhabited (Mod_ A)

source

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.

Instances For

source

@[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.tensorHom f.hom (CategoryTheory.CategoryStruct.id M.X)) M.act

source

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

source

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

source

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.

Instances For