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.

Implementation notes

Verifying the various axioms directly requires 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).
3. Automating these proofs using rewrite_search or some relative.

In this file, we take the second approach using the monoidal composition ⊗≫ and the coherence tactic.

structure CategoryTheory.HalfBraiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : C) : Type (max u₁ v₁)

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.

• β : (U : C) → CategoryTheory.MonoidalCategory.tensorObj X U ≅ CategoryTheory.MonoidalCategory.tensorObj U X
• monoidal : ∀ (U U' : C), (self.β (CategoryTheory.MonoidalCategory.tensorObj U U')).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X U U').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.β U).hom U') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator U X U').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U (self.β U').hom) (CategoryTheory.MonoidalCategory.associator U U' X).inv)))
• naturality : ∀ {U U' : C} (f : U ⟶ U'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (self.β U').hom = CategoryTheory.CategoryStruct.comp (self.β U).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)

@[simp]

theorem CategoryTheory.HalfBraiding.monoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} (self : CategoryTheory.HalfBraiding X) (U : C) (U' : C) : (self.β (CategoryTheory.MonoidalCategory.tensorObj U U')).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X U U').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.β U).hom U') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator U X U').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U (self.β U').hom) (CategoryTheory.MonoidalCategory.associator U U' X).inv)))

@[simp]

theorem CategoryTheory.HalfBraiding.naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} (self : CategoryTheory.HalfBraiding X) {U : C} {U' : C} (f : U ⟶ U') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (self.β U').hom = CategoryTheory.CategoryStruct.comp (self.β U).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)

theorem CategoryTheory.HalfBraiding.monoidal_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} (self : CategoryTheory.HalfBraiding X) (U : C) (U' : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj U U') X ⟶ Z) : CategoryTheory.CategoryStruct.comp (self.β (CategoryTheory.MonoidalCategory.tensorObj U U')).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X U U').inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.β U).hom U') (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator U X U').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U (self.β U').hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator U U' X).inv h))))

theorem CategoryTheory.HalfBraiding.naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : C} (self : CategoryTheory.HalfBraiding X) {U : C} {U' : C} (f : U ⟶ U') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj U' X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (CategoryTheory.CategoryStruct.comp (self.β U').hom h) = CategoryTheory.CategoryStruct.comp (self.β U).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X) h)

def CategoryTheory.Center (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max u₁ 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

• CategoryTheory.Center C = ((X : C) × CategoryTheory.HalfBraiding X)

structure CategoryTheory.Center.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : Type v₁

A morphism in the Drinfeld center of C.

• f : X.fst ⟶ Y.fst
• comm : ∀ (U : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.f U) (Y.snd.β U).hom = CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategory.whiskerLeft U self.f)

theorem CategoryTheory.Center.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {X Y : CategoryTheory.Center C} {x y : X.Hom Y}, x.f = y.f → x = y

@[simp]

theorem CategoryTheory.Center.Hom.comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (self : X.Hom Y) (U : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.f U) (Y.snd.β U).hom = CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.MonoidalCategory.whiskerLeft U self.f)

@[simp]

theorem CategoryTheory.Center.Hom.comm_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (self : X.Hom Y) (U : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj U Y.fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.f U) (CategoryTheory.CategoryStruct.comp (Y.snd.β U).hom h) = CategoryTheory.CategoryStruct.comp (X.snd.β U).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U self.f) h)

instance CategoryTheory.Center.instQuiver {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Quiver (CategoryTheory.Center C)

Equations

• CategoryTheory.Center.instQuiver = { Hom := CategoryTheory.Center.Hom }

theorem CategoryTheory.Center.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (f : X ⟶ Y) (g : X ⟶ Y) (w : f.f = g.f) : f = g

instance CategoryTheory.Center.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Center C)

Equations

• CategoryTheory.Center.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Center.id_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.fst

@[simp]

theorem CategoryTheory.Center.comp_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} {Z : CategoryTheory.Center C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f

def CategoryTheory.Center.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (f : X ⟶ Y) [CategoryTheory.IsIso f.f] : X ≅ Y

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

Equations

• CategoryTheory.Center.isoMk f = { hom := f, inv := { f := CategoryTheory.inv f.f, comm := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Center.isoMk_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (f : X ⟶ Y) [CategoryTheory.IsIso f.f] : (CategoryTheory.Center.isoMk f).hom = f

@[simp]

theorem CategoryTheory.Center.isoMk_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (f : X ⟶ Y) [CategoryTheory.IsIso f.f] : (CategoryTheory.Center.isoMk f).inv.f = CategoryTheory.inv f.f

instance CategoryTheory.Center.isIso_of_f_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : CategoryTheory.Center C} {Y : CategoryTheory.Center C} (f : X ⟶ Y) [CategoryTheory.IsIso f.f] : CategoryTheory.IsIso f

Equations

• ⋯ = ⋯

def CategoryTheory.Center.tensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : CategoryTheory.Center C

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Center.tensorObj_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : (X.tensorObj Y).fst = CategoryTheory.MonoidalCategory.tensorObj X.fst Y.fst

@[simp]

theorem CategoryTheory.Center.tensorObj_snd_β {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) (U : C) : (X.tensorObj Y).snd.β U = CategoryTheory.MonoidalCategory.associator X.fst Y.fst U ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (CategoryTheory.MonoidalCategory.associator X.fst U Y.fst).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫ CategoryTheory.MonoidalCategory.associator U X.fst Y.fst

theorem CategoryTheory.Center.whiskerLeft_comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) {Y₁ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) (U : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f) U) ((X.tensorObj Y₂).snd.β U).hom = CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₁).snd.β U).hom (CategoryTheory.MonoidalCategory.whiskerLeft U (CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f))

