8.2 Connectedness of suspensions

Theorem 8.2.1.

If $A$ is $n$-connected then the suspension of $A$ is $(n+1)$-connected.

Proof.

We remarked in \autorefsec:colimits  that the suspension of $A$ is the pushout $\mathbf{1}\sqcup^{A}\mathbf{1}$, so we need to prove that the following type is contractible:

 $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}.$

By \autorefreflectcommutespushout we know that $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}$ is a pushout in ${(n+1)}\text{-}\mathsf{Type}$ of the diagram

 $\xymatrix{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}\ar[d]\ar[r]&\mathopen{% }\left\|\mathbf{1}\right\|_{n+1}\mathclose{}\\ \mathopen{}\left\|\mathbf{1}\right\|_{n+1}\mathclose{}&}.$

Given that $\mathopen{}\left\|\mathbf{1}\right\|_{n+1}\mathclose{}=\mathbf{1}$, the type $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}$ is also a pushout of the following diagram in ${(n+1)}\text{-}\mathsf{Type}$ (because both diagrams are equal)

 $\mathscr{D}=\vbox{\xymatrix{\mathopen{}\left\|A\right\|_{n+1}\mathclose{} \ar[% d] \ar[r] & \mathbf{1} \\ \mathbf{1} & }}.$

We will now prove that $\mathbf{1}$ is also a pushout of $\mathscr{D}$ in ${(n+1)}\text{-}\mathsf{Type}$. Let $E$ be an $(n+1)$-truncated type; we need to prove that the following map is an equivalence

 $\left\{\begin{array}[]{rcl}(\mathbf{1}\to E)&\longrightarrow&\mathsf{cocone}_{% \mathscr{D}}(E)\\ y&\longmapsto&(y,y,{\lambda}u.\,\mathsf{refl}_{y(\star)})\end{array}\right..$

where we recall that $\mathsf{cocone}_{\mathscr{D}}(E)$ is the type

 $\mathchoice{\sum_{(f:\mathbf{1}\to E)}\,}{\mathchoice{{\textstyle\sum_{(f:% \mathbf{1}\to E)}}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{% \sum_{(f:\mathbf{1}\to E)}}}{\mathchoice{{\textstyle\sum_{(f:\mathbf{1}\to E)}% }}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}% \to E)}}}{\mathchoice{{\textstyle\sum_{(f:\mathbf{1}\to E)}}}{\sum_{(f:\mathbf% {1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}}% \mathchoice{\sum_{(g:\mathbf{1}\to E)}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathbf{1}\to E)}}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{% \sum_{(g:\mathbf{1}\to E)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbf{1}\to E)}% }}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}% \to E)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbf{1}\to E)}}}{\sum_{(g:\mathbf% {1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}}(\mathopen% {}\left\|A\right\|_{n+1}\mathclose{}\to(f(\star)=_{E}{}g(\star))).$

The map $\left\{\begin{array}[]{rcl}(\mathbf{1}\to E)&\longrightarrow&E\\ f&\longmapsto&f(\star)\end{array}\right.$ is an equivalence, hence we also have

 $\mathsf{cocone}_{\mathscr{D}}(E)=\mathchoice{\sum_{(x:E)}\,}{\mathchoice{{% \textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}}}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum_{(% y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(\mathopen{}\left\|A\right\|_{n+1}% \mathclose{}\to(x=_{E}y)).$

Now $A$ is $n$-connected hence so is $\mathopen{}\left\|A\right\|_{n+1}\mathclose{}$ because $\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n+1}\mathclose{}\right\|_{n}% \mathclose{}=\mathopen{}\left\|A\right\|_{n}\mathclose{}=\mathbf{1}$, and $(x=_{E}y)$ is $n$-truncated because $E$ is $(n+1)$-connected. Hence by \autorefconnectedtotruncated the following map is an equivalence

 $\left\{\begin{array}[]{rcl}(x=_{E}y)&\longrightarrow&(\mathopen{}\left\|A% \right\|_{n+1}\mathclose{}\to(x=_{E}y))\\ p&\longmapsto&{\lambda}z.\,p\end{array}\right.$

Hence we have

 $\mathsf{cocone}_{\mathscr{D}}(E)=\mathchoice{\sum_{(x:E)}\,}{\mathchoice{{% \textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}}}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum_{(% y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(x=_{E}y).$

But the following map is an equivalence

 $\left\{\begin{array}[]{rcl}E&\longrightarrow&\mathchoice{\sum_{(x:E)}\,}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{% (x:E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}% }}{\sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(x=_{E}y)\\ x&\longmapsto&(x,x,\mathsf{refl}_{x})\end{array}\right..$

Hence

 $\mathsf{cocone}_{\mathscr{D}}(E)=E.$

Finally we get an equivalence

 $(\mathbf{1}\to E)\simeq\mathsf{cocone}_{\mathscr{D}}(E)$

We can now unfold the definitions in order to get the explicit expression of this map, and we see easily that this is exactly the map we had at the beginning.

Hence we proved that $\mathbf{1}$ is a pushout of $\mathscr{D}$ in ${(n+1)}\text{-}\mathsf{Type}$. Using uniqueness of pushouts we get that $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}=% \mathbf{1}$ which proves that the suspension of $A$ is $(n+1)$-connected. ∎

Corollary 8.2.2.

For all $n:\mathbb{N}$, the sphere $\mathbb{S}^{n}$ is $(n-1)$-connected.

Proof.

We prove this by induction  on $n$. For $n=0$ we have to prove that $\mathbb{S}^{0}$ is merely inhabited, which is clear. Let $n:\mathbb{N}$ be such that $\mathbb{S}^{n}$ is $(n-1)$-connected. By definition $\mathbb{S}^{n+1}$ is the suspension of $\mathbb{S}^{n}$, hence by the previous lemma $\mathbb{S}^{n+1}$ is $n$-connected. ∎

Title 8.2 Connectedness of suspensions
\metatable