feat: the opposite of a braided category is braided (#10095)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Mar 22, 2024 · 28168eb · 28168eb
1 parent cdb43dd
commit 28168eb
Show file tree

Hide file tree

Showing 13 changed files with 32 additions and 11 deletions.
diff --git 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
@@ -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 → ...ategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean → ...ategoryTheory/Monoidal/Braided/Basic.lean
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
 
 /-!