Skip to content

Commit 1ab969a

Browse files
int-y1Scott Morrison
int-y1
and
Scott Morrison
committed
feat: port CategoryTheory.Monoidal.Center (#4941)
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
1 parent 889ec59 commit 1ab969a

File tree

2 files changed

+382
-0
lines changed

2 files changed

+382
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -941,6 +941,7 @@ import Mathlib.CategoryTheory.Monad.Products
941941
import Mathlib.CategoryTheory.Monad.Types
942942
import Mathlib.CategoryTheory.Monoidal.Braided
943943
import Mathlib.CategoryTheory.Monoidal.Category
944+
import Mathlib.CategoryTheory.Monoidal.Center
944945
import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
945946
import Mathlib.CategoryTheory.Monoidal.Discrete
946947
import Mathlib.CategoryTheory.Monoidal.End

‎Mathlib/CategoryTheory/Monoidal/Center.lean‎

Lines changed: 381 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,381 @@
1+
/-
2+
Copyright (c) 2021 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module category_theory.monoidal.center
7+
! leanprover-community/mathlib commit 14b69e9f3c16630440a2cbd46f1ddad0d561dee7
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Monoidal.Braided
12+
import Mathlib.CategoryTheory.Functor.ReflectsIso
13+
import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
14+
15+
/-!
16+
# Half braidings and the Drinfeld center of a monoidal category
17+
18+
We define `Center C` to be pairs `⟨X, b⟩`, where `X : C` and `b` is a half-braiding on `X`.
19+
20+
We show that `Center C` is braided monoidal,
21+
and provide the monoidal functor `Center.forget` from `Center C` back to `C`.
22+
23+
## Future work
24+
25+
Verifying the various axioms here is done by tedious rewriting.
26+
Using the `slice` tactic may make the proofs marginally more readable.
27+
28+
More exciting, however, would be to make possible one of the following options:
29+
1. Integration with homotopy.io / globular to give "picture proofs".
30+
2. The monoidal coherence theorem, so we can ignore associators
31+
(after which most of these proofs are trivial;
32+
I'm unsure if the monoidal coherence theorem is even usable in dependent type theory).
33+
3. Automating these proofs using `rewrite_search` or some relative.
34+
35+
-/
36+
37+
38+
open CategoryTheory
39+
40+
open CategoryTheory.MonoidalCategory
41+
42+
universe v v₁ v₂ v₃ u u₁ u₂ u₃
43+
44+
noncomputable section
45+
46+
namespace CategoryTheory
47+
48+
variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory C]
49+
50+
/-- A half-braiding on `X : C` is a family of isomorphisms `X ⊗ U ≅ U ⊗ X`,
51+
monoidally natural in `U : C`.
52+
53+
Thinking of `C` as a 2-category with a single `0`-morphism, these are the same as natural
54+
transformations (in the pseudo- sense) of the identity 2-functor on `C`, which send the unique
55+
`0`-morphism to `X`.
56+
-/
57+
-- @[nolint has_nonempty_instance] -- Porting note: This linter does not exist yet.
58+
structure HalfBraiding (X : C) where
59+
β : ∀ U, X ⊗ U ≅ U ⊗ X
60+
monoidal : ∀ U U', (β (U ⊗ U')).hom =
61+
(α_ _ _ _).inv ≫
62+
((β U).hom ⊗ 𝟙 U') ≫ (α_ _ _ _).hom ≫ (𝟙 U ⊗ (β U').hom) ≫ (α_ _ _ _).inv := by
63+
aesop_cat
64+
naturality : ∀ {U U'} (f : U ⟶ U'), (𝟙 X ⊗ f) ≫ (β U').hom = (β U).hom ≫ (f ⊗ 𝟙 X) := by
65+
aesop_cat
66+
#align category_theory.half_braiding CategoryTheory.HalfBraiding
67+
68+
attribute [reassoc, simp] HalfBraiding.monoidal -- the reassoc lemma is redundant as a simp lemma
69+
70+
attribute [simp, reassoc] HalfBraiding.naturality
71+
72+
variable (C)
73+
74+
/-- The Drinfeld center of a monoidal category `C` has as objects pairs `⟨X, b⟩`, where `X : C`
75+
and `b` is a half-braiding on `X`.
76+
-/
77+
-- @[nolint has_nonempty_instance] -- Porting note: This linter does not exist yet.
78+
def Center :=
79+
Σ X : C, HalfBraiding X
80+
#align category_theory.center CategoryTheory.Center
81+
82+
namespace Center
83+
84+
variable {C}
85+
86+
/-- A morphism in the Drinfeld center of `C`. -/
87+
@[ext] -- @[nolint has_nonempty_instance] -- Porting note: This linter does not exist yet.
88+
structure Hom (X Y : Center C) where
89+
f : X.1 ⟶ Y.1
90+
comm : ∀ U, (f ⊗ 𝟙 U) ≫ (Y.2.β U).hom = (X.2.β U).hom ≫ (𝟙 U ⊗ f) := by aesop_cat
91+
#align category_theory.center.hom CategoryTheory.Center.Hom
92+
93+
attribute [reassoc (attr := simp)] Hom.comm
94+
95+
instance : Quiver (Center C) where
96+
Hom := Hom
97+
98+
@[ext]
99+
theorem ext {X Y : Center C} (f g : X ⟶ Y) (w : f.f = g.f) : f = g := by
100+
cases f; cases g; congr
101+
#align category_theory.center.ext CategoryTheory.Center.ext
102+
103+
instance : Category (Center C) where
104+
id X := { f := 𝟙 X.1 }
105+
comp f g := { f := f.f ≫ g.f }
106+
107+
@[simp]
108+
theorem id_f (X : Center C) : Hom.f (𝟙 X) = 𝟙 X.1 :=
109+
rfl
110+
#align category_theory.center.id_f CategoryTheory.Center.id_f
111+
112+
@[simp]
113+
theorem comp_f {X Y Z : Center C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).f = f.f ≫ g.f :=
114+
rfl
115+
#align category_theory.center.comp_f CategoryTheory.Center.comp_f
116+
117+
/-- Construct an isomorphism in the Drinfeld center from
118+
a morphism whose underlying morphism is an isomorphism.
119+
-/
120+
@[simps]
121+
def isoMk {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : X ≅ Y where
122+
hom := f
123+
inv := ⟨inv f.f,
124+
fun U => by simp [← cancel_epi (f.f ⊗ 𝟙 U), ← comp_tensor_id_assoc, ← id_tensor_comp]⟩
125+
#align category_theory.center.iso_mk CategoryTheory.Center.isoMk
126+
127+
instance isIso_of_f_isIso {X Y : Center C} (f : X ⟶ Y) [IsIso f.f] : IsIso f := by
128+
change IsIso (isoMk f).hom
129+
infer_instance
130+
#align category_theory.center.is_iso_of_f_is_iso CategoryTheory.Center.isIso_of_f_isIso
131+
132+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
133+
@[simps]
134+
def tensorObj (X Y : Center C) : Center C :=
135+
⟨X.1 ⊗ Y.1,
136+
{ β := fun U =>
137+
α_ _ _ _ ≪≫
138+
(Iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm ≪≫ (X.2.β U ⊗ Iso.refl Y.1) ≪≫ α_ _ _ _
139+
monoidal := fun U U' => by
140+
dsimp
141+
simp only [comp_tensor_id, id_tensor_comp, Category.assoc, HalfBraiding.monoidal]
142+
-- On the RHS, we'd like to commute `((X.snd.β U).hom ⊗ 𝟙 Y.fst) ⊗ 𝟙 U'`
143+
-- and `𝟙 U ⊗ 𝟙 X.fst ⊗ (Y.snd.β U').hom` past each other,
144+
-- but there are some associators we need to get out of the way first.
145+
slice_rhs 6 8 => rw [pentagon]
146+
slice_rhs 5 6 => rw [associator_naturality]
147+
slice_rhs 7 8 => rw [← associator_naturality]
148+
slice_rhs 6 7 =>
149+
rw [tensor_id, tensor_id, tensor_id_comp_id_tensor, ← id_tensor_comp_tensor_id,
150+
← tensor_id, ← tensor_id]
151+
-- Now insert associators as needed to make the four half-braidings look identical
152+
slice_rhs 10 10 => rw [associator_inv_conjugation]
153+
slice_rhs 7 7 => rw [associator_inv_conjugation]
154+
slice_rhs 6 6 => rw [associator_conjugation]
155+
slice_rhs 3 3 => rw [associator_conjugation]
156+
-- Finish with an application of the coherence theorem.
157+
coherence
158+
naturality := fun f => by
159+
dsimp
160+
rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc,
161+
id_tensor_associator_naturality_assoc, ← id_tensor_comp_assoc, HalfBraiding.naturality,
162+
id_tensor_comp_assoc, associator_inv_naturality_assoc, ← comp_tensor_id_assoc,
163+
HalfBraiding.naturality, comp_tensor_id_assoc, associator_naturality, ← tensor_id] }⟩
164+
#align category_theory.center.tensor_obj CategoryTheory.Center.tensorObj
165+
166+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
167+
@[simps]
168+
def tensorHom {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
169+
tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂ where
170+
f := f.f ⊗ g.f
171+
comm U := by
172+
dsimp
173+
rw [Category.assoc, Category.assoc, Category.assoc, Category.assoc, associator_naturality_assoc,
174+
← tensor_id_comp_id_tensor, Category.assoc, ← id_tensor_comp_assoc, g.comm,
175+
id_tensor_comp_assoc, tensor_id_comp_id_tensor_assoc, ← id_tensor_comp_tensor_id,
176+
Category.assoc, associator_inv_naturality_assoc, id_tensor_associator_inv_naturality_assoc,
177+
tensor_id, id_tensor_comp_tensor_id_assoc, ← tensor_id_comp_id_tensor g.f, Category.assoc,
178+
← comp_tensor_id_assoc, f.comm, comp_tensor_id_assoc, id_tensor_associator_naturality,
179+
associator_naturality_assoc, ← id_tensor_comp, tensor_id_comp_id_tensor]
180+
#align category_theory.center.tensor_hom CategoryTheory.Center.tensorHom
181+
182+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
183+
@[simps]
184+
def tensorUnit : Center C :=
185+
⟨𝟙_ C,
186+
{ β := fun U => λ_ U ≪≫ (ρ_ U).symm
187+
monoidal := fun U U' => by simp
188+
naturality := fun f => by
189+
dsimp
190+
rw [leftUnitor_naturality_assoc, rightUnitor_inv_naturality, Category.assoc] }⟩
191+
#align category_theory.center.tensor_unit CategoryTheory.Center.tensorUnit
192+
193+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
194+
def associator (X Y Z : Center C) : tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) :=
195+
isoMk
196+
⟨(α_ X.1 Y.1 Z.1).hom, fun U => by
197+
dsimp
198+
simp only [comp_tensor_id, id_tensor_comp, ← tensor_id, associator_conjugation]
199+
coherence⟩
200+
#align category_theory.center.associator CategoryTheory.Center.associator
201+
202+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
203+
def leftUnitor (X : Center C) : tensorObj tensorUnit X ≅ X :=
204+
isoMk
205+
⟨(λ_ X.1).hom, fun U => by
206+
dsimp
207+
simp only [Category.comp_id, Category.assoc, tensor_inv_hom_id, comp_tensor_id,
208+
tensor_id_comp_id_tensor, triangle_assoc_comp_right_inv]
209+
rw [← leftUnitor_tensor, leftUnitor_naturality, leftUnitor_tensor'_assoc]⟩
210+
#align category_theory.center.left_unitor CategoryTheory.Center.leftUnitor
211+
212+
/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
213+
def rightUnitor (X : Center C) : tensorObj X tensorUnit ≅ X :=
214+
isoMk
215+
⟨(ρ_ X.1).hom, fun U => by
216+
dsimp
217+
simp only [tensor_id_comp_id_tensor_assoc, triangle_assoc, id_tensor_comp, Category.assoc]
218+
rw [← tensor_id_comp_id_tensor_assoc (ρ_ U).inv, cancel_epi, ← rightUnitor_tensor_inv_assoc,
219+
← rightUnitor_inv_naturality_assoc]
220+
simp⟩
221+
#align category_theory.center.right_unitor CategoryTheory.Center.rightUnitor
222+
223+
section
224+
225+
attribute [local simp] associator_naturality leftUnitor_naturality rightUnitor_naturality pentagon
226+
227+
attribute [local simp] Center.associator Center.leftUnitor Center.rightUnitor
228+
229+
instance : MonoidalCategory (Center C) where
230+
tensorObj X Y := tensorObj X Y
231+
tensorHom f g := tensorHom f g
232+
tensorUnit' := tensorUnit
233+
associator := associator
234+
leftUnitor := leftUnitor
235+
rightUnitor := rightUnitor
236+
237+
@[simp]
238+
theorem tensor_fst (X Y : Center C) : (X ⊗ Y).1 = X.1 ⊗ Y.1 :=
239+
rfl
240+
#align category_theory.center.tensor_fst CategoryTheory.Center.tensor_fst
241+
242+
@[simp]
243+
theorem tensor_β (X Y : Center C) (U : C) :
244+
(X ⊗ Y).2.β U =
245+
α_ _ _ _ ≪≫
246+
(Iso.refl X.1 ⊗ Y.2.β U) ≪≫ (α_ _ _ _).symm ≪≫ (X.2.β U ⊗ Iso.refl Y.1) ≪≫ α_ _ _ _ :=
247+
rfl
248+
#align category_theory.center.tensor_β CategoryTheory.Center.tensor_β
249+
250+
@[simp]
251+
theorem tensor_f {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (f ⊗ g).f = f.f ⊗ g.f :=
252+
rfl
253+
#align category_theory.center.tensor_f CategoryTheory.Center.tensor_f
254+
255+
@[simp]
256+
theorem tensorUnit_β (U : C) : (𝟙_ (Center C)).2.β U = λ_ U ≪≫ (ρ_ U).symm :=
257+
rfl
258+
#align category_theory.center.tensor_unit_β CategoryTheory.Center.tensorUnit_β
259+
260+
@[simp]
261+
theorem associator_hom_f (X Y Z : Center C) : Hom.f (α_ X Y Z).hom = (α_ X.1 Y.1 Z.1).hom :=
262+
rfl
263+
#align category_theory.center.associator_hom_f CategoryTheory.Center.associator_hom_f
264+
265+
@[simp]
266+
theorem associator_inv_f (X Y Z : Center C) : Hom.f (α_ X Y Z).inv = (α_ X.1 Y.1 Z.1).inv := by
267+
apply Iso.inv_ext' -- Porting note: Originally `ext`
268+
rw [← associator_hom_f, ← comp_f, Iso.hom_inv_id]; rfl
269+
#align category_theory.center.associator_inv_f CategoryTheory.Center.associator_inv_f
270+
271+
@[simp]
272+
theorem leftUnitor_hom_f (X : Center C) : Hom.f (λ_ X).hom = (λ_ X.1).hom :=
273+
rfl
274+
#align category_theory.center.left_unitor_hom_f CategoryTheory.Center.leftUnitor_hom_f
275+
276+
@[simp]
277+
theorem leftUnitor_inv_f (X : Center C) : Hom.f (λ_ X).inv = (λ_ X.1).inv := by
278+
apply Iso.inv_ext' -- Porting note: Originally `ext`
279+
rw [← leftUnitor_hom_f, ← comp_f, Iso.hom_inv_id]; rfl
280+
#align category_theory.center.left_unitor_inv_f CategoryTheory.Center.leftUnitor_inv_f
281+
282+
@[simp]
283+
theorem rightUnitor_hom_f (X : Center C) : Hom.f (ρ_ X).hom = (ρ_ X.1).hom :=
284+
rfl
285+
#align category_theory.center.right_unitor_hom_f CategoryTheory.Center.rightUnitor_hom_f
286+
287+
@[simp]
288+
theorem rightUnitor_inv_f (X : Center C) : Hom.f (ρ_ X).inv = (ρ_ X.1).inv := by
289+
apply Iso.inv_ext' -- Porting note: Originally `ext`
290+
rw [← rightUnitor_hom_f, ← comp_f, Iso.hom_inv_id]; rfl
291+
#align category_theory.center.right_unitor_inv_f CategoryTheory.Center.rightUnitor_inv_f
292+
293+
end
294+
295+
section
296+
297+
variable (C)
298+
299+
/-- The forgetful monoidal functor from the Drinfeld center to the original category. -/
300+
@[simps]
301+
def forget : MonoidalFunctor (Center C) C where
302+
obj X := X.1
303+
map f := f.f
304+
ε := 𝟙 (𝟙_ C)
305+
μ X Y := 𝟙 (X.1 ⊗ Y.1)
306+
#align category_theory.center.forget CategoryTheory.Center.forget
307+
308+
instance : ReflectsIsomorphisms (forget C).toFunctor where
309+
reflects f i := by dsimp at i; change IsIso (isoMk f).hom; infer_instance
310+
311+
end
312+
313+
/-- Auxiliary definition for the `BraidedCategory` instance on `Center C`. -/
314+
@[simps!]
315+
def braiding (X Y : Center C) : X ⊗ Y ≅ Y ⊗ X :=
316+
isoMk
317+
⟨(X.2.β Y.1).hom, fun U => by
318+
dsimp
319+
simp only [Category.assoc]
320+
rw [← IsIso.inv_comp_eq, IsIso.Iso.inv_hom, ← HalfBraiding.monoidal_assoc,
321+
← HalfBraiding.naturality_assoc, HalfBraiding.monoidal]
322+
simp⟩
323+
#align category_theory.center.braiding CategoryTheory.Center.braiding
324+
325+
instance braidedCategoryCenter : BraidedCategory (Center C) where
326+
braiding := braiding
327+
braiding_naturality f g := by
328+
ext
329+
dsimp
330+
rw [← tensor_id_comp_id_tensor, Category.assoc, HalfBraiding.naturality, f.comm_assoc,
331+
id_tensor_comp_tensor_id]
332+
#align category_theory.center.braided_category_center CategoryTheory.Center.braidedCategoryCenter
333+
334+
-- `aesop_cat` handles the hexagon axioms
335+
section
336+
337+
variable [BraidedCategory C]
338+
339+
open BraidedCategory
340+
341+
/-- Auxiliary construction for `ofBraided`. -/
342+
@[simps]
343+
def ofBraidedObj (X : C) : Center C :=
344+
⟨X, {
345+
β := fun Y => β_ X Y
346+
monoidal := fun U U' => by
347+
rw [Iso.eq_inv_comp, ← Category.assoc, ← Category.assoc, Iso.eq_comp_inv, Category.assoc,
348+
Category.assoc]
349+
exact hexagon_forward X U U' }⟩
350+
#align category_theory.center.of_braided_obj CategoryTheory.Center.ofBraidedObj
351+
352+
variable (C)
353+
354+
/-- The functor lifting a braided category to its center, using the braiding as the half-braiding.
355+
-/
356+
@[simps]
357+
def ofBraided : MonoidalFunctor C (Center C) where
358+
obj := ofBraidedObj
359+
map f :=
360+
{ f
361+
comm := fun U => braiding_naturality _ _ }
362+
ε :=
363+
{ f := 𝟙 _
364+
comm := fun U => by
365+
dsimp
366+
rw [tensor_id, Category.id_comp, tensor_id, Category.comp_id, ← braiding_rightUnitor,
367+
Category.assoc, Iso.hom_inv_id, Category.comp_id] }
368+
μ X Y :=
369+
{ f := 𝟙 _
370+
comm := fun U => by
371+
dsimp
372+
rw [tensor_id, tensor_id, Category.id_comp, Category.comp_id, ← Iso.inv_comp_eq,
373+
← Category.assoc, ← Category.assoc, ← Iso.comp_inv_eq, Category.assoc, hexagon_reverse,
374+
Category.assoc] }
375+
#align category_theory.center.of_braided CategoryTheory.Center.ofBraided
376+
377+
end
378+
379+
end Center
380+
381+
end CategoryTheory

0 commit comments

Comments
 (0)