[Merged by Bors] - Feat: Add Yang-Baxter equation and the opposite braided monoidal category

Mathlib/CategoryTheory/Monoidal/Braided.lean

@@ -3,9 +3,11 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Monoidal.Discrete
+import Mathlib.CategoryTheory.Conj
 import Mathlib.CategoryTheory.Monoidal.Free.Coherence
+import Mathlib.CategoryTheory.Monoidal.Discrete
 import Mathlib.CategoryTheory.Monoidal.NaturalTransformation
+import Mathlib.CategoryTheory.Monoidal.Opposite
 import Mathlib.Tactic.CategoryTheory.Coherence
 
 #align_import category_theory.monoidal.braided from "leanprover-community/mathlib"@"2efd2423f8d25fa57cf7a179f5d8652ab4d0df44"
@@ -26,6 +28,10 @@
 * Construct the Drinfeld center of a monoidal category as a braided monoidal category.
 * Say something about pseudo-natural transformations.
 
+## References
+
+* [Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik, *Tensor categories*][egno15]
+
 -/
 
 
@@ -123,6 +129,38 @@
   rw [tensorHom_def' f g, tensorHom_def g f]
   simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]
 
+theorem yang_baxter (X Y Z : C) :
+    (α_ X Y Z).inv ≫ ((β_ X Y).hom ▷ Z) ≫ (α_ Y X Z).hom ≫ 
+    (Y ◁ (β_ X Z).hom) ≫ (α_ Y Z X).inv ≫
+    ((β_ Y Z).hom ▷ X) ≫ (α_ Z Y X).hom
+    = (X ◁ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫
+      ((β_ X Z).hom ▷ Y) ≫ (α_ Z X Y).hom ≫
+      (Z ◁ (β_ X Y).hom) := by
+  have := (braiding_naturality_right_assoc X (β_ Y Z).hom (α_ Z Y X).hom).symm
+  refine Eq.trans (Eq.symm ?_) (Eq.trans this ?_)
+  · refine Eq.trans (congrArg (. ≫ _) (braiding_tensor_right X Y Z)) ?_
+    simp only [assoc]
+  · refine congrArg (_ ≫ .) ((Iso.eq_comp_inv _).mp ?_)
+    refine Eq.trans (braiding_tensor_right X Z Y) ?_
+    simp only [assoc]
+
+theorem yang_baxter' (X Y Z : C) :
+    Iso.homCongr (α_ X Y Z) (α_ Z Y X)
+      (((β_ X Y).hom ▷ Z) ⊗≫ (Y ◁ (β_ X Z).hom) ⊗≫ ((β_ Y Z).hom ▷ X))
+    = ((X ◁ (β_ Y Z).hom) ⊗≫ ((β_ X Z).hom ▷ Y) ⊗≫ (Z ◁ (β_ X Y).hom)) := by
+  dsimp only [Mathlib.Tactic.Coherence.monoidalComp,
+              Mathlib.Tactic.Coherence.MonoidalCoherence.hom, Iso.homCongr_apply]
+  simp only [whiskerRight_tensor, id_whiskerRight, id_comp, Iso.inv_hom_id,
+             comp_id, assoc, tensor_id, id_comp, yang_baxter]
+
+theorem yang_baxter_iso (X Y Z : C) :
+    (α_ X Y Z).symm ≪≫ whiskerRightIso (β_ X Y) Z ≪≫ α_ Y X Z ≪≫ 
+    whiskerLeftIso Y (β_ X Z) ≪≫ (α_ Y Z X).symm ≪≫
+    whiskerRightIso (β_ Y Z) X ≪≫ (α_ Z Y X)
+    = whiskerLeftIso X (β_ Y Z) ≪≫ (α_ X Z Y).symm ≪≫
+      whiskerRightIso (β_ X Z) Y ≪≫ α_ Z X Y ≪≫
+      whiskerLeftIso Z (β_ X Y) := Iso.ext (yang_baxter X Y Z)
+
 end BraidedCategory
 
 /--
@@ -298,6 +336,10 @@
 
 attribute [reassoc (attr := simp)] SymmetricCategory.symmetry
 
+lemma SymmetricCategory.braiding_swap_eq_inv_braiding {C : Type u₁}
+    [Category.{v₁} C] [MonoidalCategory C] [SymmetricCategory C] (X Y : C) :
+    (β_ Y X).hom = (β_ X Y).inv := Iso.inv_ext' (symmetry X Y)
+
 variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory C] [BraidedCategory C]
 variable (D : Type u₂) [Category.{v₂} D] [MonoidalCategory D] [BraidedCategory D]
 variable (E : Type u₃) [Category.{v₃} E] [MonoidalCategory E] [BraidedCategory E]
@@ -618,4 +660,108 @@
 
 end Tensor
 
