From 28168eb625c8309440e8e8b007d3dad4a4cd686e Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott@tqft.net>
Date: Wed, 6 Mar 2024 11:37:19 +0000
Subject: [PATCH] feat: the opposite of a braided category is braided (#10095)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
---
 Mathlib.lean                                  |  3 ++-
 .../ModuleCat/Monoidal/Symmetric.lean         |  2 +-
 .../{Braided.lean => Braided/Basic.lean}      |  0
 .../Monoidal/Braided/Opposite.lean            | 20 +++++++++++++++++++
 Mathlib/CategoryTheory/Monoidal/Center.lean   |  2 +-
 Mathlib/CategoryTheory/Monoidal/CommMon_.lean |  2 +-
 .../Monoidal/FunctorCategory.lean             |  2 +-
 Mathlib/CategoryTheory/Monoidal/Mon_.lean     |  2 +-
 .../OfChosenFiniteProducts/Symmetric.lean     |  2 +-
 .../Monoidal/OfHasFiniteProducts.lean         |  2 +-
 Mathlib/CategoryTheory/Monoidal/Skeleton.lean |  2 +-
 .../CategoryTheory/Monoidal/Subcategory.lean  |  2 +-
 .../RepresentationTheory/Action/Monoidal.lean |  2 +-
 13 files changed, 32 insertions(+), 11 deletions(-)
 rename Mathlib/CategoryTheory/Monoidal/{Braided.lean => Braided/Basic.lean} (100%)
 create mode 100644 Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index c4698cc9b4691..6ba9967c4af39 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1263,7 +1263,8 @@ import Mathlib.CategoryTheory.Monad.Monadicity
 import Mathlib.CategoryTheory.Monad.Products
 import Mathlib.CategoryTheory.Monad.Types
 import Mathlib.CategoryTheory.Monoidal.Bimod
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+import Mathlib.CategoryTheory.Monoidal.Braided.Opposite
 import Mathlib.CategoryTheory.Monoidal.Category
 import Mathlib.CategoryTheory.Monoidal.Center
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
index 8a7b8fe804a2b..a8569e1313bd7 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 
 #align_import algebra.category.Module.monoidal.symmetric from "leanprover-community/mathlib"@"74403a3b2551b0970855e14ef5e8fd0d6af1bfc2"
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
similarity index 100%
rename from Mathlib/CategoryTheory/Monoidal/Braided.lean
rename to Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean
new file mode 100644
index 0000000000000..d5406819a894b
--- /dev/null
+++ b/Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean
@@ -0,0 +1,20 @@
+/-
+Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
+import Mathlib.CategoryTheory.Monoidal.Opposite
+
+/-!
+# If `C` is braided, so is `Cᵒᵖ`.
+
+Todo: we should also do `Cᵐᵒᵖ`.
+-/
+
+open CategoryTheory MonoidalCategory BraidedCategory Opposite
+
+variable {C : Type*} [Category C] [MonoidalCategory C] [BraidedCategory C]
+
+instance : BraidedCategory Cᵒᵖ where
+  braiding X Y := (β_ (unop Y) (unop X)).op
diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean
index fe7451784d68b..88d5255c905d3 100644
--- a/Mathlib/CategoryTheory/Monoidal/Center.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Center.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Functor.ReflectsIso
 
 #align_import category_theory.monoidal.center from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7"
diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
index e1c5841a17ba2..68b25fe3af423 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Mon_
 
 #align_import category_theory.monoidal.CommMon_ from "leanprover-community/mathlib"@"a836c6dba9bd1ee2a0cdc9af0006a596f243031c"
diff --git a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
index c005ad6d3be94..2a4b44a488afb 100644
--- a/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Monoidal/FunctorCategory.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Functor.Category
 import Mathlib.CategoryTheory.Functor.Const
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
index 3cd885689d61e..334725702caa8 100644
--- a/Mathlib/CategoryTheory/Monoidal/Mon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Discrete
 import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
diff --git a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
index 17d61d3a2ad54..018836210d178 100644
--- a/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
+++ b/Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Simon Hudon
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic
 
 #align_import category_theory.monoidal.of_chosen_finite_products.symmetric from "leanprover-community/mathlib"@"95a87616d63b3cb49d3fe678d416fbe9c4217bf4"
diff --git a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
index b5649e03597dd..9c8a704d23cf8 100644
--- a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
+++ b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Simon Hudon
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Skeleton.lean b/Mathlib/CategoryTheory/Monoidal/Skeleton.lean
index 35cdf9bea613d..d6c7bd897a84a 100644
--- a/Mathlib/CategoryTheory/Monoidal/Skeleton.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Skeleton.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.CategoryTheory.Skeletal
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
index cfbc46db52951..23e836695f5c8 100644
--- a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Antoine Labelle. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Labelle
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Linear
 import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
diff --git a/Mathlib/RepresentationTheory/Action/Monoidal.lean b/Mathlib/RepresentationTheory/Action/Monoidal.lean
index eed97bdef0004..684d4ae5f730b 100644
--- a/Mathlib/RepresentationTheory/Action/Monoidal.lean
+++ b/Mathlib/RepresentationTheory/Action/Monoidal.lean
@@ -10,7 +10,7 @@ import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
 import Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Linear
-import Mathlib.CategoryTheory.Monoidal.Braided
+import Mathlib.CategoryTheory.Monoidal.Braided.Basic
 import Mathlib.CategoryTheory.Monoidal.Types.Basic
 
 /-!