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.

Implementation #

We had previously chosen to rely on HasTerminal and HasBinaryProducts instead of HasBinaryProducts, because we were later relying on the definitional form of the tensor product. Now that has_limit has been refactored to be a Prop, this issue is irrelevant and we could simplify the construction here.

See CategoryTheory.monoidalOfChosenFiniteProducts for a variant of this construction which allows specifying a particular choice of terminal object and binary products.

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