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
- CategoryTheory.monoidalOfHasFiniteProducts C = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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
- CategoryTheory.monoidalOfHasFiniteCoproducts C = CategoryTheory.MonoidalCategory.ofTensorHom ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
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.