8.7.2 The van Kampen theorem with a set of basepoints

The improvement of van Kampen we present now is closely analogous to a similar improvement in classical algebraic topology, where $A$ is equipped with a set $S$ of base points. In fact, it turns out to be unnecessary for our proof to assume that the “set of basepoints” is a set — it might just as well be an arbitrary type; the utility of assuming $S$ is a set arises later, when applying the theorem to obtain computations. What is important is that $S$ contains at least one point in each connected component of $A$ . We state this in type theory by saying that we have a type $S$ and a function $k:S\to A$ which is surjective, i.e. $(-1)$ -connected. If $S\equiv A$ and $k$ is the identity function, then we will recover the naive van Kampen theorem. Another example to keep in mind is when $A$ is pointed and (0-)connected, with $k:\mathbf{1}\to A$ the point: by \autorefthm:minusoneconn-surjective,\autorefthm:connected-pointed this map is surjective just when $A$ is 0-connected.

Let $A, B, C, f, g, P, i, j, h$ be as in the previous section. We now define, given our surjective map $k:S\to A$ , an auxiliary type which improves the connectedness of $k$ . Let $T$ be the higher inductive type generated by

•

A function $\ell:S\to T$ , and
•

For each $s,s^{\prime}:S$ , a function $m:(ks=_{A}ks^{\prime})\to(\ell s=_{T}\ell s^{\prime})$ .

There is an obvious induced function $\overline{k}:T\to A$ such that $\overline{k}\ell=k$ , and any $p:ks=ks^{\prime}$ is equal to the composite $ks=\overline{k}\ell s\overset{\overline{k}mp}{=}\overline{k}\ell s^{\prime}=ks% ^{\prime}$ .

Lemma 8.7.1.

$\overline{k}$ is 0-connected.

Proof.

