nLab pullback

Redirected from "cartesian squares".
Note: cartesian square and pullback both redirect for "cartesian squares".
Contents

Context

Limits and colimits

Equality and Equivalence

Contents

Idea

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 XA×BX \subseteq A \times B consisting of pairs (a,b)(a,b) such that the equation f(a)=g(b)f(a) = g(b) holds.

A pullback is therefore the categorical semantics of an equation.

This construction comes up, for example, when AA and BB are fiber bundles over CC: then XX as defined above is the product of AA and BB in the category of fiber bundles over CC. For this reason, a pullback is sometimes called a fibered product (or fiber product or fibre product).

In this case, the fiber of A× CBA \times_C B over a (generalized) element xx of CC is the ordinary product of the fibers of AA and BB over xx. In other words, the fiber product is the product taken fiber-wise. Of course, the fiber of AA at the generalized element x:ICx\colon I \to C is itself a fibre product I× CAI \times_C A; the terminology depends on your point of view.

Note that there are maps p A:XAp_A\colon X \to A, p B:XBp_B\colon X \to B sending any (a,b)X(a,b) \in X to aa and bb, 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:YXh\colon Y \to X such that

p Ah=q A p_A h = q_A

and

p Bh=q B. p_B h = q_B\,.

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.

Definition

In category theory

As 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 xx 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 SetSet.

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 CC is the same as a pushout in the opposite category C opC^{op}.

Nuts and bolts

Let 𝒞\mathcal{C} be a category, with f:acf\colon a\to c and g:bcg\colon b\to c coterminal arrows in 𝒞\mathcal{C} as below

A pullback of ff and gg consists of an object xx together with arrows p a:xap_a\colon x\to a and p b:xbp_b\colon x\to b such that the following diagram commutes universally

This means that for any other object xx' with arrows p a:xap'_a\colon x'\to a and p b:xbp'_b\colon x'\to b such that

commutes, there exists a unique arrow u:xxu\colon x'\to x such that

commutes.

In type theory

In type theory a pullback PP in

is given by the dependent sum over the dependent equality type

P= a:A b:B(f(a)=g(b)). P = \sum_{a\colon A} \sum_{b\colon B} (f(a) = g(b)) \,.

Properties

Proposition

(pullbacks as equalizers)

If products exist in CC, then the pullback

is equivalently the equalizer

of the two morphisms induced by ff and gg out of the product of aa with bb.

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:ABf,g:A \to B is the pullback of (1,f)mapsAA×B(1,f) \maps A \to A \times B and (1,g)mapsAA×B(1,g) \maps A \to A \times B.

Proposition

(pullbacks preserve monomorphisms and isomorphisms)

Pullbacks preserve monomorphisms and isomorphisms:

If

is a pullback square in some category then:

  1. if gg is a monomorphism then f *gf^\ast g is a monomorphism;

  2. if gg is an isomorphism then f *gf^\ast g is an isomorphism.

On the other hand that f *gf^\ast g is a monomorphism does not imply that gg is a monomorphism.

Proposition

(pasting law for pullbacks)

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.

Proof

Pasting a morphism xax \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 xax \to a includes a morphism into bb, which if bb is a pullback induces the same commuting square over defd \to e \to f and cdc \to d. So one square is universal iff the other is.

Proposition

The converse implication does not hold: it may happen that the outer and the left square are pullbacks, but not the right square.

Proof

For instance let i:abi\colon a \to b be a split monomorphism with retract p:bap\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 ii was already an isomorphism.

Remark

On the other hand, in the (∞,1)-category of ∞-groupoids, there is a sort of “partial converse”; see homotopy pullback#HomotopyFiberCharacterization.

Saturation

The saturation of the class of pullbacks is the class of limits over categories CC whose groupoid reflection Π 1(C)\Pi_1(C) is trivial and such that CC is L-finite.

Pullback functor

If f:XYf\colon X \to Y is a morphism in a category CC with pullbacks, there is an induced pullback functor f *:C/YC/Xf^*\colon C/Y \to C/X, sometimes also called base change.

Notions of pullback:

References

Early use of the terminology “pullback”:

Textbook accounts:

See also:

In view of more general finite limits and L-finite limits:

  • Robert Paré, Simply connected limits. Can. J. Math., Vol. XLH, No. 4, 1990, pp. 731-746, CMS

Morphisms admitting pullbacks along them are called carrable in some places, for instance, the following:

They are called quarrable in:

Last revised on September 27, 2024 at 15:06:20. See the history of this page for a list of all contributions to it.