product-absolute pullback

In category with finite products, the following squares must be pullbacks, for any morphisms $f,g$:

$\array{
X & \xrightarrow{(1, f)} & X \times Y \\
\mathllap{f} \downarrow & (A) & \downarrow \mathrlap{f \times Y} \\
Y & \xrightarrow{d} & Y \times Y
}
\qquad \qquad \qquad
\array{
X & \xrightarrow{1} & X \\
\mathllap{1} \downarrow & (B) & \downarrow \mathrlap{d} \\
X & \xrightarrow{d} & X \times X
}
\qquad \qquad \qquad
\array{
X \times X' & \xrightarrow{1 \times g} & X \times Y' \\
\mathllap{f \times 1} \downarrow & (C) & \downarrow \mathrlap{f \times 1} \\
Y \times X' & \xrightarrow{1 \times g} & Y \times Y'
}$

as must the naturality square for the symmetry $\sigma \colon X \times Y \cong Y \times X$, the product on one side or the other with an identity morphism of a pullback square (which we will call **type D**), and the pasting of two pullback squares side by side. These pullbacks must be preserved by any product-preserving functor, so we call them **product-absolute**.

This fact was already noted for squares of types A and C by Lawvere; the others are given by Seely. See also Todd Trimble’s exposition, noting in particular that the squares expressing coassociativity of diagonal maps $d \colon X \to X \times X$ are product-absolute pullbacks, which we call **type E**.

Last revised on December 8, 2015 at 12:41:17. See the history of this page for a list of all contributions to it.