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.

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.

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.

    Instances For

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

      Instances For

        Auxiliary definition for the MonoidalCategory instance on Center C.

        Instances For

          Auxiliary definition for the MonoidalCategory instance on Center C.

          Instances For

            Auxiliary definition for the MonoidalCategory instance on Center C.

            Instances For

              Auxiliary definition for the MonoidalCategory instance on Center C.

              Instances For

                Auxiliary definition for the MonoidalCategory instance on Center C.

                Instances For

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

                  Instances For

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

                    Instances For