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 Y W Z : Cᵒᵖ)
:
(CategoryTheory.MonoidalCategory.tensorμ X W Y Z).unop = CategoryTheory.MonoidalCategory.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 Y W Z : C)
:
(CategoryTheory.MonoidalCategory.tensorμ X W Y Z).op = CategoryTheory.MonoidalCategory.tensorμ (Opposite.op X) (Opposite.op Y) (Opposite.op W) (Opposite.op Z)