Categorical Product

The categorical product of two presheaves: pointwise conjunction of support predicates. P x Q maps each object X to P(X) AND Q(X). Projections extract each factor.

Categorical Product

Summary

The categorical product of two presheaves: pointwise conjunction of support predicates. P x Q maps each object X to P(X) AND Q(X). Projections extract each factor.

Statement

%
\label{def:categorical-product}
For presheaves $P, Q \in \mathcal{E}_\tau$,
the \textbf{categorical product}
$P \times Q$ is the presheaf:
\[
    \boxed{%
    (P \times Q)(X)
    \;:=\;
    P(X) \times Q(X)}
\]
for each object $X$ in $\mathrm{Cat}_\tau$.
For each arrow $f : X \to Y$
(a divisibility witness $Y \mid X$),
the restriction map is componentwise:
$(P \times Q)(f)(s, t) = \bigl(P(f)(s),\; Q(f)(t)\bigr)$.
The \textbf{projection morphisms}
$\pi_1 : P \times Q \to P$
and $\pi_2 : P \times Q \to Q$
are $(\pi_1)_X(s, t) := s$
and $(\pi_2)_X(s, t) := t$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: I.D55, I.D57

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.