+namespace MonoidalOpposite
+
+instance instBraiding : BraidedCategory Cᴹᵒᵖ where
+  braiding X Y := (β_ (unmop Y) (unmop X)).mop
+  braiding_naturality_right X {_ _} f := braiding_naturality_left f.unmop (unmop X)
+  braiding_naturality_left {_ _} f Z := braiding_naturality_right (unmop Z) f.unmop
+  hexagon_forward X Y Z := hexagon_reverse (unmop Z) (unmop Y) (unmop X)
+  hexagon_reverse X Y Z := hexagon_forward (unmop Z) (unmop Y) (unmop X)
+
+/-- The identity functor on `C`, viewed as a functor from `C` to its
+monoidal opposite, upgraded to a braided functor. -/
+@[simps!] def mopBraidedFunctor : BraidedFunctor C Cᴹᵒᵖ where
+  μ X Y := (β_ (mop X) (mop Y)).hom
+  ε := 𝟙 (𝟙_ Cᴹᵒᵖ)
+  associativity X Y Z := by
+    simp only [tensorHom_id, id_tensorHom]
+    change (β_ (mop X) (mop Y)).hom ▷ (mop Z) ≫ (β_ (mop Y ⊗ mop X) (mop Z)).hom ≫
+              (α_ (mop Z) (mop Y) (mop X)).inv
+            = (α_ (mop X) (mop Y) (mop Z)).hom ≫ (mop X) ◁ (β_ (mop Y) (mop Z)).hom ≫
+                (β_ (mop X) (mop Z ⊗ mop Y)).hom
+    refine (α_ (mop X) (mop Y) (mop Z)).inv_comp_eq.mp ?_
+    simp only [← assoc]
+    refine (α_ (mop Z) (mop Y) (mop X)).comp_inv_eq.mpr ?_
+    simp only [braiding_tensor_left, braiding_tensor_right,
+               assoc, Iso.inv_hom_id, comp_id]
+    exact yang_baxter (mop X) (mop Y) (mop Z)
+  left_unitality X :=
+    Eq.symm $ Eq.trans (congrArg (. ≫ _) (tensor_id _ _))
+    $ Eq.trans (id_comp _) (braiding_rightUnitor Cᴹᵒᵖ (mop X))
+  right_unitality X :=
+    Eq.symm $ Eq.trans (congrArg (. ≫ _) (tensor_id _ _))
+    $ Eq.trans (id_comp _) (braiding_leftUnitor Cᴹᵒᵖ (mop X))
+  __ := mopFunctor C
+
+/-- The identity functor on `C`, viewed as a functor from the
+monoidal opposite of `C` to `C`, upgraded to a braided functor. -/
+@[simps!] def unmopBraidedFunctor : BraidedFunctor Cᴹᵒᵖ C where
+  μ X Y := (β_ (unmop X) (unmop Y)).hom
+  ε := 𝟙 (𝟙_ C)
+  associativity X Y Z := by
+    simp only [tensorHom_id, id_tensorHom]
+    change (β_ (unmop X) (unmop Y)).hom ▷ (unmop Z) ≫ (β_ (unmop Y ⊗ unmop X) (unmop Z)).hom
+              ≫ (α_ (unmop Z) (unmop Y) (unmop X)).inv
+            = (α_ (unmop X) (unmop Y) (unmop Z)).hom ≫ (unmop X) ◁ (β_ (unmop Y) (unmop Z)).hom
+              ≫ (β_ (unmop X) (unmop Z ⊗ unmop Y)).hom
+    refine (α_ (unmop X) (unmop Y) (unmop Z)).inv_comp_eq.mp ?_
+    simp only [← assoc]
+    refine (α_ (unmop Z) (unmop Y) (unmop X)).comp_inv_eq.mpr ?_
+    simp only [braiding_tensor_left, braiding_tensor_right,
+               assoc, Iso.inv_hom_id, comp_id]
+    exact yang_baxter (unmop X) (unmop Y) (unmop Z)
+  left_unitality X :=
+    Eq.symm $ Eq.trans (congrArg (. ≫ _) (tensor_id _ _))
+    $ Eq.trans (id_comp _) (braiding_rightUnitor C (unmop X))
+  right_unitality X :=
+    Eq.symm $ Eq.trans (congrArg (. ≫ _) (tensor_id _ _))
+    $ Eq.trans (id_comp _) (braiding_leftUnitor C (unmop X))
+  __ := unmopFunctor C
+
+end MonoidalOpposite
+
+/-- The braided monoidal category obtained from `C` by replacing its braiding
+`β_ X Y : X ⊗ Y ≅ Y ⊗ X` with the inverse `(β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X`.
+This corresponds to the automorphism of the braid group swapping
+over-crossings and under-crossings. -/
+@[reducible] def reverseBraiding : BraidedCategory C where
+  braiding X Y := (β_ Y X).symm
+  braiding_naturality_right := by
+    simp_rw [Iso.symm_hom, Iso.comp_inv_eq, assoc, Iso.eq_inv_comp,
+             braiding_naturality_left, implies_true]
+  braiding_naturality_left  := by
+    simp_rw [Iso.symm_hom, Iso.comp_inv_eq, assoc, Iso.eq_inv_comp,
+             braiding_naturality_right, implies_true]
+  hexagon_forward := by
+    intros X Y Z
+    simp only [← Iso.symm_inv, ← Iso.trans_inv,
+               ← whiskerLeftIso_inv, ← whiskerRightIso_inv]
+    refine (Iso.inv_eq_inv _ _).mpr ?_
+    simp only [Iso.trans_hom, Iso.symm_symm_eq, Iso.symm_hom, assoc]
+    exact hexagon_reverse Y Z X
+  hexagon_reverse := by
+    intros X Y Z
+    simp only [← Iso.symm_inv, ← Iso.trans_inv,
+               ← whiskerLeftIso_inv, ← whiskerRightIso_inv]
+    refine (Iso.inv_eq_inv _ _).mpr ?_
+    simp only [Iso.trans_hom, Iso.symm_symm_eq, Iso.symm_hom, assoc]
+    exact hexagon_forward Z X Y
+
+lemma SymmetricCategory.reverseBraiding_eq (C : Type u₁) [Category.{v₁} C]
+    [MonoidalCategory C] [i : SymmetricCategory C] :
+    reverseBraiding C = i.toBraidedCategory := by
+  dsimp only [reverseBraiding]
+  congr
+  funext X Y
+  exact Iso.ext (braiding_swap_eq_inv_braiding Y X).symm
+
+/-- The identity functor from `C` to `C`, where the codomain is given the
+reversed braiding, upgraded to a braided functor. -/
+def SymmetricCategory.equivReverseBraiding (C : Type u₁) [Category.{v₁} C]
+    [MonoidalCategory C] [SymmetricCategory C] :=
+  @BraidedFunctor.mk C _ _ _ C _ _ (reverseBraiding C) (.id C) $ fun X Y =>
+    (IsIso.eq_inv_comp _).mpr $ Eq.trans (id_comp _)
+    $ Eq.trans (braiding_swap_eq_inv_braiding Y X) (comp_id _).symm
+
 end CategoryTheory

