ncatlab.org

homotopy pullback in nLab

Contents

Context

(∞,1)(\infty,1)-Limits and colimits

limits and colimits

1-Categorical

2-Categorical

(∞,1)-Categorical

Model-categorical

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…

models: topological, simplicial, localic, …

see also algebraic topology

Introductions

Definitions

Paths and cylinders

Homotopy groups

Basic facts

Theorems

Model category theory

model category, model ∞ \infty -category

Definitions

Morphisms

Universal constructions

Refinements

Producing new model structures

Presentation of (∞,1)(\infty,1)-categories

Model structures

for ∞\infty-groupoids

for ∞-groupoids

for equivariant ∞\infty-groupoids

for rational ∞\infty-groupoids

for rational equivariant ∞\infty-groupoids

for nn-groupoids

for ∞\infty-groups

for ∞\infty-algebras

general ∞\infty-algebras

specific ∞\infty-algebras

for stable/spectrum objects

for (∞,1)(\infty,1)-categories

for stable (∞,1)(\infty,1)-categories

for (∞,1)(\infty,1)-operads

for (n,r)(n,r)-categories

for (∞,1)(\infty,1)-sheaves / ∞\infty-stacks

Contents

Idea

A homotopy pullback is a special kind of homotopy limit: the appropriate notion of pullback in the context of homotopy theory. Homotopy pullbacks model the quasi-category pullbacks in the (infinity,1)-category that is presented by a given homotopical category. Since pullbacks are also called fiber products, homotopy pullbacks are also called homotopy fiber products.

The notion of homotopy pushout is the dual concept.

For more details see homotopy limit.

In the context of homotopy type theory a homotopy pullback is the interpretation of the space of solutions to an equation.

Definition

In category theory

As with all homotopy limits, there is both a local and a global notion of homotopy pullback.

The global definition says that the homotopy pullback of a cospan X→Z←YX \to Z \leftarrow Y in a category with weak equivalences CC is its image under the right derived functor of the base change functor pb:C →←→Cpb: C^{\to \leftarrow} \to C.

The local definition says that the homotopy pullback of X→Z←YX \to Z \leftarrow Y in a category with a notion of homotopy consists of a square

P → Y ↓ ↓ X → Z \array{ P & \to& Y \\ \downarrow && \downarrow \\ X &\to& Z }

that commutes up to homotopy, and such that for any other square

T → Y ↓ ↓ X → Z \array{ T & \to& Y \\ \downarrow && \downarrow \\ X &\to& Z }

that commutes up to homotopy, there exists a morphism T→PT\to P, unique up to homotopy, making the two triangles commute up to homotopy, and similarly for homotopies and higher homotopies. In other words, there is an equivalence

Map(T,P)≃HoSq(T,X→Z←Y)Map(T,P) \simeq HoSq(T,X\to Z\leftarrow Y)

between the space of maps T→PT\to P and the space of homotopy commutative squares with vertex TT.

In good situations, such as when X,Y,ZX,Y,Z are fibrant in a model category, the two constructions agree up to weak equivalence.

Note that in both cases, there is a canonical map from the actual pullback X× ZYX\times_Z Y to the homotopy pullback X× Z hYX\times_Z^h Y. In the global case this comes by the definition of a derived functor; in the local case it comes because a commutative square is, in particular, a homotopy commutative one.

In homotopy type theory

In homotopy type theory the homotopy pullback of a term of function type

f:A→C f : A \to C

along a term of function type

g:B→C g : B \to C

is given formally by precisely the same formula that would also define the ordinary fiber product of functions of sets, namely by

{a:A,b:B|f(a)=g(b)}. \left\{ a : A, b : B \;\; | \;\; f(a) = g(b) \right\} \,.

Spelled out, this is the dependent sum

∑a:A b:B(f(a)=g(b)) \underset{ \array{ {a \colon A} \\ {b\colon B} } }{\sum} \big( f(a) = g(b) \big)

over the dependent identity type over the evaluation of ff and gg.

What in classical logic is interpreted as the set of pairs (a,b)(a,b) such that f(a)f(a) and g(b)g(b) are equal here becomes the restriction of a mapping cocylinder.

Formal proof that this is the homotopy pullback in homotopy type theory is in (Brunerie). Proof in the categorical semantics of homotopy type theory is below.

Concrete constructions

