If C is braided, so is Cᵒᵖ. #
Todo: we should also do Cᵐᵒᵖ.
@[instance_reducible]
instance
instBraidedCategoryOpposite
{C : Type u_1}
[CategoryTheory.Category.{v_1, 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}
[Category.{v_2, u_2} C]
[MonoidalCategory C]
[BraidedCategory C]
(X Y W Z : Cᵒᵖ)
:
(MonoidalCategory.tensorμ X W Y Z).unop = MonoidalCategory.tensorμ (Opposite.unop X) (Opposite.unop Y) (Opposite.unop W) (Opposite.unop Z)
@[simp]
theorem
CategoryTheory.BraidedCategory.op_tensorμ
{C : Type u_2}
[Category.{v_2, u_2} C]
[MonoidalCategory C]
[BraidedCategory C]
(X Y W Z : C)
:
(MonoidalCategory.tensorμ X W Y Z).op = MonoidalCategory.tensorμ (Opposite.op X) (Opposite.op Y) (Opposite.op W) (Opposite.op Z)