8.7 The van Kampen theorem
The van Kampen theorem calculates the fundamental group of a (homotopy) pushout of spaces. It is traditionally stated for a topological space which is the union of two open subspaces and , but in homotopy-theoretic terms this is just a convenient way of ensuring that is the pushout of and over their intersection. Thus, we will prove a version of the van Kampen theorem for arbitrary pushouts.
In this section we will describe a proof of the van Kampen theorem which uses the same encode-decode method that we used for in \autorefsec:pi1-s1-intro. There is also a more homotopy-theoretic approach; see \autorefex:rezk-vankampen.
We need a more refined version of the encode-decode method. In \autorefsec:pi1-s1-intro (as well as in \autorefsec:compute-coprod,\autorefsec:compute-nat) we used it to characterize the path space of a (higher) inductive type — deriving as a consequence a characterization of the loop space , and thereby also of its 0-truncation . In the van Kampen theorem, our goal is only to characterize the fundamental group , and we do not have any explicit description of the loop spaces or the path spaces to use.
It turns out that we can use the same technique directly for a truncated version of the path fibration, thereby characterizing not only the fundamental group , but also the whole fundamental groupoid. Specifically, for a type , write for the -truncation of its identity type, i.e. . Note that we have induced groupoid operations
for which we use the same notation as the corresponding operations on paths.
|Title||8.7 The van Kampen theorem|