theorem CategoryTheory.Center.whiskerLeft_comm_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) {Y₁ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) (U : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj U (X.tensorObj Y₂).fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f) U) (CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₂).snd.β U).hom h) = CategoryTheory.CategoryStruct.comp ((X.tensorObj Y₁).snd.β U).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U (CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f)) h)

def CategoryTheory.Center.whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) {Y₁ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) : X.tensorObj Y₁ ⟶ X.tensorObj Y₂

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• X.whiskerLeft f = { f := CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f, comm := ⋯ }

theorem CategoryTheory.Center.whiskerRight_comm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) (U : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst) U) ((X₂.tensorObj Y).snd.β U).hom = CategoryTheory.CategoryStruct.comp ((X₁.tensorObj Y).snd.β U).hom (CategoryTheory.MonoidalCategory.whiskerLeft U (CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst))

theorem CategoryTheory.Center.whiskerRight_comm_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) (U : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj U (X₂.tensorObj Y).fst ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst) U) (CategoryTheory.CategoryStruct.comp ((X₂.tensorObj Y).snd.β U).hom h) = CategoryTheory.CategoryStruct.comp ((X₁.tensorObj Y).snd.β U).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft U (CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst)) h)

def CategoryTheory.Center.whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) : X₁.tensorObj Y ⟶ X₂.tensorObj Y

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• CategoryTheory.Center.whiskerRight f Y = { f := CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst, comm := ⋯ }

def CategoryTheory.Center.tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {Y₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : X₁.tensorObj X₂ ⟶ Y₁.tensorObj Y₂

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• CategoryTheory.Center.tensorHom f g = { f := CategoryTheory.MonoidalCategory.tensorHom f.f g.f, comm := ⋯ }

@[simp]

theorem CategoryTheory.Center.tensorHom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {Y₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.Center.tensorHom f g).f = CategoryTheory.MonoidalCategory.tensorHom f.f g.f

def CategoryTheory.Center.tensorUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Center C

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Center.tensorUnit_snd_β {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (U : C) : CategoryTheory.Center.tensorUnit.snd.β U = CategoryTheory.MonoidalCategory.leftUnitor U ≪≫ (CategoryTheory.MonoidalCategory.rightUnitor U).symm

@[simp]

theorem CategoryTheory.Center.tensorUnit_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.Center.tensorUnit.fst = 𝟙_ C

def CategoryTheory.Center.associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) (Z : CategoryTheory.Center C) : (X.tensorObj Y).tensorObj Z ≅ X.tensorObj (Y.tensorObj Z)

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• X.associator Y Z = CategoryTheory.Center.isoMk { f := (CategoryTheory.MonoidalCategory.associator X.fst Y.fst Z.fst).hom, comm := ⋯ }

def CategoryTheory.Center.leftUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : CategoryTheory.Center.tensorUnit.tensorObj X ≅ X

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• X.leftUnitor = CategoryTheory.Center.isoMk { f := (CategoryTheory.MonoidalCategory.leftUnitor X.fst).hom, comm := ⋯ }

def CategoryTheory.Center.rightUnitor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : X.tensorObj CategoryTheory.Center.tensorUnit ≅ X

Auxiliary definition for the MonoidalCategory instance on Center C.

Equations

• X.rightUnitor = CategoryTheory.Center.isoMk { f := (CategoryTheory.MonoidalCategory.rightUnitor X.fst).hom, comm := ⋯ }

instance CategoryTheory.Center.instMonoidalCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalCategory (CategoryTheory.Center C)

Equations

• CategoryTheory.Center.instMonoidalCategory = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Center.tensor_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.tensorObj X Y).fst = CategoryTheory.MonoidalCategory.tensorObj X.fst Y.fst

@[simp]

theorem CategoryTheory.Center.tensor_β {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) (U : C) : (CategoryTheory.MonoidalCategory.tensorObj X Y).snd.β U = CategoryTheory.MonoidalCategory.associator X.fst Y.fst U ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫ (CategoryTheory.MonoidalCategory.associator X.fst U Y.fst).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫ CategoryTheory.MonoidalCategory.associator U X.fst Y.fst

@[simp]

theorem CategoryTheory.Center.whiskerLeft_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) {Y₁ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : Y₁ ⟶ Y₂) : (CategoryTheory.MonoidalCategory.whiskerLeft X f).f = CategoryTheory.MonoidalCategory.whiskerLeft X.fst f.f

@[simp]

