Product Universal Property

Product universal property: if R maps to both P and Q pointwise, then R maps to P x Q. Also: product is commutative, associative, and unital (with terminal presheaf).

Product Universal Property

Summary

Product universal property: if R maps to both P and Q pointwise, then R maps to P x Q. Also: product is commutative, associative, and unital (with terminal presheaf).

Statement

%
\label{thm:product-universal}
For presheaves $P, Q \in \mathcal{E}_\tau$,
the product $(P \times Q, \pi_1, \pi_2)$
satisfies the universal property:
for any presheaf $R$ and natural transformations
$f : R \to P$ and $g : R \to Q$,
there exists a \emph{unique} natural transformation
\[
    \boxed{%
    \langle f, g \rangle : R \to P \times Q}
\]
such that $\pi_1 \circ \langle f, g \rangle = f$
and $\pi_2 \circ \langle f, g \rangle = g$.

Proof / Justification

\textbf{Existence.}
Define $\langle f, g \rangle_X(r)
:= \bigl(f_X(r),\; g_X(r)\bigr)$
for each $X$ and $r \in R(X)$.
Naturality follows from the naturality of $f$ and $g$:
for $\phi : X \to Y$,
$(P \times Q)(\phi) \circ \langle f, g \rangle_Y
= \langle f, g \rangle_X \circ R(\phi)$.
The projection laws hold by construction.

\textbf{Uniqueness.}
If $h : R \to P \times Q$
satisfies $\pi_1 \circ h = f$
and $\pi_2 \circ h = g$,
then $h_X(r) = (f_X(r),\; g_X(r))
= \langle f, g \rangle_X(r)$.

Source Context

• Registry source: book-01.jsonl line 140
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part15/ch57-cartesian-product.tex lines 116-131

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Topos.CartesianProduct
• Name: Tau.Topos.product_universal

Dependencies

• Canonical: I.D60

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.