Finn Lawler product-absolute pullback (Rev #1)

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

\array{ X & \xrightarrow{\langle 1, f \rangle} & X \times Y \\ \mathllap{f} \downarrow & (A) & \downarrow \mathrlap{f \times Y} \\ Y & \xrightarrow{\Delta} & Y \times Y } \qquad \qquad \qquad \array{ X & \xrightarrow{1} & X \\ \mathllap{1} \downarrow & (B) & \downarrow \mathrlap{\Delta} \\ X & \xrightarrow{\Delta} & 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, 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.

Revision on November 22, 2012 at 22:50:11 by Finn Lawler?. See the history of this page for a list of all contributions to it.