We must show that for all $a : A$ , the 0-truncation of the type $\mathchoice{\sum_{t:T}\,}{\mathchoice{{\textstyle\sum_{(t:T)}}}{\sum_{(t:T)}}{% \sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{\textstyle\sum_{(t:T)}}}{\sum_{(t:T)% }}{\sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{\textstyle\sum_{(t:T)}}}{\sum_{(t% :T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}(\overline{k}t=a)$ is contractible. Since contractibility is a mere proposition and $k$ is $(-1)$ -connected, we may assume that $a=ks$ for some $s : S$ . Now we can take the center of contraction to be $\mathopen{}\left|(\ell s,q)\right|_{0}\mathclose{}$ where $q$ is the equality $\overline{k}\ell s=ks$ .

It remains to show that for any $\phi:\mathopen{}\left\|\mathchoice{\sum_{t:T}\,}{\mathchoice{{\textstyle\sum_{% (t:T)}}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{\textstyle% \sum_{(t:T)}}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{% \textstyle\sum_{(t:T)}}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}(\overline{% k}t=ks)\right\|_{0}\mathclose{}$ we have $\phi=\mathopen{}\left|(\ell s,q)\right|_{0}\mathclose{}$ . Since the latter is a mere proposition, and in particular a set, we may assume that $\phi=\mathopen{}\left|(t,p)\right|_{0}\mathclose{}$ for $t : T$ and $p:\overline{k}t=ks$ .

Now we can do induction on $t : T$ . If $t\equiv\ell s^{\prime}$ , then $ks^{\prime}=\overline{k}\ell s^{\prime}\overset{p}{=}ks$ yields via $m$ an equality $\ell s=\ell s^{\prime}$ . Hence by definition of $\overline{k}$ and of equality in homotopy fibers, we obtain an equality $(ks^{\prime},p)=(ks,q)$ , and thus $\mathopen{}\left|(ks^{\prime},p)\right|_{0}\mathclose{}=\mathopen{}\left|(ks,q% )\right|_{0}\mathclose{}$ . Next we must show that as $t$ varies along $m$ these equalities agree. But they are equalities in a set (namely $\mathopen{}\left\|\mathchoice{\sum_{t:T}\,}{\mathchoice{{\textstyle\sum_{(t:T)% }}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{\textstyle\sum_{(t% :T)}}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}{\mathchoice{{\textstyle\sum_% {(t:T)}}}{\sum_{(t:T)}}{\sum_{(t:T)}}{\sum_{(t:T)}}}(\overline{k}t=ks)\right\|% _{0}\mathclose{}$ ), and hence this is automatic. ∎

Remark 8.7.2.

$T$ can be regarded as the (homotopy) coequalizer of the “kernel pair” of $k$ . If $S$ and $A$ were sets, then the $(-1)$ -connectivity of $k$ would imply that $A$ is the $0$ -truncation of this coequalizer (see \autorefcha:set-math). For general types, higher topos theory suggests that $(-1)$ -connectivity of $k$ will imply instead that $A$ is the colimit (a.k.a. “geometric realization”) of the “simplicial kernel” of $k$ . The type $T$ is the colimit of the “1-skeleton” of this simplicial kernel, so it makes sense that it improves the connectivity of $k$ by $1$ . More generally, we might expect the colimit of the $n$ -skeleton to improve connectivity by $n$ .

Now we define $\mathsf{code}:P\to P\to\mathcal{U}$ by double induction as follows

•

$\mathsf{code}(ib,ib^{\prime})$ is now a set-quotient of the type of sequences

$(b,p_{0},x_{1},q_{1},y_{1},p_{1},x_{2},q_{2},y_{2},p_{2},\dots,y_{n},p_{n},b^{% \prime})$

where

–

$n:\mathbb{N}$ ,
–

$x_{k}:S$ and $y_{k}:S$ for $0<k\leq n$ ,
–

$p_{0}:\Pi_{1}B(b,fkx_{1})$ and $p_{n}:\Pi_{1}B(fky_{n},b^{\prime})$ for $n>0$ , and $p_{0}:\Pi_{1}B(b,b^{\prime})$ for $n=0$ ,
–

$p_{k}:\Pi_{1}B(fky_{k},fkx_{k+1})$ for $1\leq k<n$ ,
–

$q_{k}:\Pi_{1}C(gkx_{k},gky_{k})$ for $1\leq k\leq n$ .

The quotient is generated by the following equalities (see \autorefrmk:naive):

$\displaystyle(\dots,q_{k},y_{k},\mathsf{refl}_{fy_{k}},y_{k},q_{k+1},\dots)$	$\displaystyle=(\dots,q_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q_{k+1},\dots)$
$\displaystyle(\dots,p_{k},x_{k},\mathsf{refl}_{gx_{k}},x_{k},p_{k+1},\dots)$	$\displaystyle=(\dots,p_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p_{k+1},\dots)$
$\displaystyle(\dots,p_{k-1}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}fw,x_{k}^{\prime},q_{k},\dots)$	$\displaystyle=(\dots,p_{k-1},x_{k},gw\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}q_{k},\dots){}$	(for $w:\Pi_{1}A(kx_{k},kx_{k}^{\prime})$)
$\displaystyle(\dots,q_{k}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}gw,y_{k}^{\prime},p_{k},\dots)$	$\displaystyle=(\dots,q_{k},y_{k},fw\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p_{k},\dots).{}$	(for $w:\Pi_{1}A(ky_{k},ky_{k}^{\prime})$)

We will need below the definition of the case of $\mathsf{decode}$ on such a sequence, which as before concatenates all the paths $p_{k}$ and $q_{k}$ together with instances of $h$ to give an element of $\Pi_{1}P(ifb,ifb^{\prime})$ , cf. (LABEL:eq:decode). As before, the other three point cases are nearly identical.

•

For $a : A$ and $b : B$ , we require an equivalence

$\mathsf{code}(ib,ifa)\simeq\mathsf{code}(ib,jga).$

(8.7.3)

Since $\mathsf{code}$ is set-valued, by \autorefthm:kbar we may assume that $a=\overline{k}t$ for some $t : T$ . Next, we can do induction on $t$ . If $t\equiv\ell s$ for $s : S$ , then we define (8.7.3) as in \autorefsec:naive-vankampen:

	$\displaystyle(\dots,y_{n},p_{n},fks)$	$\displaystyle\mapsto(\dots,y_{n},p_{n},s,\mathsf{refl}_{gks},gks),$
	$\displaystyle(\dots,x_{n},p_{n},s,\mathsf{refl}_{fks},fks)$	$\displaystyle\mapsfrom(\dots,x_{n},p_{n},gks).$

These respect the equivalence relations, and define quasi-inverses just as before. Now suppose $t$ varies along $m_{s,s^{\prime}}(w)$ for some $w:ks=ks^{\prime}$ ; we must show that (8.7.3) respects transporting along $\overline{k}mw$ . By definition of $\overline{k}$ , this essentially boils down to transporting along $w$ itself. By the characterization of transport in path types, what we need to show is that

$w_{*}(\dots,y_{n},p_{n},fks)=(\dots,y_{n},p_{n}\mathchoice{\mathbin{\raisebox{% 2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}% }{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}fw,fks^{\prime})$

is mapped by (8.7.3) to

$w_{*}(\dots,y_{n},p_{n},s,\mathsf{refl}_{gks},gks)=(\dots,y_{n},p_{n},s,% \mathsf{refl}_{gks}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}gw,gks^{\prime})$

But this follows directly from the new generators we have imposed on the set-quotient relation defining $\mathsf{code}$ .

•

The other three requisite equivalences are defined similarly.
•

Finally, since the commutativity (LABEL:eq:bfa-bga-comm) is a mere proposition, by $(-1)$ -connectedness of $k$ we may assume that $a=ks$ and $a^{\prime}=ks^{\prime}$ , in which case it follows exactly as before.

Theorem 8.7.4 (van Kampen with a set of basepoints).

For all $u, v : P$ there is an equivalence

$\Pi_{1}P(u,v)\simeq\mathsf{code}(u,v).$

with $\mathsf{code}$ defined as in this section.

Proof.

Basically just like before. To show that $\mathsf{decode}$ respects the new generators of the quotient relation, we use the naturality of $h$ . And to show that $\mathsf{decode}$ respects the equivalences such as (8.7.3), we need to induct on $\overline{k}$ and on $T$ in order to decompose those equivalences into their definitions, but then it becomes again simply functoriality of $f$ and $g$ . The rest is easy. In particular, no additional argument is required for $\mathsf{encode}\circ\mathsf{decode}$ , since the goal is to prove an equality in a set, and so the case of $h$ is trivial. ∎

\autoref

thm:van-Kampen allows us to calculate the fundamental group of a space $A$ , even when $A$ is not a set, provided $S$ is a set, for in that case, each $\mathsf{code}(u,v)$ is, by definition, a set-quotient of a set by a relation. In that respect, it is an improvement over \autorefthm:naive-van-kampen.

Example 8.7.5.

Suppose $S:\!\!\equiv\mathbf{1}$ , so that $A$ has a basepoint $a:\!\!\equiv k(\star)$ and is connected. Then code for loops in the pushout can be identified with alternating sequences of loops in $\pi_{1}(B,f(a))$ and $\pi_{1}(C,g(a))$ , modulo an equivalence relation which allows us to slide elements of $\pi_{1}(A,a)$ between them (after applying $f$ and $g$ respectively). Thus, $\pi_{1}(P)$ can be identified with the amalgamated free product $\pi_{1}(B)*_{\pi_{1}(A)}\pi_{1}(C)$ (the pushout in the category of groups), as constructed in \autorefsec:free-algebras. This (in the case when $B$ and $C$ are open subspaces of $P$ and $A$ their intersection) is probably the most classical version of the van Kampen theorem.

Example 8.7.6.

As a special case of \autorefeg:clvk, suppose additionally that $C:\!\!\equiv\mathbf{1}$ , so that $P$ is the cofiber $B/A$ . Then every loop in $C$ is equal to reflexivity, so the relations on path codes allow us to collapse all sequences to a single loop in $B$ . The additional relations require that multiplying on the left, right, or in the middle by an element in the image of $\pi_{1}(A)$ is the identity. We can thus identify $\pi_{1}(B/A)$ with the quotient of the group $\pi_{1}(B)$ by the normal subgroup generated by the image of $\pi_{1}(A)$ .

Example 8.7.7.

As a further special case of \autorefeg:cofiber, let $B:\!\!\equiv S^{1}\vee S^{1}$ , let $A:\!\!\equiv S^{1}$ , and let $f:A\to B$ pick out the composite loop $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{q}^{-1}}$ , where $p$ and $q$ are the generating loops in the two copies of $S^{1}$ comprising $B$ . Then $P$ is a presentation of the torus $T^{2}$ . Indeed, it is not hard to identify $P$ with the presentation of $T^{2}$ as described in \autorefsec:hubs-spokes, using the cone on a particular loop. Thus, $\pi_{1}(T^{2})$ is the quotient of the free group on two generators (i.e., $\pi_{1}(B)$ ) by the relation $p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{q}^{-1}}=1$ . This clearly yields the free abelian group on two generators, which is $\mathbb{Z}\times\mathbb{Z}$ .

