mathlib3 documentation

category_theory.monoidal.center

Half braidings and the Drinfeld center of a monoidal category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

Integration with homotopy.io / globular to give "picture proofs".
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).
Automating these proofs using rewrite_search or some relative.

@[nolint]

structure category_theory.half_braiding {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : C) :

Type (max u₁ v₁)

β : Π (U : C), X ⊗ U ≅ U ⊗ X
monoidal' : (∀ (U U' : C), (self.β (U ⊗ U')).hom = (α_ X U U').inv ≫ ((self.β U).hom ⊗ 𝟙 U') ≫ (α_ U X U').hom ≫ (𝟙 U ⊗ (self.β U').hom) ≫ (α_ U U' X).inv) . "obviously"
naturality' : (∀ {U U' : C} (f : U ⟶ U'), (𝟙 X ⊗ f) ≫ (self.β U').hom = (self.β U).hom ≫ (f ⊗ 𝟙 X)) . "obviously"

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.

Instances for category_theory.half_braiding

category_theory.half_braiding.has_sizeof_inst

@[simp]

theorem category_theory.half_braiding.monoidal {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X : C} (self : category_theory.half_braiding X) (U U' : C) :

(self.β (U ⊗ U')).hom = (α_ X U U').inv ≫ ((self.β U).hom ⊗ 𝟙 U') ≫ (α_ U X U').hom ≫ (𝟙 U ⊗ (self.β U').hom) ≫ (α_ U U' X).inv

theorem category_theory.half_braiding.monoidal_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X : C} (self : category_theory.half_braiding X) (U U' : C) {X' : C} (f' : (U ⊗ U') ⊗ X ⟶ X') :

(self.β (U ⊗ U')).hom ≫ f' = (α_ X U U').inv ≫ ((self.β U).hom ⊗ 𝟙 U') ≫ (α_ U X U').hom ≫ (𝟙 U ⊗ (self.β U').hom) ≫ (α_ U U' X).inv ≫ f'

@[simp]

theorem category_theory.half_braiding.naturality {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X : C} (self : category_theory.half_braiding X) {U U' : C} (f : U ⟶ U') :

(𝟙 X ⊗ f) ≫ (self.β U').hom = (self.β U).hom ≫ (f ⊗ 𝟙 X)

@[simp]

theorem category_theory.half_braiding.naturality_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X : C} (self : category_theory.half_braiding X) {U U' : C} (f : U ⟶ U') {X' : C} (f' : U' ⊗ X ⟶ X') :

(𝟙 X ⊗ f) ≫ (self.β U').hom ≫ f' = (self.β U).hom ≫ (f ⊗ 𝟙 X) ≫ f'

@[nolint]

def category_theory.center (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

Type (max u₁ v₁)

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.

Equations

category_theory.center C = Σ (X : C), category_theory.half_braiding X

Instances for category_theory.center

theorem category_theory.center.hom.ext {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {X Y : category_theory.center C} (x y : X.hom Y) (h : x.f = y.f) :

x = y

@[nolint, ext]

structure category_theory.center.hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

Type v₁

f : X.fst ⟶ Y.fst
comm' : (∀ (U : C), (self.f ⊗ 𝟙 U) ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ (𝟙 U ⊗ self.f)) . "obviously"

A morphism in the Drinfeld center of C.

Instances for category_theory.center.hom

category_theory.center.hom.has_sizeof_inst

theorem category_theory.center.hom.ext_iff {C : Type u₁} {_inst_1 : category_theory.category C} {_inst_2 : category_theory.monoidal_category C} {X Y : category_theory.center C} (x y : X.hom Y) :

x = y ↔ x.f = y.f

@[simp]

theorem category_theory.center.hom.comm {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (self : X.hom Y) (U : C) :

(self.f ⊗ 𝟙 U) ≫ (Y.snd.β U).hom = (X.snd.β U).hom ≫ (𝟙 U ⊗ self.f)

@[simp]

theorem category_theory.center.hom.comm_assoc {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (self : X.hom Y) (U : C) {X' : C} (f' : U ⊗ Y.fst ⟶ X') :

(self.f ⊗ 𝟙 U) ≫ (Y.snd.β U).hom ≫ f' = (X.snd.β U).hom ≫ (𝟙 U ⊗ self.f) ≫ f'

@[protected, instance]

def category_theory.center.category_theory.category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.category (category_theory.center C)

Equations

category_theory.center.category_theory.category = {to_category_struct := {to_quiver := {hom := category_theory.center.hom _inst_2}, id := λ (X : category_theory.center C), {f := 𝟙 X.fst, comm' := _}, comp := λ (X Y Z : category_theory.center C) (f : X ⟶ Y) (g : Y ⟶ Z), {f := f.f ≫ g.f, comm' := _}}, id_comp' := _, comp_id' := _, assoc' := _}

@[simp]

theorem category_theory.center.id_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(𝟙 X).f = 𝟙 X.fst

@[simp]

theorem category_theory.center.comp_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z : category_theory.center C} (f : X ⟶ Y) (g : Y ⟶ Z) :

(f ≫ g).f = f.f ≫ g.f

@[ext]

theorem category_theory.center.ext {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (f g : X ⟶ Y) (w : f.f = g.f) :

f = g

@[simp]

theorem category_theory.center.iso_mk_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (f : X ⟶ Y) [category_theory.is_iso f.f] :

(category_theory.center.iso_mk f).hom = f

noncomputable def category_theory.center.iso_mk {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (f : X ⟶ Y) [category_theory.is_iso f.f] :

X ≅ Y

Construct an isomorphism in the Drinfeld center from a morphism whose underlying morphism is an isomorphism.

Equations

category_theory.center.iso_mk f = {hom := f, inv := {f := category_theory.inv f.f _inst_3, comm' := _}, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem category_theory.center.iso_mk_inv_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (f : X ⟶ Y) [category_theory.is_iso f.f] :

(category_theory.center.iso_mk f).inv.f = category_theory.inv f.f

@[protected, instance]

def category_theory.center.is_iso_of_f_is_iso {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X Y : category_theory.center C} (f : X ⟶ Y) [category_theory.is_iso f.f] :

category_theory.is_iso f

def category_theory.center.tensor_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

category_theory.center C

Auxiliary definition for the monoidal_category instance on center C.

Equations

X.tensor_obj Y = ⟨X.fst ⊗ Y.fst, {β := λ (U : C), α_ X.fst Y.fst U ≪≫ (category_theory.iso.refl X.fst ⊗ Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ (X.snd.β U ⊗ category_theory.iso.refl Y.fst) ≪≫ α_ U X.fst Y.fst, monoidal' := _, naturality' := _}⟩

@[simp]

theorem category_theory.center.tensor_obj_fst {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

(X.tensor_obj Y).fst = X.fst ⊗ Y.fst

@[simp]

theorem category_theory.center.tensor_obj_snd_β {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) (U : C) :

(X.tensor_obj Y).snd.β U = α_ X.fst Y.fst U ≪≫ (category_theory.iso.refl X.fst ⊗ Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ (X.snd.β U ⊗ category_theory.iso.refl Y.fst) ≪≫ α_ U X.fst Y.fst

@[simp]

theorem category_theory.center.tensor_hom_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X₁ Y₁ X₂ Y₂ : category_theory.center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :

(category_theory.center.tensor_hom f g).f = f.f ⊗ g.f

def category_theory.center.tensor_hom {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X₁ Y₁ X₂ Y₂ : category_theory.center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :

X₁.tensor_obj X₂ ⟶ Y₁.tensor_obj Y₂

Auxiliary definition for the monoidal_category instance on center C.

Equations

category_theory.center.tensor_hom f g = {f := f.f ⊗ g.f, comm' := _}

def category_theory.center.tensor_unit {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.center C

Auxiliary definition for the monoidal_category instance on center C.

Equations

category_theory.center.tensor_unit = ⟨𝟙_ C _inst_2, {β := λ (U : C), λ_ U ≪≫ (ρ_ U).symm, monoidal' := _, naturality' := _}⟩

@[simp]

theorem category_theory.center.tensor_unit_fst {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.center.tensor_unit.fst = 𝟙_ C

@[simp]

theorem category_theory.center.tensor_unit_snd_β {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (U : C) :

category_theory.center.tensor_unit.snd.β U = λ_ U ≪≫ (ρ_ U).symm

noncomputable def category_theory.center.associator {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : category_theory.center C) :

(X.tensor_obj Y).tensor_obj Z ≅ X.tensor_obj (Y.tensor_obj Z)

Auxiliary definition for the monoidal_category instance on center C.

Equations

X.associator Y Z = category_theory.center.iso_mk {f := (α_ X.fst Y.fst Z.fst).hom, comm' := _}

noncomputable def category_theory.center.left_unitor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

category_theory.center.tensor_unit.tensor_obj X ≅ X

Auxiliary definition for the monoidal_category instance on center C.

Equations

X.left_unitor = category_theory.center.iso_mk {f := (λ_ X.fst).hom, comm' := _}

noncomputable def category_theory.center.right_unitor {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

X.tensor_obj category_theory.center.tensor_unit ≅ X

Auxiliary definition for the monoidal_category instance on center C.

Equations

X.right_unitor = category_theory.center.iso_mk {f := (ρ_ X.fst).hom, comm' := _}

@[protected, instance]

noncomputable def category_theory.center.category_theory.monoidal_category {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_category (category_theory.center C)

Equations

category_theory.center.category_theory.monoidal_category = {tensor_obj := λ (X Y : category_theory.center C), X.tensor_obj Y, tensor_hom := λ (X₁ Y₁ X₂ Y₂ : category_theory.center C) (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂), category_theory.center.tensor_hom f g, tensor_id' := _, tensor_comp' := _, tensor_unit := category_theory.center.tensor_unit _inst_2, associator := category_theory.center.associator _inst_2, associator_naturality' := _, left_unitor := category_theory.center.left_unitor _inst_2, left_unitor_naturality' := _, right_unitor := category_theory.center.right_unitor _inst_2, right_unitor_naturality' := _, pentagon' := _, triangle' := _}

@[simp]

theorem category_theory.center.tensor_fst {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

(X ⊗ Y).fst = X.fst ⊗ Y.fst

@[simp]

theorem category_theory.center.tensor_β {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) (U : C) :

(X ⊗ Y).snd.β U = α_ X.fst Y.fst U ≪≫ (category_theory.iso.refl X.fst ⊗ Y.snd.β U) ≪≫ (α_ X.fst U Y.fst).symm ≪≫ (X.snd.β U ⊗ category_theory.iso.refl Y.fst) ≪≫ α_ U X.fst Y.fst

@[simp]

theorem category_theory.center.tensor_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] {X₁ Y₁ X₂ Y₂ : category_theory.center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :

(f ⊗ g).f = f.f ⊗ g.f

@[simp]

theorem category_theory.center.tensor_unit_β {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (U : C) :

(𝟙_ (category_theory.center C)).snd.β U = λ_ U ≪≫ (ρ_ U).symm

@[simp]

theorem category_theory.center.associator_hom_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : category_theory.center C) :

(α_ X Y Z).hom.f = (α_ X.fst Y.fst Z.fst).hom

@[simp]

theorem category_theory.center.associator_inv_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y Z : category_theory.center C) :

(α_ X Y Z).inv.f = (α_ X.fst Y.fst Z.fst).inv

@[simp]

theorem category_theory.center.left_unitor_hom_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(λ_ X).hom.f = (λ_ X.fst).hom

@[simp]

theorem category_theory.center.left_unitor_inv_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(λ_ X).inv.f = (λ_ X.fst).inv

@[simp]

theorem category_theory.center.right_unitor_hom_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(ρ_ X).hom.f = (ρ_ X.fst).hom

@[simp]

theorem category_theory.center.right_unitor_inv_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(ρ_ X).inv.f = (ρ_ X.fst).inv

def category_theory.center.forget (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.monoidal_functor (category_theory.center C) C

The forgetful monoidal functor from the Drinfeld center to the original category.

Equations

category_theory.center.forget C = {to_lax_monoidal_functor := {to_functor := {obj := λ (X : category_theory.center C), X.fst, map := λ (X Y : category_theory.center C) (f : X ⟶ Y), f.f, map_id' := _, map_comp' := _}, ε := 𝟙 (𝟙_ C), μ := λ (X Y : category_theory.center C), 𝟙 (X.fst ⊗ Y.fst), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.center.forget_to_lax_monoidal_functor_to_functor_map (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) (f : X ⟶ Y) :

(category_theory.center.forget C).to_lax_monoidal_functor.to_functor.map f = f.f

@[simp]

theorem category_theory.center.forget_to_lax_monoidal_functor_ε (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

(category_theory.center.forget C).to_lax_monoidal_functor.ε = 𝟙 (𝟙_ C)

@[simp]

theorem category_theory.center.forget_to_lax_monoidal_functor_to_functor_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X : category_theory.center C) :

(category_theory.center.forget C).to_lax_monoidal_functor.to_functor.obj X = X.fst

@[simp]

theorem category_theory.center.forget_to_lax_monoidal_functor_μ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

(category_theory.center.forget C).to_lax_monoidal_functor.μ X Y = 𝟙 (X.fst ⊗ Y.fst)

@[protected, instance]

def category_theory.center.to_functor.category_theory.reflects_isomorphisms (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.reflects_isomorphisms (category_theory.center.forget C).to_lax_monoidal_functor.to_functor

@[simp]

theorem category_theory.center.braiding_hom_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

(X.braiding Y).hom.f = (X.snd.β Y.fst).hom

noncomputable def category_theory.center.braiding {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

X ⊗ Y ≅ Y ⊗ X

Auxiliary definition for the braided_category instance on center C.

Equations

X.braiding Y = category_theory.center.iso_mk {f := (X.snd.β Y.fst).hom, comm' := _}

@[simp]

theorem category_theory.center.braiding_inv_f {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] (X Y : category_theory.center C) :

(X.braiding Y).inv.f = (X.snd.β Y.fst).inv

@[protected, instance]

noncomputable def category_theory.center.braided_category_center {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] :

category_theory.braided_category (category_theory.center C)

Equations

category_theory.center.braided_category_center = {braiding := category_theory.center.braiding _inst_2, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}

def category_theory.center.of_braided_obj {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

category_theory.center C

Auxiliary construction for of_braided.

Equations

category_theory.center.of_braided_obj X = ⟨X, {β := λ (Y : C), β_ X Y, monoidal' := _, naturality' := _}⟩

@[simp]

theorem category_theory.center.of_braided_obj_fst {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(category_theory.center.of_braided_obj X).fst = X

@[simp]

theorem category_theory.center.of_braided_obj_snd_β {C : Type u₁} [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X Y : C) :

(category_theory.center.of_braided_obj X).snd.β Y = β_ X Y

noncomputable def category_theory.center.of_braided (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

category_theory.monoidal_functor C (category_theory.center C)

The functor lifting a braided category to its center, using the braiding as the half-braiding.

Equations

category_theory.center.of_braided C = {to_lax_monoidal_functor := {to_functor := {obj := category_theory.center.of_braided_obj _inst_3, map := λ (X X' : C) (f : X ⟶ X'), {f := f, comm' := _}, map_id' := _, map_comp' := _}, ε := {f := 𝟙 (𝟙_ (category_theory.center C)).fst, comm' := _}, μ := λ (X Y : C), {f := 𝟙 ({obj := category_theory.center.of_braided_obj _inst_3, map := λ (X X' : C) (f : X ⟶ X'), {f := f, comm' := _}, map_id' := _, map_comp' := _}.obj X ⊗ {obj := category_theory.center.of_braided_obj _inst_3, map := λ (X X' : C) (f : X ⟶ X'), {f := f, comm' := _}, map_id' := _, map_comp' := _}.obj Y).fst, comm' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := _, μ_is_iso := _}

@[simp]

theorem category_theory.center.of_braided_to_lax_monoidal_functor_ε_f (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] :

(category_theory.center.of_braided C).to_lax_monoidal_functor.ε.f = 𝟙 (𝟙_ (category_theory.center C)).fst

@[simp]

theorem category_theory.center.of_braided_to_lax_monoidal_functor_μ_f (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X Y : C) :

((category_theory.center.of_braided C).to_lax_monoidal_functor.μ X Y).f = 𝟙 ({obj := category_theory.center.of_braided_obj _inst_3, map := λ (X X' : C) (f : X ⟶ X'), {f := f, comm' := _}, map_id' := _, map_comp' := _}.obj X ⊗ {obj := category_theory.center.of_braided_obj _inst_3, map := λ (X X' : C) (f : X ⟶ X'), {f := f, comm' := _}, map_id' := _, map_comp' := _}.obj Y).fst

@[simp]

theorem category_theory.center.of_braided_to_lax_monoidal_functor_to_functor_map_f (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X X' : C) (f : X ⟶ X') :

((category_theory.center.of_braided C).to_lax_monoidal_functor.to_functor.map f).f = f

@[simp]

theorem category_theory.center.of_braided_to_lax_monoidal_functor_to_functor_obj (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X : C) :

(category_theory.center.of_braided C).to_lax_monoidal_functor.to_functor.obj X = category_theory.center.of_braided_obj X