Mathlib/CategoryTheory/Monoidal/Category.lean

@@ -348,6 +348,20 @@ theorem inv_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
     inv (X ◁ f) = X ◁ inv f := by
   aesop_cat
 
+@[simp]
+lemma whiskerLeftIso_refl (W X : C) :
+    whiskerLeftIso W (Iso.refl X) = Iso.refl (W ⊗ X) :=
+  Iso.ext (whiskerLeft_id W X)
+
+@[simp]
+lemma whiskerLeftIso_trans (W : C) {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) :
+    whiskerLeftIso W (f ≪≫ g) = whiskerLeftIso W f ≪≫ whiskerLeftIso W g :=
+  Iso.ext (whiskerLeft_comp W f.hom g.hom)
+
+@[simp]
+lemma whiskerLeftIso_symm (W : C) {X Y : C} (f : X ≅ Y) :
+    whiskerLeftIso W f.symm = (whiskerLeftIso W f).symm := rfl
+
 /-- The right whiskering of an isomorphism is an isomorphism. -/
 @[simps!]
 def whiskerRightIso {X Y : C} (f : X ≅ Y) (Z : C) : X ⊗ Z ≅ Y ⊗ Z where
@@ -362,6 +376,20 @@ theorem inv_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
     inv (f ▷ Z) = inv f ▷ Z := by
   aesop_cat
 
+@[simp]
+lemma whiskerRightIso_refl (X W : C) :
+    whiskerRightIso (Iso.refl X) W = Iso.refl (X ⊗ W) :=
+  Iso.ext (id_whiskerRight X W)
+
+@[simp]
+lemma whiskerRightIso_trans {X Y Z : C} (f : X ≅ Y) (g : Y ≅ Z) (W : C) :
+    whiskerRightIso (f ≪≫ g) W = whiskerRightIso f W ≪≫ whiskerRightIso g W :=
+  Iso.ext (comp_whiskerRight f.hom g.hom W)
+
+@[simp]
+lemma whiskerRightIso_symm {X Y : C} (f : X ≅ Y) (W : C) :
+    whiskerRightIso f.symm W = (whiskerRightIso f W).symm := rfl
+
 end MonoidalCategory
 
 /-- The tensor product of two isomorphisms is an isomorphism. -/

Mathlib/CategoryTheory/Monoidal/Opposite.lean

@@ -166,6 +166,13 @@ def mop (f : X ≅ Y) : mop X ≅ mop Y where
 
 end Iso
 
+namespace IsIso
+
+instance {X Y : C}    (f : X ⟶ Y) [i : IsIso f] : IsIso f.mop := i
+instance {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) [i : IsIso f] : IsIso f.unmop := i
+
+end IsIso
+
 variable [MonoidalCategory.{v₁} C]
 
 open Opposite MonoidalCategory
@@ -222,4 +229,63 @@ theorem mop_tensorUnit : 𝟙_ Cᴹᵒᵖ = mop (𝟙_ C) :=
   rfl
 #align category_theory.mop_tensor_unit CategoryTheory.mop_tensorUnit
 
+variable (C)
+
+/-- The identity functor on `C`, viewed as a functor from `C` to its monoidal opposite. -/
+@[simps!] def mopFunctor : C ⥤ Cᴹᵒᵖ := Functor.mk ⟨mop, mop⟩
+/-- The identity functor on `C`, viewed as a functor from the monoidal opposite of `C` to `C`. -/
+@[simps!] def unmopFunctor : Cᴹᵒᵖ ⥤ C := Functor.mk ⟨unmop, unmop⟩
+
+/-- The (identity) equivalence between `C` and its monoidal opposite. -/
+@[simps!] def MonoidalOpposite.underlyingEquiv : C ≌ Cᴹᵒᵖ := Equivalence.refl
+
+-- todo: upgrade to monoidal equivalence
+/-- The equivalence between `C` and its monoidal opposite's monoidal opposite. -/
+@[simps!] def MonoidalOpposite.double_dual_equiv : Cᴹᵒᵖᴹᵒᵖ ≌ C := Equivalence.refl
+
+/-- The identification `mop X ⊗ mop Y = mop (Y ⊗ X)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensor_iso :
+    tensor Cᴹᵒᵖ ≅ (unmopFunctor C).prod (unmopFunctor C)
+                  ⋙ Prod.swap C C ⋙ tensor C ⋙ mopFunctor C :=
+  Iso.refl _
+
+variable {C}
+
+/-- The identification `X ⊗ - = mop (- ⊗ unmop X)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorLeft_iso (X : Cᴹᵒᵖ) :
+    tensorLeft X ≅ unmopFunctor C ⋙ tensorRight (unmop X) ⋙ mopFunctor C :=
+  Iso.refl _
+
+/-- The identification `mop X ⊗ - = mop (- ⊗ X)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorLeft_mop_iso (X : C) :
+    tensorLeft (mop X) ≅ unmopFunctor C ⋙ tensorRight X ⋙ mopFunctor C :=
+  Iso.refl _
+
+/-- The identification `unmop X ⊗ - = unmop (mop - ⊗ X)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorLeft_unmop_iso (X : Cᴹᵒᵖ) :
+    tensorLeft (unmop X) ≅ mopFunctor C ⋙ tensorRight X ⋙ unmopFunctor C :=
+  Iso.refl _
+
+/-- The identification `- ⊗ X = mop (unmop X ⊗ -)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorRight_iso (X : Cᴹᵒᵖ) :
+    tensorRight X ≅ unmopFunctor C ⋙ tensorLeft (unmop X) ⋙ mopFunctor C :=
+  Iso.refl _
+
+/-- The identification `- ⊗ mop X = mop (- ⊗ unmop X)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorRight_mop_iso (X : C) :
+    tensorRight (mop X) ≅ unmopFunctor C ⋙ tensorLeft X ⋙ mopFunctor C :=
+  Iso.refl _
+
+/-- The identification `- ⊗ unmop X = unmop (X ⊗ mop -)` as a natural isomorphism. -/
+@[simps!]
+def MonoidalOpposite.tensorRight_unmop_iso (X : Cᴹᵒᵖ) :
+    tensorRight (unmop X) ≅ mopFunctor C ⋙ tensorLeft X ⋙ unmopFunctor C :=
+  Iso.refl _
+
 end CategoryTheory

docs/references.bib

@@ -911,6 +911,16 @@ @Article{         dyckhoff_1992
   doi           = {10.2307/2275431}
 }
 
+@Book{            egno15,
+  author        = {Etingof, Pavel and Gelaki, Shlomo and Nikshych, Dmitri and
+                  Ostrik, Victor},
+  title         = {Tensor Categories},
+  publisher     = {American Mathematical Society (AMS), Providence, RI},
+  year          = 2015,
+  pages         = {xvi+343},
+  isbn          = {978-1-4704-3441-0}
+}
+
 @Book{            EinsiedlerWard2017,
   author        = {Einsiedler, Manfred and Ward, Thomas},
   title         = {Functional Analysis, Spectral Theory, and Applications},