equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
In the category Set a ‘pullback’ is a subset of the cartesian product of two sets. Given a diagram of sets and functions like this:
the ‘pullback’ of this diagram is the subset $X \subseteq A \times B$ consisting of pairs $(a,b)$ such that the equation $f(a) = g(b)$ holds.
A pullback is therefore the categorical semantics of an equation.
This construction comes up, for example, when $A$ and $B$ are fiber bundles over $C$: then $X$ as defined above is the product of $A$ and $B$ in the category of fiber bundles over $C$. For this reason, a pullback is sometimes called a fibered product (or fiber product or fibre product).
In this case, the fiber of $A \times_C B$ over a (generalized) element $x$ of $C$ is the ordinary product of the fibers of $A$ and $B$ over $x$. In other words, the fiber product is the product taken fiber-wise. Of course, the fiber of $A$ at the generalized element $x\colon I \to C$ is itself a fibre product $I \times_C A$; the terminology depends on your point of view.
Note that there are maps $p_A\colon X \to A$, $p_B\colon X \to B$ sending any $(a,b) \in X$ to $a$ and $b$, respectively. These maps make this square commute:
In fact, the pullback is the universal solution to finding a commutative square like this. In other words, given any commutative square
there is a unique function $h\colon Y \to X$ such that
and
Since this universal property expresses the concept of pullback purely arrow-theoretically, we can formulate it in any category. It is, in fact, a simple special case of a limit.
A pullback is a limit of a diagram like this:
Such a diagram is also called a pullback diagram or a cospan. If the limit exists, we obtain a commutative square
and the object $x$ is also called the pullback. It is well defined up to unique isomorphism. It has the universal property already described above in the special case of the category $Set$.
The last commutative square above is called a pullback square.
The concept of pullback is dual to the concept of pushout: that is, a pullback in $C$ is the same as a pushout in the opposite category $C^{op}$.
Let $\mathcal{C}$ be a category, with $f\colon a\to c$ and $g\colon b\to c$ coterminal arrows in $\mathcal{C}$ as below
A pullback of $f$ and $g$ consists of an object $x$ together with arrows $p_a\colon x\to a$ and $p_b\colon x\to b$ such that the following diagram commutes universally
This means that for any other object $x'$ with arrows $p'_a\colon x'\to a$ and $p'_b\colon x'\to b$ such that
commutes, there exists a unique arrow $u\colon x'\to x$ such that
commutes.
In type theory a pullback $P$ in
is given by the dependent sum over the dependent equality type
(pullbacks as equalizers)
If products exist in $C$, then the pullback
is equivalently the equalizer
of the two morphisms induced by $f$ and $g$ out of the product of $a$ with $b$.
As a consequence of the above, any category with binary products and equalizers has pullbacks. Conversely any category with binary products and pullbacks has equalizers: the equalizer of $f,g:A \to B$ is the pullback of $(1,f) \maps A \to A \times B$ and $(1,g) \maps A \to A \times B$.
(pullbacks preserve monomorphisms and isomorphisms)
Pullbacks preserve monomorphisms and isomorphisms:
If
is a pullback square in some category then:
if $g$ is a monomorphism then $f^\ast g$ is a monomorphism;
if $g$ is an isomorphism then $f^\ast g$ is an isomorphism.
On the other hand that $f^\ast g$ is a monomorphism does not imply that $g$ is a monomorphism.
In any category consider a diagram of the form
There are three commuting squares: the two inner ones and the outer one.
Suppose the right-hand inner square is a pullback, then:
The square on the left is a pullback if and only if the outer square is.
Pasting a morphism $x \to a$ with the outer square gives rise to a commuting square over the (composite) bottom and right edges of the diagram. The square over the cospan in the left-hand inner square arising from $x \to a$ includes a morphism into $b$, which if $b$ is a pullback induces the same commuting square over $d \to e \to f$ and $c \to d$. So one square is universal iff the other is.
The converse implication does not hold: it may happen that the outer and the left square are pullbacks, but not the right square.
For instance let $i\colon a \to b$ be a split monomorphism with retract $p\colon b \to a$ and consider
Then the left square and the outer rectangle are pullbacks but the right square cannot be a pullback unless $i$ was already an isomorphism.
On the other hand, in the (∞,1)-category of ∞-groupoids, there is a sort of “partial converse”; see homotopy pullback#HomotopyFiberCharacterization.
The saturation of the class of pullbacks is the class of limits over categories $C$ whose groupoid reflection $\Pi_1(C)$ is trivial and such that $C$ is L-finite.
If $f\colon X \to Y$ is a morphism in a category $C$ with pullbacks, there is an induced pullback functor $f^*\colon C/Y \to C/X$, sometimes also called base change.
Notions of pullback:
pullback, fiber product (limit over a cospan)
lax pullback, comma object (lax limit over a cospan)
(∞,1)-pullback, homotopy pullback, ((∞,1)-limit over a cospan)
Early use of the terminology “pullback”:
Textbook accounts:
Saunders MacLane, p. 71 in: Categories for the Working Mathematician, Springer (1971) [doi:10.1007/978-1-4757-4721-8]
Francis Borceux, Section 2.5 in Vol. 1: Basic Category Theory of: Handbook of Categorical Algebra, Encyclopedia of Mathematics and its Applications 50 Cambridge University Press (1994) (doi:10.1017/CBO9780511525858)
See also:
In view of more general finite limits and L-finite limits:
Morphisms admitting pullbacks along them are called carrable in some places, for instance, the following:
Last revised on August 22, 2024 at 13:55:30. See the history of this page for a list of all contributions to it.