8.2 Connectedness of suspensions

Recall from sec:connectivity that a type $A$ is called $n$-connected if ${\parallel A\parallel }_n$ is contractible. The aim of this section is to prove that the operation of suspension from sec:suspension increases connectedness.

Theorem 8.2.1.

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

Proof.

We remarked in sec:colimits that the suspension of $A$ is the pushout $\mathrm{𝟏}{\bigsqcup }^A\mathrm{𝟏}$, so we need to prove that the following type is contractible:

$${\parallel \mathrm{𝟏}{\bigsqcup }^A\mathrm{𝟏}\parallel }_{n+1}.$$

By reflectcommutespushout we know that ${\parallel \mathrm{𝟏}{\bigsqcup }^A\mathrm{𝟏}\parallel }_{n+1}$ is a pushout in $(n+1)\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ of the diagram

Given that $\parallel \mathrm{𝟏}{\parallel }_{n+1}=\mathrm{𝟏}$, the type ${\parallel \mathrm{𝟏}{\bigsqcup }^A\mathrm{𝟏}\parallel }_{n+1}$ is also a pushout of the following diagram in $(n+1)\text{-}\mathrm{𝖳𝗒𝗉𝖾}$ (because both diagrams are equal)

We will now prove that $\mathrm{𝟏}$ is also a pushout of $𝒟$ in $(n+1)\text{-}\mathrm{𝖳𝗒𝗉𝖾}$. Let $E$ be an $(n+1)$-truncated type; we need to prove that the following map is an equivalence

where we recall that ${\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(E)$ is the type

$$\sum _{(f:\mathrm{𝟏}\to E)}\sum _{(g:\mathrm{𝟏}\to E)}(\parallel A{\parallel }_{n+1}\to (f(\star ){=}_{E}g(\star ))).$$

The map is an equivalence, hence we also have

$${\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(E)=\sum _{(x:E)}\sum _{(y:E)}(\parallel A{\parallel }_{n+1}\to (x{=}_{E}y)).$$

Now $A$ is $n$-connected hence so is ${\parallel A\parallel }_{n+1}$ because $\parallel \parallel A{\parallel }_{n+1}{\parallel }_n=\parallel A{\parallel }_n=\mathrm{𝟏}$, and $(x{=}_{E}y)$ is $n$-truncated because $E$ is $(n+1)$-connected. Hence by connectedtotruncated the following map is an equivalence

Hence we have

$${\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(E)=\sum _{(x:E)}\sum _{(y:E)}(x{=}_{E}y).$$

But the following map is an equivalence

Hence

$${\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(E)=E.$$

Finally we get an equivalence

$$(\mathrm{𝟏}\to E)\simeq {\mathrm{𝖼𝗈𝖼𝗈𝗇𝖾}}_{𝒟}(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 $\mathrm{𝟏}$ is a pushout of $𝒟$ in $(n+1)\text{-}\mathrm{𝖳𝗒𝗉𝖾}$. Using uniqueness of pushouts we get that $\parallel \mathrm{𝟏}{\bigsqcup }^A\mathrm{𝟏}{\parallel }_{n+1}=\mathrm{𝟏}$ which proves that the suspension of $A$ is $(n+1)$-connected. ∎

Corollary 8.2.2.

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

Proof.

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

Title	8.2 Connectedness of suspensions