Documentation

Mathlib.CategoryTheory.Closed.Monoidal

Closed monoidal categories #

Define (right) closed objects and (right) closed monoidal categories.

TODO #

Some of the theorems proved about cartesian closed categories should be generalised and moved to this file.

An object X is (right) closed if (X ⊗ -) is a left adjoint.

Instances

    A monoidal category C is (right) monoidal closed if every object is (right) closed.

    Instances

      If X and Y are closed then X ⊗ Y is. This isn't an instance because it's not usually how we want to construct internal homs, we'll usually prove all objects are closed uniformly.

      Equations
      Instances For

        The unit object is always closed. This isn't an instance because most of the time we'll prove closedness for all objects at once, rather than just for this one.

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

          The adjunction between A ⊗ - and A ⟹ -.

          Equations
          Instances For

            A ⟶[C] B denotes the internal hom from A to B

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

              Currying in a monoidal closed category.

              Equations
              Instances For

                Uncurrying in a monoidal closed category.

                Equations
                Instances For

                  Pre-compose an internal hom with an external hom.

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

                    The internal hom functor given by the monoidal closed structure.

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

                      Transport the property of being monoidal closed across a monoidal equivalence of categories

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

                        Suppose we have a monoidal equivalence F : C ≌ D, with D monoidal closed. We can pull the monoidal closed instance back along the equivalence. For X, Y, Z : C, this lemma describes the resulting currying map Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z)). (X ⟶[C] Z is defined to be F⁻¹(F(X) ⟶[D] F(Z)), so currying in C is given by essentially conjugating currying in D by F.)

                        Suppose we have a monoidal equivalence F : C ≌ D, with D monoidal closed. We can pull the monoidal closed instance back along the equivalence. For X, Y, Z : C, this lemma describes the resulting uncurrying map Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z). (X ⟶[C] Z is defined to be F⁻¹(F(X) ⟶[D] F(Z)), so uncurrying in C is given by essentially conjugating uncurrying in D by F.)