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
Instances For
@[simp]
@[simp]
theorem
CategoryTheory.endofunctorMonoidalCategory_tensorUnit_map
(C : Type u)
[Category.{v, u} 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)
:
@[simp]
@[simp]
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.μ_δ_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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
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]
:
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)
:
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]
:
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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
@[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]
:
@[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)
:
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]
:
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)
:
@[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]
:
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)
:
@[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]
:
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)
:
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]
:
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)
:
@[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]
:
@[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]
:
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]
:
@[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)
:
@[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
Instances For
@[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)
:
@[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)
:
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.
Instances For
@[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]
: