8.2 Connectedness of suspensions

Recall from \autorefsec:connectivity that a type A is called n-connected if βˆ₯Aβˆ₯n is contractibleMathworldPlanetmath. The aim of this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath is to prove that the operationMathworldPlanetmath of suspension from \autorefsec:suspension increases connectedness.

Theorem 8.2.1.

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


We remarked in \autorefsec:colimitsMathworldPlanetmath that the suspension of A is the pushout πŸβŠ”A𝟏, so we need to prove that the following type is contractible:


By \autorefreflectcommutespushout we know that βˆ₯πŸβŠ”A𝟏βˆ₯n+1 is a pushout in (n+1)⁒-⁒𝖳𝗒𝗉𝖾 of the diagram


Given that βˆ₯𝟏βˆ₯n+1=𝟏, the type βˆ₯πŸβŠ”A𝟏βˆ₯n+1 is also a pushout of the following diagram in (n+1)⁒-⁒𝖳𝗒𝗉𝖾 (because both diagrams are equal)

π’Ÿ=\xymatrixβˆ₯Aβˆ₯_n+1\ar[d]Β \ar[r] & 𝟏 
𝟏 & 

We will now prove that 𝟏 is also a pushout of π’Ÿ in (n+1)⁒-⁒𝖳𝗒𝗉𝖾. Let E be an (n+1)-truncated type; we need to prove that the following map is an equivalence


where we recall that π–Όπ—ˆπ–Όπ—ˆπ—‡π–Ύπ’Ÿβ’(E) is the type


The map {(πŸβ†’E)⟢Ef⟼f⁒(⋆) is an equivalence, hence we also have


Now A is n-connected hence so is βˆ₯Aβˆ₯n+1 because βˆ₯βˆ₯Aβˆ₯n+1βˆ₯n=βˆ₯Aβˆ₯n=𝟏, and (x=Ey) is n-truncated because E is (n+1)-connected. Hence by \autorefconnectedtotruncated the following map is an equivalence


Hence we have


But the following map is an equivalence




Finally we get an equivalence


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 𝟏 is a pushout of π’Ÿ in (n+1)⁒-⁒𝖳𝗒𝗉𝖾. Using uniqueness of pushouts we get that βˆ₯πŸβŠ”A𝟏βˆ₯n+1=𝟏 which proves that the suspension of A is (n+1)-connected. ∎

Corollary 8.2.2.

For all n:N, the sphere Sn is (n-1)-connected.


We prove this by inductionMathworldPlanetmath on n. For n=0 we have to prove that π•Š0 is merely inhabited, which is clear. Let 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