Documentation

Mathlib.CategoryTheory.Monoidal.Braided.Basic

Braided and symmetric monoidal categories #

The basic definitions of braided monoidal categories, and symmetric monoidal categories, as well as braided functors.

Implementation note #

We make BraidedCategory another typeclass, but then have SymmetricCategory extend this. The rationale is that we are not carrying any additional data, just requiring a property.

Future work #

References #

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

Instances

    The braiding natural isomorphism.

    Equations
    Instances For
      theorem CategoryTheory.BraidedCategory.yang_baxter_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z✝ (CategoryTheory.MonoidalCategory.tensorObj Y X) Z) :

      Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding by a faithful monoidal functor.

      Equations
      Instances For

        Pull back a braiding along a fully faithful monoidal functor.

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

          We now establish how the braiding interacts with the unitors.

          I couldn't find a detailed proof in print, but this is discussed in:

          A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.

          See https://stacks.math.columbia.edu/tag/0FFW.

          Instances

            A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.

            Instances For

              The identity lax braided monoidal functor.

              Equations
              Instances For

                The composition of lax braided monoidal functors.

                Equations
                • F.comp G = let __src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; { toLaxMonoidalFunctor := __src, braided := }
                Instances For

                  Interpret a natural isomorphism of the underlying lax monoidal functors as an isomorphism of the lax braided monoidal functors.

                  Equations
                  Instances For

                    A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.

                    Instances For

                      The identity braided monoidal functor.

                      Equations
                      Instances For

                        Interpret a natural isomorphism of the underlying monoidal functors as an isomorphism of the braided monoidal functors.

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

                          A multiplicative morphism between commutative monoids gives a braided functor between the corresponding discrete braided monoidal categories.

                          Equations
                          Instances For
                            theorem CategoryTheory.tensor_associativity_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) (Z₁ : C) (Z₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ (CategoryTheory.MonoidalCategory.tensorObj Y₁ Z₁)) (CategoryTheory.MonoidalCategory.tensorObj X₂ (CategoryTheory.MonoidalCategory.tensorObj Y₂ Z₂)) Z) :

                            The tensor product functor from C × C to C as a monoidal functor.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem CategoryTheory.associator_monoidal_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (X₃ : C) (Y₁ : C) (Y₂ : C) (Y₃ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)) Z) :
                              @[simp]
                              theorem CategoryTheory.MonoidalOpposite.mop_hom_braiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) :
                              (β_ X Y).hom.mop = (β_ { unmop := Y } { unmop := X }).hom
                              @[simp]
                              theorem CategoryTheory.MonoidalOpposite.mop_inv_braiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) :
                              (β_ X Y).inv.mop = (β_ { unmop := Y } { unmop := X }).inv

                              The identity functor on C, viewed as a functor from C to its monoidal opposite, upgraded to a braided functor.

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

                                The identity functor on C, viewed as a functor from the monoidal opposite of C to C, upgraded to a braided functor.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[reducible, inline]

                                  The braided monoidal category obtained from C by replacing its braiding β_ X Y : X ⊗ Y ≅ Y ⊗ X with the inverse (β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X. This corresponds to the automorphism of the braid group swapping over-crossings and under-crossings.

                                  Equations
                                  • CategoryTheory.reverseBraiding C = { braiding := fun (X Y : C) => (β_ Y X).symm, braiding_naturality_right := , braiding_naturality_left := , hexagon_forward := , hexagon_reverse := }
                                  Instances For

                                    The identity functor from C to C, where the codomain is given the reversed braiding, upgraded to a braided functor.

                                    Equations
                                    Instances For