Example 8.7.8.

More generally, any CW complex can be obtained by repeatedly “coning off” spheres, as described in \autorefsec:hubs-spokes. That is, we start with a set $X_{0}$ of points (“0-cells”), which is the “0-skeleton” of the CW complex. We take the pushout

$\vbox{\xymatrix{ S_1 \times\mathbb{S}^0\ar[r]^-{f_1}\ar[d] & X_0\ar[d]\\ $\mathbf{1}$ \ar[r] & X_1 }}$

for some set $S_{1}$ of 1-cells and some family $f_{1}$ of “attaching maps”, obtaining the “1-skeleton” $X_{1}$ . Then we take the pushout

$\vbox{\xymatrix{ S_2 \times\mathbb{S}^1\ar[r]^{f_2}\ar[d] & X_1\ar[d]\\ $\mathbf{1}$ \ar[r] & X_2 }}$

for some set $S_{2}$ of 2-cells and some family $f_{2}$ of attaching maps, obtaining the 2-skeleton $X_{2}$ , and so on. The fundamental group of each pushout can be calculated from the van Kampen theorem: we obtain the group presented by generators derived from the 1-skeleton, and relations derived from $S_{2}$ and $f_{2}$ . The pushouts after this stage do not alter the fundamental group, since $\pi_{1}(\mathbb{S}^{n})$ is trivial for $n>1$ (see \autorefsec:pik-le-n).

Example 8.7.9.

In particular, suppose given any presentation of a (set-)group $G=\langle X\mid R\rangle$ , with $X$ a set of generators and $R$ a set of words in these generators. Let $B:\!\!\equiv\bigvee_{X}S^{1}$ and $A:\!\!\equiv\bigvee_{R}S^{1}$ , with $f:A\to B$ sending each copy of $S^{1}$ to the corresponding word in the generating loops of $B$ . It follows that $\pi_{1}(P)\cong G$ ; thus we have constructed a connected type whose fundamental group is $G$ . Since any group has a presentation, any group is the fundamental group of some type. If we 1-truncate such a type, we obtain a type whose only nontrivial homotopy group is $G$ ; this is called an Eilenberg–Mac Lane space $K(G,1)$ .

Title	8.7.2 The van Kampen theorem with a set of basepoints
\metatable