Endofunctors as a monoidal category. #
We give the monoidal category structure on C ⥤ C,
and show that when C itself is monoidal, it embeds via a monoidal functor into C ⥤ C.
TODO #
Can we use this to show coherence results, e.g. a cheap proof that λ_ (𝟙_ C) = ρ_ (𝟙_ C)?
I suspect this is harder than is usually made out.
def
CategoryTheory.endofunctorMonoidalCategory
(C : Type u)
[Category.{v, u} C]
:
MonoidalCategory (Functor C C)
The category of endofunctors of any category is a monoidal category, with tensor product given by composition of functors (and horizontal composition of natural transformations).
Equations
- CategoryTheory.endofunctorMonoidalCategory C = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorUnit_obj
(C : Type u)
[Category.{v, u} C]
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map
(C : Type u)
[Category.{v, u} C]
{X Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorObj_obj
(C : Type u)
[Category.{v, u} C]
(F G : Functor C C)
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorObj_map
(C : Type u)
[Category.{v, u} C]
(F G : Functor C C)
{X Y : C}
(f : X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorMap_app
(C : Type u)
[Category.{v, u} C]
{F G H K : Functor C C}
{α : F ⟶ G}
{β : H ⟶ K}
(X : C)
:
(MonoidalCategoryStruct.tensorHom α β).app X = CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_whiskerLeft_app
(C : Type u)
[Category.{v, u} C]
{F H K : Functor C C}
{β : H ⟶ K}
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_whiskerRight_app
(C : Type u)
[Category.{v, u} C]
{F G H : Functor C C}
{α : F ⟶ G}
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_associator_hom_app
(C : Type u)
[Category.{v, u} C]
(F G H : Functor C C)
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_associator_inv_app
(C : Type u)
[Category.{v, u} C]
(F G H : Functor C C)
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_leftUnitor_hom_app
(C : Type u)
[Category.{v, u} C]
(F : Functor C C)
(X : C)
:
(MonoidalCategoryStruct.leftUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (𝟙_ (Functor C C)) F).obj X)
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_leftUnitor_inv_app
(C : Type u)
[Category.{v, u} C]
(F : Functor C C)
(X : C)
:
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_rightUnitor_hom_app
(C : Type u)
[Category.{v, u} C]
(F : Functor C C)
(X : C)
:
(MonoidalCategoryStruct.rightUnitor F).hom.app X = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj F (𝟙_ (Functor C C))).obj X)
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_rightUnitor_inv_app
(C : Type u)
[Category.{v, u} C]
(F : Functor C C)
(X : C)
:
instance
CategoryTheory.MonoidalCategory.instMonoidalFunctorTensoringRight
(C : Type u)
[Category.{v, u} C]
[MonoidalCategory C]
:
Tensoring on the right gives a monoidal functor from C into endofunctors of C.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.MonoidalCategory.tensoringRight_ε
(C : Type u)
[Category.{v, u} C]
[MonoidalCategory C]
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.tensoringRight_η
(C : Type u)
[Category.{v, u} C]
[MonoidalCategory C]
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.tensoringRight_μ
(C : Type u)
[Category.{v, u} C]
[MonoidalCategory C]
(X Y Z : C)
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.tensoringRight_δ
(C : Type u)
[Category.{v, u} C]
[MonoidalCategory C]
(X Y Z : C)
:
@[simp]
theorem
CategoryTheory.μ_δ_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(i j : M)
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) ((Functor.OplaxMonoidal.δ F i j).app X) = CategoryStruct.id ((MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X)
@[simp]
theorem
CategoryTheory.μ_δ_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(i j : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (MonoidalCategoryStruct.tensorObj (F.obj i) (F.obj j)).obj X ⟶ Z)
:
CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) h) = h
@[simp]
theorem
CategoryTheory.δ_μ_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(i j : M)
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X) ((Functor.LaxMonoidal.μ F i j).app X) = CategoryStruct.id ((F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X)
@[simp]
theorem
CategoryTheory.δ_μ_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(i j : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj i j)).obj X ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F i j).app X)
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F i j).app X) h) = h
@[simp]
theorem
CategoryTheory.ε_η_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.id ((𝟙_ (Functor C C)).obj X)
@[simp]
theorem
CategoryTheory.ε_η_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(X : C)
[F.Monoidal]
{Z : C}
(h : (𝟙_ (Functor C C)).obj X ⟶ Z)
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) h) = h
@[simp]
theorem
CategoryTheory.η_ε_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.id ((F.obj (𝟙_ M)).obj X)
@[simp]
theorem
CategoryTheory.η_ε_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj (𝟙_ M)).obj X ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) h) = h
@[simp]
theorem
CategoryTheory.ε_naturality
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{X Y : C}
(f : X ⟶ Y)
[F.LaxMonoidal]
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) ((F.obj (𝟙_ M)).map f) = CategoryStruct.comp f ((Functor.LaxMonoidal.ε F).app Y)
@[simp]
theorem
CategoryTheory.ε_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{X Y : C}
(f : X ⟶ Y)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (𝟙_ M)).obj Y ⟶ Z)
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X) (CategoryStruct.comp ((F.obj (𝟙_ M)).map f) h) = CategoryStruct.comp f (CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app Y) h)
@[simp]
theorem
CategoryTheory.η_naturality
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{X Y : C}
(f : X ⟶ Y)
[F.OplaxMonoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) ((𝟙_ (Functor C C)).map f) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) f
@[simp]
theorem
CategoryTheory.η_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{X Y : C}
(f : X ⟶ Y)
[F.OplaxMonoidal]
{Z : C}
(h : (𝟙_ (Functor C C)).obj Y ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp ((𝟙_ (Functor C C)).map f) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X) (CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.μ_naturality
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) ((Functor.LaxMonoidal.μ F m n).app Y) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f)
@[simp]
theorem
CategoryTheory.μ_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m n)).obj Y ⟶ Z)
:
CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app Y) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X)
(CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) h)
theorem
CategoryTheory.δ_naturality
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
[F.OplaxMonoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.obj m).map f)) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f) ((Functor.OplaxMonoidal.δ F m n).app Y)
theorem
CategoryTheory.δ_naturality_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n : M}
{X Y : C}
(f : X ⟶ Y)
[F.OplaxMonoidal]
{Z : C}
(h : (F.obj n).obj ((F.obj m).obj Y) ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.obj m).map f)) h) = CategoryStruct.comp ((F.obj (MonoidalCategoryStruct.tensorObj m n)).map f)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app Y) h)
theorem
CategoryTheory.μ_naturality₂
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' n' : M}
(f : m ⟶ m')
(g : n ⟶ n')
(X : C)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
(CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n').app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X)
theorem
CategoryTheory.μ_naturality₂_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' n' : M}
(f : m ⟶ m')
(g : n ⟶ n')
(X : C)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m' n')).obj X ⟶ Z)
:
CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
(CategoryStruct.comp ((F.obj n').map ((F.map f).app X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n').app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.tensorHom f g)).app X) h)
@[simp]
theorem
CategoryTheory.μ_naturalityₗ
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) ((Functor.LaxMonoidal.μ F m' n).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X)
@[simp]
theorem
CategoryTheory.μ_naturalityₗ_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m' n)).obj X ⟶ Z)
:
CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m' n).app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) h)
@[simp]
theorem
CategoryTheory.μ_naturalityᵣ
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) ((Functor.LaxMonoidal.μ F m n').app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X) ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X)
@[simp]
theorem
CategoryTheory.μ_naturalityᵣ_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m n')).obj X ⟶ Z)
:
CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n').app X) h) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) h)
@[simp]
theorem
CategoryTheory.δ_naturalityₗ
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
[F.OplaxMonoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.obj n).map ((F.map f).app X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X) ((Functor.OplaxMonoidal.δ F m' n).app X)
@[simp]
theorem
CategoryTheory.δ_naturalityₗ_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n m' : M}
(f : m ⟶ m')
(X : C)
[F.OplaxMonoidal]
{Z : C}
(h : (F.obj n).obj ((F.obj m').obj X) ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.obj n).map ((F.map f).app X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerRight f n)).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m' n).app X) h)
@[simp]
theorem
CategoryTheory.δ_naturalityᵣ
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
[F.OplaxMonoidal]
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) ((F.map g).app ((F.obj m).obj X)) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X) ((Functor.OplaxMonoidal.δ F m n').app X)
@[simp]
theorem
CategoryTheory.δ_naturalityᵣ_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m n n' : M}
(g : n ⟶ n')
(X : C)
[F.OplaxMonoidal]
{Z : C}
(h : (F.obj n').obj ((F.obj m).obj X) ⟶ Z)
:
CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n).app X) (CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.whiskerLeft m g)).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m n').app X) h)
theorem
CategoryTheory.left_unitality_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X)
((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)) = CategoryStruct.id ((F.obj n).obj ((𝟙_ (Functor C C)).obj X))
theorem
CategoryTheory.left_unitality_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj n).obj X ⟶ Z)
:
CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)) = h
@[simp]
theorem
CategoryTheory.obj_ε_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
:
(F.obj n).map ((Functor.LaxMonoidal.ε F).app X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X)
((Functor.OplaxMonoidal.δ F (𝟙_ M) n).app X)
theorem
CategoryTheory.obj_ε_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj n).obj ((F.obj (𝟙_ M)).obj X) ⟶ Z)
:
CategoryStruct.comp ((F.obj n).map ((Functor.LaxMonoidal.ε F).app X)) h = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).inv).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (𝟙_ M) n).app X) h)
@[simp]
theorem
CategoryTheory.obj_η_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
:
(F.obj n).map ((Functor.OplaxMonoidal.η F).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X)
((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X)
theorem
CategoryTheory.obj_η_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj n).obj ((𝟙_ (Functor C C)).obj X) ⟶ Z)
:
CategoryStruct.comp ((F.obj n).map ((Functor.OplaxMonoidal.η F).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) n).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor n).hom).app X) h)
theorem
CategoryTheory.right_unitality_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X)
((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)) = CategoryStruct.id ((𝟙_ (Functor C C)).obj ((F.obj n).obj X))
theorem
CategoryTheory.right_unitality_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj n).obj X ⟶ Z)
:
CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app ((F.obj n).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X) h)) = h
@[simp]
theorem
CategoryTheory.ε_app_obj
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
:
(Functor.LaxMonoidal.ε F).app ((F.obj n).obj X) = CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor n).inv).app X)
((Functor.OplaxMonoidal.δ F n (𝟙_ M)).app X)
@[simp]
theorem
CategoryTheory.η_app_obj
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(n : M)
(X : C)
[F.Monoidal]
:
(Functor.OplaxMonoidal.η F).app ((F.obj n).obj X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F n (𝟙_ M)).app X)
((F.map (MonoidalCategoryStruct.rightUnitor n).hom).app X)
theorem
CategoryTheory.associativity_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.LaxMonoidal]
:
CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
theorem
CategoryTheory.associativity_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.LaxMonoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃))).obj X ⟶ Z)
:
CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X) h)) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X) h)
@[simp]
theorem
CategoryTheory.obj_μ_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.Monoidal]
:
(F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X)
((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)))
theorem
CategoryTheory.obj_μ_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj m₃).obj ((F.obj (MonoidalCategoryStruct.tensorObj m₁ m₂)).obj X) ⟶ Z)
:
CategoryStruct.comp ((F.obj m₃).map ((Functor.LaxMonoidal.μ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₂ m₃).app ((F.obj m₁).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).inv).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X) h)))
@[simp]
theorem
CategoryTheory.obj_μ_inv_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.Monoidal]
:
(F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X))))
theorem
CategoryTheory.obj_μ_inv_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ m₃ : M)
(X : C)
[F.Monoidal]
{Z : C}
(h : (F.obj m₃).obj ((MonoidalCategoryStruct.tensorObj (F.obj m₁) (F.obj m₂)).obj X) ⟶ Z)
:
CategoryStruct.comp ((F.obj m₃).map ((Functor.OplaxMonoidal.δ F m₁ m₂).app X)) h = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (MonoidalCategoryStruct.tensorObj m₁ m₂) m₃).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ m₂ m₃).hom).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₁ (MonoidalCategoryStruct.tensorObj m₂ m₃)).app X)
(CategoryStruct.comp ((Functor.OplaxMonoidal.δ F m₂ m₃).app ((F.obj m₁).obj X)) h)))
@[simp]
theorem
CategoryTheory.obj_zero_map_μ_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m : M}
{X Y : C}
(f : X ⟶ (F.obj m).obj Y)
[F.Monoidal]
:
CategoryStruct.comp ((F.obj (𝟙_ M)).map f) ((Functor.LaxMonoidal.μ F m (𝟙_ M)).app Y) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X)
(CategoryStruct.comp f ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y))
@[simp]
theorem
CategoryTheory.obj_zero_map_μ_app_assoc
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
{m : M}
{X Y : C}
(f : X ⟶ (F.obj m).obj Y)
[F.Monoidal]
{Z : C}
(h : (F.obj (MonoidalCategoryStruct.tensorObj m (𝟙_ M))).obj Y ⟶ Z)
:
CategoryStruct.comp ((F.obj (𝟙_ M)).map f) (CategoryStruct.comp ((Functor.LaxMonoidal.μ F m (𝟙_ M)).app Y) h) = CategoryStruct.comp ((Functor.OplaxMonoidal.η F).app X)
(CategoryStruct.comp f (CategoryStruct.comp ((F.map (MonoidalCategoryStruct.rightUnitor m).inv).app Y) h))
@[simp]
theorem
CategoryTheory.obj_μ_zero_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m₁ m₂ : M)
(X : C)
[F.Monoidal]
:
CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X))
(CategoryStruct.comp ((Functor.LaxMonoidal.μ F m₁ (MonoidalCategoryStruct.tensorObj (𝟙_ M) m₂)).app X)
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.associator m₁ (𝟙_ M) m₂).inv).app X)
((Functor.OplaxMonoidal.δ F (MonoidalCategoryStruct.tensorObj m₁ (𝟙_ M)) m₂).app X))) = CategoryStruct.comp ((Functor.LaxMonoidal.μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X))
(CategoryStruct.comp ((F.map (MonoidalCategoryStruct.leftUnitor m₂).hom).app ((F.obj m₁).obj X))
((F.obj m₂).map ((F.map (MonoidalCategoryStruct.rightUnitor m₁).inv).app X)))
noncomputable def
CategoryTheory.unitOfTensorIsoUnit
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
[F.Monoidal]
:
If m ⊗ n ≅ 𝟙_M, then F.obj m is a left inverse of F.obj n.
Equations
@[simp]
theorem
CategoryTheory.unitOfTensorIsoUnit_inv_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
[F.Monoidal]
(X : C)
:
(unitOfTensorIsoUnit F m n h).inv.app X = CategoryStruct.comp ((Functor.LaxMonoidal.ε F).app X)
(CategoryStruct.comp ((F.map h.inv).app X) ((Functor.OplaxMonoidal.δ F m n).app X))
@[simp]
theorem
CategoryTheory.unitOfTensorIsoUnit_hom_app
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
[F.Monoidal]
(X : C)
:
(unitOfTensorIsoUnit F m n h).hom.app X = CategoryStruct.comp ((Functor.LaxMonoidal.μ F m n).app X)
(CategoryStruct.comp ((F.map h.hom).app X) ((Functor.OplaxMonoidal.η F).app X))
noncomputable def
CategoryTheory.equivOfTensorIsoUnit
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
(h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M)
(H :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom))
[F.Monoidal]
:
If m ⊗ n ≅ 𝟙_M and n ⊗ m ≅ 𝟙_M (subject to some commuting constraints),
then F.obj m and F.obj n forms a self-equivalence of C.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.equivOfTensorIsoUnit_unitIso
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
(h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M)
(H :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom))
[F.Monoidal]
:
@[simp]
theorem
CategoryTheory.equivOfTensorIsoUnit_functor
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
(h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M)
(H :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom))
[F.Monoidal]
:
@[simp]
theorem
CategoryTheory.equivOfTensorIsoUnit_counitIso
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
(h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M)
(H :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom))
[F.Monoidal]
:
@[simp]
theorem
CategoryTheory.equivOfTensorIsoUnit_inverse
{C : Type u}
[Category.{v, u} C]
{M : Type u_1}
[Category.{u_2, u_1} M]
[MonoidalCategory M]
(F : Functor M (Functor C C))
(m n : M)
(h₁ : MonoidalCategoryStruct.tensorObj m n ≅ 𝟙_ M)
(h₂ : MonoidalCategoryStruct.tensorObj n m ≅ 𝟙_ M)
(H :
CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight h₁.hom m) (MonoidalCategoryStruct.leftUnitor m).hom = CategoryStruct.comp (MonoidalCategoryStruct.associator m n m).hom
(CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft m h₂.hom) (MonoidalCategoryStruct.rightUnitor m).hom))
[F.Monoidal]
: