[Merged by Bors] - feat(category_theory/monoidal): Drinfeld center

src/category_theory/monoidal/category.lean

@@ -192,6 +192,7 @@ by { rw [←tensor_comp], simp }
   (g ⊗ (𝟙 W)) ≫ ((𝟙 Z) ⊗ f) = g ⊗ f :=
 by { rw [←tensor_comp], simp }
 
+@[reassoc]
 lemma left_unitor_inv_naturality {X X' : C} (f : X ⟶ X') :
   f ≫ (λ_ X').inv = (λ_ X).inv ≫ (𝟙 _ ⊗ f) :=
 begin
@@ -200,6 +201,7 @@ begin
   rw [left_unitor_naturality, ←category.assoc, iso.inv_hom_id, category.id_comp]
 end
 
+@[reassoc]
 lemma right_unitor_inv_naturality {X X' : C} (f : X ⟶ X') :
   f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ (f ⊗ 𝟙 _) :=
 begin
@@ -229,6 +231,7 @@ by { rw [←cancel_mono (λ_ Y).hom, left_unitor_naturality, left_unitor_natural
 by { rw [←cancel_mono (ρ_ Y).hom, right_unitor_naturality, right_unitor_naturality], simp }
 
 -- See Proposition 2.2.4 of <http://www-math.mit.edu/~etingof/egnobookfinal.pdf>
+@[reassoc]
 lemma left_unitor_tensor' (X Y : C) :
   ((α_ (𝟙_ C) X Y).hom) ≫ ((λ_ (X ⊗ Y)).hom) = ((λ_ X).hom ⊗ (𝟙 Y)) :=
 by
@@ -258,15 +261,27 @@ by
       associator_naturality, ←triangle_assoc, ←triangle, id_tensor_comp, pentagon_assoc,
       ←associator_naturality, tensor_id]
 
-@[simp]
+@[reassoc, simp]
 lemma right_unitor_tensor_inv (X Y : C) :
   ((ρ_ (X ⊗ Y)).inv) = ((𝟙 X) ⊗ (ρ_ Y).inv) ≫ ((α_ X Y (𝟙_ C)).inv) :=
 eq_of_inv_eq_inv (by simp)
 
+@[reassoc]
 lemma associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
   (f ⊗ (g ⊗ h)) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ g) ⊗ h) :=
 by { rw [comp_inv_eq, assoc, associator_naturality], simp }
 
+@[reassoc]
+lemma id_tensor_associator_naturality {X Y Z Z' : C} (h : Z ⟶ Z') :
+  (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ (𝟙 Y ⊗ h)) :=
+by { rw [←tensor_id, associator_naturality], }
+
+@[reassoc]
+lemma id_tensor_associator_inv_naturality {X Y Z X' : C} (f : X ⟶ X')  :
+  (f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z) :=
+by { rw [←tensor_id, associator_inv_naturality] }
+
+@[reassoc]
 lemma pentagon_inv (W X Y Z : C) :
   ((𝟙 W) ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv ≫ ((α_ W X Y).inv ⊗ (𝟙 Z))
     = (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv :=
@@ -300,6 +315,26 @@ lemma unitors_equal : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
 by rw [←tensor_left_iff, ←cancel_epi (α_ (𝟙_ C) (𝟙_ _) (𝟙_ _)).hom, ←cancel_mono (ρ_ (𝟙_ C)).hom,
        triangle, ←right_unitor_tensor, right_unitor_naturality]
 
+@[simp, reassoc]
+lemma hom_inv_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
+  (f.hom ⊗ g) ≫ (f.inv ⊗ h) = 𝟙 V ⊗ (g ≫ h) :=
+by rw [←tensor_comp, f.hom_inv_id]
+
+@[simp, reassoc]
+lemma inv_hom_id_tensor {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
+  (f.inv ⊗ g) ≫ (f.hom ⊗ h) = 𝟙 W ⊗ (g ≫ h) :=
+by rw [←tensor_comp, f.inv_hom_id]
+
+@[simp, reassoc]
+lemma tensor_hom_inv_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
+  (g ⊗ f.hom) ≫ (h ⊗ f.inv) = (g ≫ h) ⊗ 𝟙 V :=
+by rw [←tensor_comp, f.hom_inv_id]
+
+@[simp, reassoc]
+lemma tensor_inv_hom_id {V W X Y Z : C} (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) :
+  (g ⊗ f.inv) ≫ (h ⊗ f.hom) = (g ≫ h) ⊗ 𝟙 W :=
+by rw [←tensor_comp, f.inv_hom_id]
+
 end
 
 section

src/category_theory/monoidal/center.lean

@@ -0,0 +1,274 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.monoidal.braided
+import category_theory.reflects_isomorphisms
+
+/-!
+# Half braidings and the Drinfeld center of a monoidal category
+
+We define `center C` to be pairs `⟨X, b⟩`, where `X : C` and `b` is a half-braiding on `X`.
+
+We show that `center C` is braided monoidal,
+and provide the monoidal functor `center.forget` from `center C` back to `C`.
+
+## Future work
+
+Verifying the various axioms here is done by tedious rewriting.
+Using the `slice` tactic may make the proofs marginally more readable.
+
+More exciting, however, would be to make possible one of the following options:
+1. Integration with homotopy.io / globular to give "picture proofs".
+2. The monoidal coherence theorem, so we can ignore associators
+   (after which most of these proofs are trivial;
+   I'm unsure if the monoidal coherence theorem is even usable in dependent type theory).
+3. Automating these proofs using `rewrite_search` or some relative.
+
+-/
+
+open category_theory
+open category_theory.monoidal_category
+
+universes v v₁ v₂ v₃ u u₁ u₂ u₃
+noncomputable theory
+
+namespace category_theory
+
+variables {C : Type u₁} [category.{v₁} C] [monoidal_category C]
+
+/--
+A half-braiding on `X : C` is a family of isomorphisms `X ⊗ U ≅ U ⊗ X`,
+monoidally natural in `U : C`.
+
+Thinking of `C` as a 2-category with a single `0`-morphism, these are the same as natural
+transformations (in the pseudo- sense) of the identity 2-functor on `C`, which send the unique
+`0`-morphism to `X`.
+-/
+@[nolint has_inhabited_instance]
+structure half_braiding (X : C) :=
+(β : Π U, X ⊗ U ≅ U ⊗ X)
+(monoidal' : ∀ U U', (β (U ⊗ U')).hom =
+  (α_ _ _ _).inv ≫ ((β U).hom ⊗ 𝟙 U') ≫ (α_ _ _ _).hom ≫ (𝟙 U ⊗ (β U').hom) ≫ (α_ _ _ _).inv
+  . obviously)
+(naturality' : ∀ {U U'} (f : U ⟶ U'), (𝟙 X ⊗ f) ≫ (β U').hom = (β U).hom ≫ (f ⊗ 𝟙 X) . obviously)
+
+restate_axiom half_braiding.monoidal'
+attribute [reassoc, simp] half_braiding.monoidal -- the reassoc lemma is redundant as a simp lemma
+restate_axiom half_braiding.naturality'
+attribute [simp, reassoc] half_braiding.naturality
+
+variables (C)
+/--
+The Drinfeld center of a monoidal category `C` has as objects pairs `⟨X, b⟩`, where `X : C`
+and `b` is a half-braiding on `X`.
+-/
+@[nolint has_inhabited_instance]
+def center := Σ X : C, half_braiding X
+
+namespace center
+
+variables {C}
+
+/-- A morphism in the Drinfeld center of `C`. -/
+@[ext, nolint has_inhabited_instance]
+structure hom (X Y : center C) :=
+(f : X.1 ⟶ Y.1)
+(comm' : ∀ U, (f ⊗ 𝟙 U) ≫ (Y.2.β U).hom = (X.2.β U).hom ≫ (𝟙 U ⊗ f) . obviously)
+
+restate_axiom hom.comm'
+attribute [simp, reassoc] hom.comm
+
+instance : category (center C) :=
+{ hom := hom,
+  id := λ X, { f := 𝟙 X.1, },
+  comp := λ X Y Z f g, { f := f.f ≫ g.f, }, }
+
+@[simp] lemma id_f (X : center C) : hom.f (𝟙 X) = 𝟙 X.1 := rfl
+@[simp] lemma comp_f {X Y Z : center C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).f = f.f ≫ g.f := rfl
+
+/--
+Construct an isomorphism in the Drinfeld center from
+a morphism whose underlying morphism is an isomorphism.
+-/
+@[simps]
+def iso_mk {X Y : center C} (f : X ⟶ Y) [is_iso f.f] : X ≅ Y :=
+{ hom := f,
+  inv := ⟨inv f.f, λ U, by simp [←cancel_epi (f.f ⊗ 𝟙 U), ←comp_tensor_id_assoc, ←id_tensor_comp]⟩ }
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+@[simps]
+def tensor_obj (X Y : center C) : center C :=
+⟨X.1 ⊗ Y.1,
+  { β := λ U, α_ _ _ _ ≪≫ (iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm
+      ≪≫ (X.2.β U ⊗ iso.refl Y.1) ≪≫ α_ _ _ _,
+    monoidal' := λ U U',
+    begin
+      dsimp,
+      simp only [comp_tensor_id, id_tensor_comp, category.assoc, half_braiding.monoidal],
+      rw [pentagon_assoc, pentagon_inv_assoc, iso.eq_inv_comp, ←pentagon_assoc,
+        ←id_tensor_comp_assoc, iso.hom_inv_id, tensor_id, category.id_comp,
+        ←associator_naturality_assoc, cancel_epi, cancel_epi,
+        ←associator_inv_naturality_assoc (X.2.β U).hom,
+        associator_inv_naturality_assoc _ _ (Y.2.β U').hom, tensor_id, tensor_id,
+        id_tensor_comp_tensor_id_assoc, associator_naturality_assoc (X.2.β U).hom,
+        ←associator_naturality_assoc _ _ (Y.2.β U').hom, tensor_id, tensor_id,
+        tensor_id_comp_id_tensor_assoc, ←id_tensor_comp_tensor_id, tensor_id, category.comp_id,
+        ←is_iso.inv_comp_eq, inv_tensor, is_iso.inv_id, is_iso.iso.inv_inv, pentagon_assoc,
+        iso.hom_inv_id_assoc, cancel_epi, cancel_epi, ←is_iso.inv_comp_eq, is_iso.iso.inv_hom,
+        ←pentagon_inv_assoc, ←comp_tensor_id_assoc, iso.inv_hom_id, tensor_id, category.id_comp,
+        ←associator_inv_naturality_assoc, cancel_epi, cancel_epi, ←is_iso.inv_comp_eq, inv_tensor,
+        is_iso.iso.inv_hom, is_iso.inv_id, pentagon_inv_assoc, iso.inv_hom_id, category.comp_id],
+    end,
+    naturality' := λ U U' f,
+    begin
+      dsimp,
+      rw [category.assoc, category.assoc, category.assoc, category.assoc,
+        id_tensor_associator_naturality_assoc, ←id_tensor_comp_assoc, half_braiding.naturality,
+        id_tensor_comp_assoc, associator_inv_naturality_assoc, ←comp_tensor_id_assoc,
+        half_braiding.naturality, comp_tensor_id_assoc, associator_naturality, ←tensor_id],
+    end, }⟩
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+@[simps]
+def tensor_hom {X₁ Y₁ X₂ Y₂ : center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
+  tensor_obj X₁ X₂ ⟶ tensor_obj Y₁ Y₂ :=
+{ f := f.f ⊗ g.f,
+  comm' := λ U, begin
+    dsimp,
+    rw [category.assoc, category.assoc, category.assoc, category.assoc,
+      associator_naturality_assoc, ←tensor_id_comp_id_tensor, category.assoc,
+      ←id_tensor_comp_assoc, g.comm, id_tensor_comp_assoc, tensor_id_comp_id_tensor_assoc,
+      ←id_tensor_comp_tensor_id, category.assoc, associator_inv_naturality_assoc,
+      id_tensor_associator_inv_naturality_assoc, tensor_id,
+      id_tensor_comp_tensor_id_assoc, ←tensor_id_comp_id_tensor g.f, category.assoc,
+      ←comp_tensor_id_assoc, f.comm, comp_tensor_id_assoc, id_tensor_associator_naturality,
+      associator_naturality_assoc, ←id_tensor_comp, tensor_id_comp_id_tensor],
+  end  }
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+@[simps]
+def tensor_unit : center C :=
+⟨𝟙_ C,
+  { β := λ U, (λ_ U) ≪≫ (ρ_ U).symm,
+    monoidal' := λ U U', by simp,
+    naturality' := λ U U' f, begin
+      dsimp,
+      rw [left_unitor_naturality_assoc, right_unitor_inv_naturality, category.assoc],
+    end, }⟩
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+def associator (X Y Z : center C) : tensor_obj (tensor_obj X Y) Z ≅ tensor_obj X (tensor_obj Y Z) :=
+iso_mk ⟨(α_ X.1 Y.1 Z.1).hom, λ U, begin
+  dsimp,
+  simp only [category.assoc, comp_tensor_id, id_tensor_comp],
+  rw [pentagon, pentagon_assoc, ←associator_naturality_assoc (𝟙 X.1) (𝟙 Y.1), tensor_id, cancel_epi,
+    cancel_epi, iso.eq_inv_comp, ←pentagon_assoc, ←id_tensor_comp_assoc, iso.hom_inv_id, tensor_id,
+    category.id_comp, ←associator_naturality_assoc, cancel_epi, cancel_epi, ←is_iso.inv_comp_eq,
+    inv_tensor, is_iso.inv_id, is_iso.iso.inv_inv, pentagon_assoc, iso.hom_inv_id_assoc, ←tensor_id,
+    ←associator_naturality_assoc],
+end⟩
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+def left_unitor (X : center C) : tensor_obj tensor_unit X ≅ X :=
+iso_mk ⟨(λ_ X.1).hom, λ U, begin
+  dsimp,
+  simp only [category.comp_id, category.assoc, tensor_inv_hom_id, comp_tensor_id,
+    tensor_id_comp_id_tensor, triangle_assoc_comp_right_inv],
+  rw [←left_unitor_tensor, left_unitor_naturality, left_unitor_tensor'_assoc],
+end⟩
+
+/-- Auxiliary definition for the `monoidal_category` instance on `center C`. -/
+def right_unitor (X : center C) : tensor_obj X tensor_unit ≅ X :=
+iso_mk ⟨(ρ_ X.1).hom, λ U, begin
+  dsimp,
+  simp only [tensor_id_comp_id_tensor_assoc, triangle_assoc, id_tensor_comp, category.assoc],
+  rw [←tensor_id_comp_id_tensor_assoc (ρ_ U).inv, cancel_epi, ←right_unitor_tensor_inv_assoc,
+    ←right_unitor_inv_naturality_assoc],
+  simp,
+end⟩
+
+section
+local attribute [simp] associator_naturality left_unitor_naturality right_unitor_naturality
+  pentagon
+local attribute [simp] center.associator center.left_unitor center.right_unitor
+
+instance : monoidal_category (center C) :=
+{ tensor_obj := λ X Y, tensor_obj X Y,
+  tensor_hom := λ X₁ Y₁ X₂ Y₂ f g, tensor_hom f g,
+  tensor_unit := tensor_unit,
+  associator := associator,
+  left_unitor := left_unitor,
+  right_unitor := right_unitor, }
+
+@[simp] lemma tensor_fst (X Y : center C) : (X ⊗ Y).1 = X.1 ⊗ Y.1 := rfl
+
+@[simp] lemma tensor_β (X Y : center C) (U : C) :
+  (X ⊗ Y).2.β U =
+    α_ _ _ _ ≪≫ (iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm
+      ≪≫ (X.2.β U ⊗ iso.refl Y.1) ≪≫ α_ _ _ _ :=
+rfl
+@[simp] lemma tensor_f {X₁ Y₁ X₂ Y₂ : center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
+  (f ⊗ g).f = f.f ⊗ g.f :=
+rfl
+
+@[simp] lemma associator_hom_f (X Y Z : center C) : hom.f (α_ X Y Z).hom = (α_ X.1 Y.1 Z.1).hom :=
+rfl
+
+@[simp] lemma associator_inv_f (X Y Z : center C) : hom.f (α_ X Y Z).inv = (α_ X.1 Y.1 Z.1).inv :=
+by { ext, rw [←associator_hom_f, ←comp_f, iso.hom_inv_id], refl, }
+
+@[simp] lemma left_unitor_hom_f (X : center C) : hom.f (λ_ X).hom = (λ_ X.1).hom :=
+rfl
+
+@[simp] lemma left_unitor_inv_f (X : center C) : hom.f (λ_ X).inv = (λ_ X.1).inv :=
+by { ext, rw [←left_unitor_hom_f, ←comp_f, iso.hom_inv_id], refl, }
+
+@[simp] lemma right_unitor_hom_f (X : center C) : hom.f (ρ_ X).hom = (ρ_ X.1).hom :=
+rfl
+
+@[simp] lemma right_unitor_inv_f (X : center C) : hom.f (ρ_ X).inv = (ρ_ X.1).inv :=
+by { ext, rw [←right_unitor_hom_f, ←comp_f, iso.hom_inv_id], refl, }
+
+end
+
+section
+variables (C)
+
+/-- The forgetful monoidal functor from the Drinfeld center to the original category. -/
+@[simps]
+def forget : monoidal_functor (center C) C :=
+{ obj := λ X, X.1,
+  map := λ X Y f, f.f,
+  ε := 𝟙 (𝟙_ C),
+  μ := λ X Y, 𝟙 (X.1 ⊗ Y.1), }
+
+instance : reflects_isomorphisms (forget C).to_functor :=
+{ reflects := λ A B f i, by { dsimp at i, resetI, change is_iso (iso_mk f).hom, apply_instance, } }
+
+end
+
+/-- Auxiliary definition for the `braided_category` instance on `center C`. -/
+@[simps]
+def braiding (X Y : center C) : X ⊗ Y ≅ Y ⊗ X :=
+iso_mk ⟨(X.2.β Y.1).hom, λ U, begin
+  dsimp,
+  simp only [category.assoc],
+  rw [←is_iso.inv_comp_eq, is_iso.iso.inv_hom, ←half_braiding.monoidal_assoc,
+    ←half_braiding.naturality_assoc, half_braiding.monoidal],
+  simp,
+end⟩
+
+instance : braided_category (center C) :=
+{ braiding := braiding,
+  braiding_naturality' := λ X Y X' Y' f g, begin
+    ext,
+    dsimp,
+    rw [←tensor_id_comp_id_tensor, category.assoc, half_braiding.naturality, f.comm_assoc,
+      id_tensor_comp_tensor_id],
+  end, } -- `obviously` handles the hexagon axioms
+
+end center
+
+end category_theory