8.7 The van Kampen theorem

The van Kampen theoremMathworldPlanetmath calculates the fundamental groupMathworldPlanetmathPlanetmath Ο€1 of a (homotopyMathworldPlanetmathPlanetmath) pushout of spaces. It is traditionally stated for a topological spaceMathworldPlanetmath X which is the union of two open subspaces U and V, but in homotopy-theoretic terms this is just a convenient way of ensuring that X is the pushout of U and V over their intersectionMathworldPlanetmathPlanetmath. Thus, we will prove a version of the van Kampen theorem for arbitrary pushouts.

In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we will describe a proof of the van Kampen theorem which uses the same encode-decode method that we used for Ο€1⁒(π•Š1) 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 W β€” deriving as a consequence a characterization of the loop spaceMathworldPlanetmath Ω⁒(W), and thereby also of its 0-truncation Ο€1⁒(W). In the van Kampen theorem, our goal is only to characterize the fundamental group Ο€1⁒(W), 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 fibrationMathworldPlanetmath, thereby characterizing not only the fundamental group Ο€1⁒(W), but also the whole fundamental groupoidPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. Specifically, for a type X, write Ξ 1⁒X:Xβ†’X→𝒰 for the 0-truncation of its identity type, i.e.Β Ξ 1X(x,y):≑βˆ₯x=yβˆ₯0. Note that we have induced groupoid operationsMathworldPlanetmath

(–⁒\centerdot⁒–)  :Ξ 1⁒X⁒(x,y)β†’Ξ 1⁒X⁒(y,z)β†’Ξ 1⁒X⁒(x,z)
(–)-1  :Ξ 1⁒X⁒(x,y)β†’Ξ 1⁒X⁒(y,x)
𝗋𝖾𝖿𝗅x  :Ξ 1⁒X⁒(x,x)
𝖺𝗉f  :Ξ 1⁒X⁒(x,y)β†’Ξ 1⁒Y⁒(f⁒x,f⁒y)

for which we use the same notation as the corresponding operations on paths.

Title 8.7 The van Kampen theorem