mathlib3 documentation

category_theory.monoidal.Mod_

The category of module objects over a monoid object. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_.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'
@[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'
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
@[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
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
@[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

A monoid object as a module over itself.

Equations
@[protected, instance]
Equations

The forgetful functor from module objects to the ambient category.

Equations
@[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_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
def Mod_.comap {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {A B : Mon_ C} (f : A B) :

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

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