The category of module objects over a monoid object. #

Mod_.instCategory = { Hom := fun (M N : Mod_ A) => M.Hom N, id := Mod_.id, comp := fun {X Y Z : Mod_ A} (f : X.Hom Y) (g : Y.Hom Z) => Mod_.comp f g, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

source

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

f₁ = f₂

source

theorem Mod_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {M N : Mod_ A} {f₁ f₂ : M ⟶ N} :

f₁ = f₂ ↔ f₁.hom = f₂.hom

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 N K : Mod_ A} (f : M ⟶ N) (g : N ⟶ K) :

(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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.

Equations

Mod_.regular A = { X := A.X, smul := A.mul, one_smul := ⋯, assoc := ⋯ }

source

@[simp]

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

(regular A).smul = A.mul

source

@[simp]

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

(regular A).X = A.X

source

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

Inhabited (Mod_ A)

Equations

Mod_.instInhabited A = { default := Mod_.regular 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.

Equations

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

source

def Mod_.comap {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A 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.

source

@[simp]

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

((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 B : Mon_ C} (f : A ⟶ B) (M : Mod_ B) :

((comap f).obj M).X = M.X

source

@[simp]

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

((comap f).obj M).smul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom M.X) M.smul

source

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

Type v₁

An action of a monoid object M on an object X is the data of a map smul : M ⊗ X ⟶ X that satisfies unitality and associativity with multiplication.

See MulAction for the non-categorical version.