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₁)
A module object for a monoid object, all internal to some monoidal category.
- X : C
- act : CategoryTheory.MonoidalCategory.tensorObj A.X self.X ⟶ self.X
- one_act : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.one self.X) self.act = (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom
- assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul self.X) self.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.act) self.act)
Instances For
@[simp]
theorem
Mod_.one_act
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(self : Mod_ A)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.one self.X) self.act = (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom
@[simp]
theorem
Mod_.assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(self : Mod_ A)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul self.X) self.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X self.X).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.act) self.act)
@[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)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.one self.X)
(CategoryTheory.CategoryStruct.comp self.act h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h
@[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.whiskerRight A.mul 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.whiskerLeft A.X self.act)
(CategoryTheory.CategoryStruct.comp self.act h))
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.whiskerLeft A.X M.act) M.act = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X M.X).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.mul 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 : M.Hom 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 : M.Hom 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₁
A morphism of module objects.
- hom : M.X ⟶ N.X
- act_hom : CategoryTheory.CategoryStruct.comp M.act self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.hom) N.act
Instances For
@[simp]
theorem
Mod_.Hom.act_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
{M : Mod_ A}
{N : Mod_ A}
(self : M.Hom N)
:
CategoryTheory.CategoryStruct.comp M.act self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.hom) N.act
@[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 : M.Hom N)
{Z : C}
(h : N.X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp M.act (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X self.hom)
(CategoryTheory.CategoryStruct.comp N.act h)
@[simp]
theorem
Mod_.id_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(M : Mod_ A)
:
M.id.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)
:
M.Hom M
The identity morphism on a module object.
Equations
- M.id = { hom := CategoryTheory.CategoryStruct.id M.X, act_hom := ⋯ }
Instances For
instance
Mod_.homInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
(M : Mod_ A)
:
Inhabited (M.Hom M)
Equations
- M.homInhabited = { default := M.id }
@[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 : M.Hom N)
(g : N.Hom O)
:
(Mod_.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
def
Mod_.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
{M : Mod_ A}
{N : Mod_ A}
{O : Mod_ A}
(f : M.Hom N)
(g : N.Hom O)
:
M.Hom O
Composition of module object morphisms.
Equations
- Mod_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, act_hom := ⋯ }
Instances For
instance
Mod_.instCategory
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
{A : Mon_ C}
:
Equations
- Mod_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
theorem
Mod_.hom_ext_iff
{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}
:
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_act
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
(Mod_.regular A).act = A.mul
@[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
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, act := A.mul, one_act := ⋯, assoc := ⋯ }
Instances For
instance
Mod_.instInhabited
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(A : Mon_ C)
:
Equations
- Mod_.instInhabited A = { default := Mod_.regular A }
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 := ⋯ }
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.whiskerRight f.hom M.X) M.act
@[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
@[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
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.
Equations
- One or more equations did not get rendered due to their size.