theorem CategoryTheory.Center.whiskerRight_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} (f : X₁ ⟶ X₂) (Y : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.whiskerRight f Y).f = CategoryTheory.MonoidalCategory.whiskerRight f.f Y.fst

@[simp]

theorem CategoryTheory.Center.tensor_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X₁ : CategoryTheory.Center C} {Y₁ : CategoryTheory.Center C} {X₂ : CategoryTheory.Center C} {Y₂ : CategoryTheory.Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (CategoryTheory.MonoidalCategory.tensorHom f g).f = CategoryTheory.MonoidalCategory.tensorHom f.f g.f

@[simp]

theorem CategoryTheory.Center.tensorUnit_β {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (U : C) : (𝟙_ (CategoryTheory.Center C)).snd.β U = CategoryTheory.MonoidalCategory.leftUnitor U ≪≫ (CategoryTheory.MonoidalCategory.rightUnitor U).symm

@[simp]

theorem CategoryTheory.Center.associator_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) (Z : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom.f = (CategoryTheory.MonoidalCategory.associator X.fst Y.fst Z.fst).hom

@[simp]

theorem CategoryTheory.Center.associator_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) (Z : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv.f = (CategoryTheory.MonoidalCategory.associator X.fst Y.fst Z.fst).inv

@[simp]

theorem CategoryTheory.Center.leftUnitor_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom.f = (CategoryTheory.MonoidalCategory.leftUnitor X.fst).hom

@[simp]

theorem CategoryTheory.Center.leftUnitor_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv.f = (CategoryTheory.MonoidalCategory.leftUnitor X.fst).inv

@[simp]

theorem CategoryTheory.Center.rightUnitor_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom.f = (CategoryTheory.MonoidalCategory.rightUnitor X.fst).hom

@[simp]

theorem CategoryTheory.Center.rightUnitor_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv.f = (CategoryTheory.MonoidalCategory.rightUnitor X.fst).inv

def CategoryTheory.Center.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.MonoidalFunctor (CategoryTheory.Center C) C

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Center.forget_toLaxMonoidalFunctor_toFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) : (CategoryTheory.Center.forget C).obj X = X.fst

@[simp]

theorem CategoryTheory.Center.forget_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Center.forget C).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.Center.forget_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : (CategoryTheory.Center.forget C).μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.fst Y.fst)

@[simp]

theorem CategoryTheory.Center.forget_toLaxMonoidalFunctor_toFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : ∀ {X Y : CategoryTheory.Center C} (f : X ⟶ Y), (CategoryTheory.Center.forget C).map f = f.f

instance CategoryTheory.Center.instReflectsIsomorphismsForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : (CategoryTheory.Center.forget C).ReflectsIsomorphisms

Equations

• ⋯ = ⋯

def CategoryTheory.Center.braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X

Auxiliary definition for the BraidedCategory instance on Center C.

Equations

• X.braiding Y = CategoryTheory.Center.isoMk { f := (X.snd.β Y.fst).hom, comm := ⋯ }

@[simp]

theorem CategoryTheory.Center.braiding_hom_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : (X.braiding Y).hom.f = (X.snd.β Y.fst).hom

@[simp]

theorem CategoryTheory.Center.braiding_inv_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (X : CategoryTheory.Center C) (Y : CategoryTheory.Center C) : (X.braiding Y).inv.f = (X.snd.β Y.fst).inv

instance CategoryTheory.Center.braidedCategoryCenter {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : CategoryTheory.BraidedCategory (CategoryTheory.Center C)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Center.ofBraidedObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.Center C

Auxiliary construction for ofBraided.

Equations

• CategoryTheory.Center.ofBraidedObj X = ⟨X, { β := fun (Y : C) => β_ X Y, monoidal := ⋯, naturality := ⋯ }⟩

@[simp]

theorem CategoryTheory.Center.ofBraidedObj_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : (CategoryTheory.Center.ofBraidedObj X).fst = X

@[simp]

theorem CategoryTheory.Center.ofBraidedObj_snd_β {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) : (CategoryTheory.Center.ofBraidedObj X).snd.β Y = β_ X Y

def CategoryTheory.Center.ofBraided (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalFunctor C (CategoryTheory.Center C)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Center.ofBraided_toLaxMonoidalFunctor_toFunctor_map_f (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Center.ofBraided C).map f).f = f

@[simp]

theorem CategoryTheory.Center.ofBraided_toLaxMonoidalFunctor_ε_f (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.Center.ofBraided C).ε.f = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Center C)).fst

@[simp]

theorem CategoryTheory.Center.ofBraided_toLaxMonoidalFunctor_toFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : (CategoryTheory.Center.ofBraided C).obj X = CategoryTheory.Center.ofBraidedObj X

@[simp]

theorem CategoryTheory.Center.ofBraided_toLaxMonoidalFunctor_μ_f (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) : ((CategoryTheory.Center.ofBraided C).μ X Y).f = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ({ obj := CategoryTheory.Center.ofBraidedObj, map := fun {X Y : C} (f : X ⟶ Y) => { f := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj X) ({ obj := CategoryTheory.Center.ofBraidedObj, map := fun {X Y : C} (f : X ⟶ Y) => { f := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }.obj Y)).fst