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.

Instances for Mod
@[simp]
theorem Mod.one_act {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (self : Mod A) :
(A.one 𝟙 self.X) self.act = (λ_ self.X).hom
@[simp]
theorem Mod.assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (self : Mod A) :
(A.mul 𝟙 self.X) self.act = (α_ A.X A.X self.X).hom (𝟙 A.X self.act) self.act
@[simp]
theorem Mod.assoc_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (self : Mod A) {X' : C} (f' : self.X X') :
(A.mul 𝟙 self.X) self.act f' = (α_ A.X A.X self.X).hom (𝟙 A.X self.act) self.act f'
@[simp]
theorem Mod.one_act_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A : Mon_ C} (self : Mod A) {X' : C} (f' : self.X X') :
(A.one 𝟙 self.X) self.act f' = (λ_ self.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.

Instances for Mod.hom
@[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} (self : M.hom N) :
M.act self.hom = (𝟙 A.X self.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} (self : M.hom N) {X' : C} (f' : N.X X') :
M.act self.hom f' = (𝟙 A.X self.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
@[protected, 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
@[protected, 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]
@[protected, 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