mathlib documentation

category_theory.monoidal.Mod

The category of module objects over a monoid object.

structure Mod {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (A : Mon_ C) :
Type (max u₁ v₁)

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

@[simp]
theorem Mod.one_act {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (c : Mod A) :
(A.one 𝟙 c.X) c.act = (λ_ c.X).hom

@[simp]
theorem Mod.assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (c : Mod A) :
(A.mul 𝟙 c.X) c.act = (α_ A.X A.X c.X).hom (𝟙 A.X c.act) c.act

@[simp]
theorem Mod.assoc_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (c : Mod A) {X' : C} (f' : c.X X') :
(A.mul 𝟙 c.X) c.act f' = (α_ A.X A.X c.X).hom (𝟙 A.X c.act) c.act f'

@[simp]
theorem Mod.one_act_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (c : Mod A) {X' : C} (f' : c.X X') :
(A.one 𝟙 c.X) c.act f' = (λ_ c.X).hom f'

theorem Mod.assoc_flip {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :
(𝟙 A.X M.act) M.act = (α_ A.X A.X M.X).inv (A.mul 𝟙 M.X) M.act

theorem Mod.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {A : Mon_ C} {M N : Mod A} (x y : M.hom N) :
x = y x.hom = y.hom

theorem Mod.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {A : Mon_ C} {M N : Mod A} (x y : M.hom N) (h : x.hom = y.hom) :
x = y

@[ext]
structure Mod.hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M N : Mod A) :
Type v₁

A morphism of module objects.

@[simp]
theorem Mod.hom.act_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N : Mod A} (c : M.hom N) :
M.act c.hom = (𝟙 A.X c.hom) N.act

@[simp]
theorem Mod.hom.act_hom_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N : Mod A} (c : M.hom N) {X' : C} (f' : N.X X') :
M.act c.hom f' = (𝟙 A.X c.hom) N.act f'

@[simp]
theorem Mod.id_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :
M.id.hom = 𝟙 M.X

def Mod.id {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :
M.hom M

The identity morphism on a module object.

Equations
@[instance]

Equations
def Mod.comp {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N O : Mod A} (f : M.hom N) (g : N.hom O) :
M.hom O

Composition of module object morphisms.

Equations
@[simp]
theorem Mod.comp_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N O : Mod A} (f : M.hom N) (g : N.hom O) :
(Mod.comp f g).hom = f.hom g.hom

@[instance]

Equations
@[simp]
theorem Mod.id_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (M : Mod A) :
(𝟙 M).hom = 𝟙 M.X

@[simp]
theorem Mod.comp_hom' {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} {M N K : Mod A} (f : M N) (g : N K) :
(f g).hom = f.hom g.hom

@[simp]

A monoid object as a module over itself.

Equations
@[simp]

@[instance]

Equations

The forgetful functor from module objects to the ambient category.

Equations
def Mod.comap {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A B) :
Mod B Mod A

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

Equations
@[simp]
theorem Mod.comap_map_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A B) (M N : Mod B) (g : M N) :
((Mod.comap f).map g).hom = g.hom

@[simp]
theorem Mod.comap_obj_X {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A B) (M : Mod B) :
((Mod.comap f).obj M).X = M.X

@[simp]
theorem Mod.comap_obj_act {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A B) (M : Mod B) :
((Mod.comap f).obj M).act = (f.hom 𝟙 M.X) M.act