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))
@[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)
:
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)
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
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
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
@[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)
:
@[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
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
instance
Mod_.homInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(M : Mod_ A)
:
@[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
instance
Mod_.instCategoryMod_
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
:
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₂
@[simp]
theorem
Mod_.id_hom'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(M : Mod_ A)
:
@[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
@[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
@[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
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
instance
Mod_.instInhabitedMod_
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
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
@[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
@[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
@[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
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.