Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
An -pullback is a limit in an (∞,1)-category over a diagram of the shape
In other words it is a cone
which is universal among all such cones in the -categorical sense.
This is the analog in (∞,1)-category theory of the notion of pullback in category theory.
Let be a quasi-category. Recall the notion of limit in a quasi-category.
The non-degenerate cells of the simplicial set obtained as the cartesian product of the simplicial 1-simplex with itself look like
A square in a quasi-category is an image of this in , i.e. a morphism
The simplicial square is isomorphic, as a simplicial set, to the join of simplicial sets of a 2-horn with the point:
and
If a square exhibits as a quasi-categorical limit over , we say the limit
is the quasi-categorical pullback of the diagram .
We have the following quasi-categorical analog of the familiar pasting law of pullbacks in ordinary category theory:
A pasting diagram of two squares is a morphism
Schematically this looks like
in .
(pasting law for quasi-categorical pullbacks)
If the right square is a pullback diagram in , then the left square is precisely if the outer square is.
This is HTT, lemma 4.4.2.1
Consider the diagram inclusions
and the induced diagram of over quasi-categories
Notice that by definition of limit in a quasi-category the quasi-categorical pullback is the terminal object in , while is the terminal object in .
The strategy now is to show that both these morphisms and are acyclic Kan fibrations. That will imply that these terminal objects coincide as objects of .
First notice that the inclusion
is a left anodyne morphism, being the composite of pushouts of left horn inclusions
We could also prove this by showing that this functor is homotopy initial using the characterization in terms of slice categories, and then invoking the theorem of HTT 4.1.1.3(4) which says (in dual form) that an inclusion of simplicial sets is homotopy initial if and only if it is left anodyne.
One of the properties of left anodyne morphisms is that restriction of over quasi-categories along left anodyne morphisms produces an acyclic Kan fibration. This shows the desired statement for .
To see that is also an acyclic fibration observe that can be factored as
Observe that fits into a pullback diagram
and hence is an acyclic Kan fibration since is one, on account of the fact that the square
is a pullback in . Finally, is a trivial fibration since
is left anodyne; clearly this is a pushout of and so it suffices to show that is left anodyne. But this map factors as and clearly is left anodyne since it is a pushout of .
If has a terminal object and is a pointed object, then the fiber or -kernel of a morphisms is the -pullback
For more on this see fiber sequence.
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)
A formalization of homotopy pullbacks in homotopy type theory is Coq-coded in
Last revised on December 2, 2020 at 17:34:02. See the history of this page for a list of all contributions to it.