If C is braided, so is Cᵒᵖ. #
Todo: we should also do Cᵐᵒᵖ.
instance
instBraidedCategoryOpposite
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.BraidedCategory.unop_tensor_μ
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_2} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : Cᵒᵖ)
(Y : Cᵒᵖ)
(W : Cᵒᵖ)
(Z : Cᵒᵖ)
:
(CategoryTheory.tensor_μ X W Y Z).unop = CategoryTheory.tensor_μ (Opposite.unop X) (Opposite.unop Y) (Opposite.unop W) (Opposite.unop Z)
@[simp]
theorem
CategoryTheory.BraidedCategory.op_tensor_μ
{C : Type u_2}
[CategoryTheory.Category.{u_3, u_2} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
(X : C)
(Y : C)
(W : C)
(Z : C)
:
(CategoryTheory.tensor_μ X W Y Z).op = CategoryTheory.tensor_μ (Opposite.op X) (Opposite.op Y) (Opposite.op W) (Opposite.op Z)