Documentation

Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Rigid (autonomous) monoidal categories #

This file defines rigid (autonomous) monoidal categories and the necessary theory about exact pairings and duals.

Main definitions #

Main statements #

Notations #

Future work #

Notes #

Although we construct the adjunction tensorLeft Y ⊣ tensorLeft X from ExactPairing X Y, this is not a bijective correspondence. I think the correct statement is that tensorLeft Y and tensorLeft X are module endofunctors of C as a right C module category, and ExactPairing X Y is in bijection with adjunctions compatible with this right C action.

References #

Tags #

rigid category, monoidal category

An exact pairing is a pair of objects X Y : C which admit a coevaluation and evaluation morphism which fulfill two triangle equalities.

Instances

    A class of objects which have a right dual.

    Instances

      A class of objects which have a left dual.

      Instances

        The right adjoint mate fᘁ : Xᘁ ⟶ Yᘁ of a morphism f : X ⟶ Y.

        Instances For

          The left adjoint mate ᘁf : ᘁY ⟶ ᘁX of a morphism f : X ⟶ Y.

          Instances For

            The composition of left adjoint mates is the adjoint mate of the composition.

            Given an exact pairing on Y Y', we get a bijection on hom-sets (Y' ⊗ X ⟶ Z) ≃ (X ⟶ Y ⊗ Z) by "pulling the string on the left" up or down.

            This gives the adjunction tensorLeftAdjunction Y Y' : tensorLeft Y' ⊣ tensorLeft Y.

            This adjunction is often referred to as "Frobenius reciprocity" in the fusion categories / planar algebras / subfactors literature.

            Instances For

              Given an exact pairing on Y Y', we get a bijection on hom-sets (X ⊗ Y ⟶ Z) ≃ (X ⟶ Z ⊗ Y') by "pulling the string on the right" up or down.

              Instances For

                If Y Y' have an exact pairing, then the functor tensorLeft Y' is left adjoint to tensorLeft Y.

                Instances For

                  If Y Y' have an exact pairing, then the functor tensor_right Y is left adjoint to tensor_right Y'.

                  Instances For

                    If Y has a left dual ᘁY, then it is a closed object, with the internal hom functor Y ⟶[C] - given by left tensoring by ᘁY. This has to be a definition rather than an instance to avoid diamonds, for example between category_theory.monoidal_closed.functor_closed and category_theory.monoidal.functor_has_left_dual. Moreover, in concrete applications there is often a more useful definition of the internal hom object than ᘁY ⊗ X, in which case the closed structure shouldn't come from has_left_dual (e.g. in the category FinVect k, it is more convenient to define the internal hom as Y →ₗ[k] X rather than ᘁY ⊗ X even though these are naturally isomorphic).

                    Instances For

                      Transport an exact pairing across an isomorphism in the first argument.

                      Instances For

                        Transport an exact pairing across an isomorphism in the second argument.

                        Instances For

                          Transport an exact pairing across isomorphisms.

                          Instances For

                            Right duals are isomorphic.

                            Instances For

                              Left duals are isomorphic.

                              Instances For

                                A right rigid monoidal category is one in which every object has a right dual.

                                Instances

                                  A left rigid monoidal category is one in which every object has a right dual.

                                  Instances

                                    Any left rigid category is monoidal closed, with the internal hom X ⟶[C] Y = ᘁX ⊗ Y. This has to be a definition rather than an instance to avoid diamonds, for example between category_theory.monoidal_closed.functor_category and category_theory.monoidal.left_rigid_functor_category. Moreover, in concrete applications there is often a more useful definition of the internal hom object than ᘁY ⊗ X, in which case the monoidal closed structure shouldn't come the rigid structure (e.g. in the category FinVect k, it is more convenient to define the internal hom as Y →ₗ[k] X rather than ᘁY ⊗ X even though these are naturally isomorphic).

                                    Instances For

                                        A rigid monoidal category is a monoidal category which is left rigid and right rigid.

                                        Instances