Documentation

Mathlib.CategoryTheory.Monoidal.Center

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.

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

    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
    Instances For
      theorem CategoryTheory.Center.Hom.ext_iff {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 = y x.f = y.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.fx = y

      A morphism in the Drinfeld center of C.

      Instances For
        Equations
        • CategoryTheory.Center.instQuiver = { Hom := CategoryTheory.Center.Hom }

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

        Equations
        Instances For

          Auxiliary definition for the MonoidalCategory instance on Center C.

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

            Auxiliary definition for the MonoidalCategory instance on Center C.

            Equations
            Instances For

              Auxiliary definition for the MonoidalCategory instance on Center C.

              Equations
              Instances For
                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
                Instances For
                  @[simp]
                  theorem CategoryTheory.Center.tensorUnit_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] :
                  CategoryTheory.Center.tensorUnit.fst = 𝟙_ C

                  Auxiliary definition for the MonoidalCategory instance on Center C.

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

                    Auxiliary definition for the MonoidalCategory instance on Center C.

                    Equations
                    Instances For

                      Auxiliary definition for the MonoidalCategory instance on Center C.

                      Equations
                      Instances For

                        Auxiliary definition for the MonoidalCategory instance on Center C.

                        Equations
                        Instances For

                          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.
                          Instances For

                            Auxiliary definition for the BraidedCategory instance on Center C.

                            Equations
                            Instances For

                              Auxiliary construction for ofBraided.

                              Equations
                              Instances For
                                @[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

                                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.
                                Instances For