Documentation

Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts

The natural monoidal structure on any category with finite (co)products. #

A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category, although this is also sometimes used to mean a finitely complete category. (See https://ncatlab.org/nlab/show/cartesian+category.)

As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.

TODO #

Replace monoidalOfHasFiniteProducts and symmetricOfHasFiniteProducts with CartesianMonoidalCategory.ofHasFiniteProducts.

A category with a terminal object and binary products has a natural monoidal structure.

Equations
Instances For

    The monoidal structure coming from finite products is symmetric.

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

      A category with an initial object and binary coproducts has a natural monoidal structure.

      Equations
      Instances For

        The monoidal structure coming from finite coproducts is symmetric.

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

          Promote a finite products preserving functor to a monoidal functor between categories equipped with the monoidal category structure given by finite products.

          Equations