Category theory MOC

Cartesian category

A cartesian category is a (necessarily symmetric) monoidal category whose tensor product is a categorical product and whose tensor unit is a terminal object. #m/def/cat Specifically, for any there exist natural transformations

so that for any the data satisfy the universal property of the product.

From finitary product category

Suppose has (chosen1) finite products: That is, a terminal object , and for every pair of objects a binary product . Then extends to a tensor product with unit so that is a cartesian category. The naturality of fully determines the action on morphisms:

c

Deriving the associator and unitors is routine, if a little hairy. Deriving the coherence conditions is outright herculean.

Proof

The associator and its inverse are given by the diagonal morphisms in

c|https://q.uiver.app/#q=WzAsNyxbMCwwLCIoWCBcXHRpbWVzIFkpIFxcdGltZXMgWiJdLFswLDIsIlggXFx0aW1lcyBZIl0sWzAsNCwiWCJdLFs0LDAsIloiXSxbMiwyLCJZIl0sWzQsNCwiWCBcXHRpbWVzIChZIFxcdGltZXMgWikiXSxbNCwyLCJZIFxcdGltZXMgWiJdLFswLDNdLFswLDFdLFsxLDJdLFsxLDRdLFs2LDRdLFs2LDNdLFs1LDJdLFs1LDZdLFswLDYsIiIsMSx7ImN1cnZlIjotMiwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzAsNSwiIiwxLHsiY3VydmUiOi0yLCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNSwwLCIiLDEseyJjdXJ2ZSI6LTIsInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFs1LDEsIiIsMSx7Im9mZnNldCI6LTEsImN1cnZlIjotMiwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV1d&macro_url=https%3A%2F%2Fraw.githubusercontent.com%2Fjajaperson%2FPKM%2Frefs%2Fheads%2Fmain%2Fpreamble.sty

which explicitly gives

The left and right unitors are given by the projections themselves.

Their inverses are shown by

c|https://q.uiver.app/#q=WzAsNixbMiwwLCJYIFxcdGltZXMgMSJdLFsyLDIsIjEiXSxbMCwxLCJYIl0sWzQsMCwiMSBcXHRpbWVzIFgiXSxbNiwxLCJYIl0sWzQsMiwiMSJdLFswLDEsIlxcb3Bue3ByfV8yIl0sWzAsMiwiXFxvcG57cHJ9XzEiLDIseyJjdXJ2ZSI6Mn1dLFsyLDEsIiFfWCIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dLFsyLDAsIlxcbGFuZ2xlIFgsICFfWCBcXHJhbmdsZSIsMix7ImN1cnZlIjoyLCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMyw1LCJcXG9wbntwcn1fMSIsMl0sWzMsNCwiXFxvcG57cHJ9XzIiLDAseyJjdXJ2ZSI6LTJ9XSxbNCw1LCIhX1giLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbNCwzLCJcXGxhbmdsZSAhX1gsIFggXFxyYW5nbGUiLDAseyJjdXJ2ZSI6LTIsInN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&macro_url=https%3A%2F%2Fraw.githubusercontent.com%2Fjajaperson%2FPKM%2Frefs%2Fheads%2Fmain%2Fpreamble.sty

to be

A fully formal proof of the coherence relations are best carried out with a proof assistant with tactics, see the 1Lab. For now we note that the above morphisms were constructed as the unique solutions to universal mapping problems, and that we can do analogous constructions for iterate products, which will then commute (again by uniqueness).

See also

#state/tidy | #lang/en | #SemBr

Footnotes

  1. Here we mean we have the actual exhibition of products, not the mere existence. We get this for free from the right Global Axiom of Choice, or the Principle of Unique Choice in a univalent category; otherwise they need to be provided, lest we get an anafunctor from this construction. ↩