We discuss various concrete constructions by ordinary pullbacks and ordinary limits such that under some sufficient conditions these compute homotopy pullbacks, up to weak equivalence.

General

Proposition

Let A→C←BA \to C \leftarrow B be a diagram in some model category. Then sufficient conditions for the ordinary (1-categorical) pullback A× CBA \times_C B to present the homotopy pullback of the diagram are

Both statements are classical. They are reviewed for instance as Lurie, prop. A.2.4.4. The proof of the second statement is spelled out here.

Due to prop. one typically computes homotopy pullbacks of a diagram by first forming a resolution of one of the two morphisms by a fibration and then forming an ordinary pullback.

Corollary

If in A→fC←gBA \stackrel{f}{\to} C \stackrel{g}{\leftarrow} B all three objects are fibrant objects, then the homotopy pullback of this diagram is presented by the ordinary pullback

A× C hB → C I× CB ↓ ↓ A →f C. \array{ A\times_C^h B & \to & C^I \times_C B \\ \downarrow && \downarrow \\ A & \stackrel{f}{\to} & C } \,.

or, equivalently up to isomorphism, as the ordinary pullback

A× C hB → C I ↓ ↓ A×B →(f,g) C×C. \array{ A\times_C^h B & \to & C^I \\ \downarrow && \downarrow \\ A\times B & \stackrel{(f,g)}{\to} & C\times C } \,.

See also at Mayer-Vietoris sequence (this proposition) and at homotopy equalizer (this section).

Proof

Since the objects are already fibrant, prop. implies that it is sufficient to replace one of the morphisms by a fibrant resolution. Such a resolution is provided by the factorization lemma: by Lemma 3, B→CB \to C admits a canonical fibrant resolution

C I× CB↠C C^I \times_C B \twoheadrightarrow C

where C→≃C I→C×CC \stackrel{\simeq}{\to} C^I \to C \times C is a path space object for CC (for instance, when CC is a closed monoidal homotopical category then this can be taken to be the internal hom with an interval object II).

The homotopy pullback constructed in this way is an example of a strict homotopy limit, as mentioned at homotopy limit. In such a case, one can say that an arbitrary homotopy-commutative square

W → Y ↓ ↓ X → Z \array{ W & \to& Y \\ \downarrow && \downarrow \\ X &\to& Z }

is a homotopy pullback square if the induced morphism from WW to the strict homotopy pullback is a weak equivalence.

A useful class of examples of this is implied by the following:

Proof

The global projective model structure on simplicial presheaves is right proper. So by prop. the ordinary pullback in question presents the homotopy pullback in the global structure. By the discussion at homotopy limit and Bousfield localization of model categories, this presents the (∞,1)-pullback of the diagram of (∞,1)-presheaves, and the fibrant replacement of that pullback in the local model structure presents the (∞,1)-sheafification of this (∞,1)-presheaf. This is (essentially by definition, see (∞,1)-topos) a left exact (∞,1)-functor and hence preserves finite (∞,1)-limits.

In homotopy type theory

If we unwind the categorical semantics of the above definition

A× C hB≃{a:A,b:B|(f(a)=g(b))} A \times_C^h B \;\simeq\; \Big\{ a \colon A ,\, b \colon B \;\big\vert\; \big( f(a) = g(b) \big) \Big\}

of the homotopy pullback in homotopy type theory, we re-obtain the above prescription for how to construct homotopy pullbacks.

So let the ambient category be a suitable type-theoretic model category.

Example

The type a:A,b:B⊢(f(a)=g(b)) a : A, b : B \vdash (f(a) = g(b)) is obtained by substitution from the identity type of CC. By the discussion there, the categorical semantics of substitution is given by pullback of the fibrations that interpret the dependent types, and so this is interpreted as the pullback [a:A,b:B⊢(f(a)=g(b))]≔(f,g) *C I[a : A, b : B \vdash (f(a) = g(b))] \coloneqq (f,g)^* C^I of the path space object of CC:

[a:A,b:B⊢(f(a)=g(b))] → [IdC] ↓ ↓ [a:A,b:B] →(f,g) [c 1:C,c 2:C]=(f,g) *C I → C I ↓ ↓ A×B →(f,g) C×C. \array{ [a : A, b : B \vdash (f(a) = g(b))] &\to& [Id C] \\ \downarrow && \downarrow \\ [a : A , b : B] &\stackrel{(f,g)}{\to}& [c_1 : C , c_2 : C] } \;\; = \;\; \array{ (f,g)^* C^I &\to& C^I \\ \downarrow && \downarrow \\ A \times B & \stackrel{(f,g)}{\to} & C \times C } \,.

Forming the dependent sum over a:A,b:Ba : A, b : B is simply interpreted as regarding the resulting object (f,g) *C I(f,g)^* C^I as an object in 𝒞≃𝒞 /*\mathcal{C} \simeq \mathcal{C}_{/*} instead of as an object in the slice category 𝒞 /A×B\mathcal{C}_{/ A \times B}.

Since by assumption on the categorical interpretation of a type, all objects here are fibrant, this coincides with the expression of the homotopy pullback from corollary above.

Example

Specifically, let f:A⟶Bf \colon A \longrightarrow B be a function, then the categorical semantics for the expression

∑b:Bfib(f,b)=∑b:B∑a:A(f(a)=b) \underset{b \colon B}{\sum} fib(f,b) = \underset{b \colon B}{\sum} \underset{a \colon A}{\sum} (f(a) = b)

is the canonical fibration replacement of ff as it appears notably in the factorization lemma

A× BB I ⟶ B I ↓ ↓ A×B ⟶(f,Id) B×B. \array{ A \times_B B^I &\longrightarrow& B^I \\ \downarrow && \downarrow \\ A \times B &\stackrel{(f, Id)}{\longrightarrow}& B \times B } \,.

Properties

Fiber-wise characterization

Proposition

In plain homotopy types (i.e. in ∞-groupoids, in the classical model structure on simplicial sets etc.) the following holds:

a diagram

A ⟶f B ↓ ↓ p C ⟶g D \array{ A &\stackrel{f}{\longrightarrow}& B \\ \downarrow && \downarrow^{\mathrlap{p}} \\ C &\stackrel{g}{\longrightarrow}& D }

is a homotopy pullback diagram precisely if it induces a weak equivalence on all homotopy fibers

hfib b(f) ⟶ A ⟶f B ↓ ≃ ↓ ↓ p hfib p(b)(g) ⟶ C ⟶g D \array{ hfib_b(f) &\longrightarrow& A &\stackrel{f}{\longrightarrow}& B \\ \downarrow^{\mathrlap{\simeq}} && \downarrow && \downarrow^{\mathrlap{p}} \\ hfib_{p(b)}(g) &\longrightarrow& C &\stackrel{g}{\longrightarrow}& D }

for all elements b∈Bb \in B.

(e.g. CPS 05, 5.2, MO)

On the other hand in stable homotopy theory the statement holds generally:

Proposition

For 𝒞\mathcal{C} a stable model category, then for a diagram

A ⟶f B ↓ ↓ p C ⟶g D \array{ A &\stackrel{f}{\longrightarrow}& B \\ \downarrow && \downarrow^{\mathrlap{p}} \\ C &\stackrel{g}{\longrightarrow}& D }

the following are equivalent

  1. the square is a homotopy pullback square;

  2. the square is a homotopy pushout squre;

  3. the induced morphism on the homotopy fiber over the zero object 0 is a weak equivalence

    hfib 0(f)⟶≃hfib 0(g). hfib_0(f) \stackrel{\simeq}{\longrightarrow} hfib_0(g) \,.

A proof in terms of stable model categories including the third item is spelled out for instance in (Hovey 07, remark 7.1.12). (Beware: this is not in the original volume from 1999, but is in the version “reprinted with corrections” from 2007.) A proof in terms of stable (∞,1)-categories is in (Lurie HA, prop. 1.1.3.4 (2) lemma 1.2.4.14).

Pasting law

Examples

Fiber sequences

Of particular interest are consecutive homotopy pullbacks of point inclusions. These give rise to fiber sequences and loop space objects.

References

General

See also the references at homotopy limit .

Homotopy pullbacks are at least mentioned in almost any textbook on homotopy theory.

Dedicated textbook introductions:

Exposition in model category-theory:

Fairly comprehensive general resources:

See also:

In terms of homotopy type theory

Discussion of homotopy pullbacks in homotopy type theory:

Last revised on January 18, 2023 at 14:28:18. See the history of this page for a list of all contributions to it.