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 $𝐴, 𝐵 \in 𝖢$ there exist natural transformations

p r 𝐵 1 : 1 \otimes 𝐵 \Rightarrow 1 : 𝖢 \to 𝖢 p r 𝐴 2 : 𝐴 \otimes 1 \Rightarrow 1 : 𝖢 \to 𝖢

so that for any $𝐴, 𝐵 \in 𝖢$ the data $(𝐴 \otimes 𝐵, p r 𝐵 1, 𝐴, p r 𝐴 2, 𝐵)$ satisfy the universal property of the product.

From finitary product category

Suppose $𝖢$ has (chosen¹) finite products: That is, a terminal object $1 \in 𝖢$ , and for every pair of objects $𝐴, 𝐵 \in 𝖢$ a binary product $𝐴 \times 𝐵$ . Then $(\times)$ extends to a tensor product with unit $1$ so that $𝖢$ is a cartesian category. The naturality of $p r 𝑖$ fully determines the action on morphisms:

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

which explicitly gives

𝛼 𝑋 𝑌 𝑍 = ⟨ p r 1 p r 1, ⟨ p r 2 p r 1, p r 2 ⟩ ⟩ 𝛼 - 1 𝑋 𝑌 𝑍 = ⟨ ⟨ p r 1, p r 1, p r 2 ⟩, p r 2 p r 2 ⟩ .

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

𝜆 𝑋 = p r 2, 𝜌 𝑋 = p r 3

Their inverses are shown by

to be

𝜆 - 1 𝑋 = ⟨! 𝑋, 𝑋 ⟩, 𝜌 - 1 𝑋 = ⟨ 𝑋,! 𝑋 ⟩

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).

Cartesian category

From finitary product category

See also

Footnotes