6.5 Suspensions

The suspension of a type $A$ is the universal way of making the points of $A$ into paths (and hence the paths in $A$ into 2-paths, and so on).It is a type $\mathrm{\Sigma }A$ defined by the following generators:

• a point $𝖭:\mathrm{\Sigma }A$,

• a point $𝖲:\mathrm{\Sigma }A$, and

• a function $\mathrm{𝗆𝖾𝗋𝗂𝖽}:A\to (𝖭{=}_{\mathrm{\Sigma }A}𝖲)$.

The names are intended to suggest a “globe” of sorts, with a north pole, a south pole, and an $A$’s worth of meridiansfrom one to the other.Indeed, as we will see, if $A={𝕊}^1$, then its suspension is equivalent to the surface of an ordinary sphere, ${𝕊}^2$.

The recursion principle for $\mathrm{\Sigma }A$ says that given a type $B$ together with

• points $n,s:B$ and

• a function $m:A\to (n=s)$,

we have a function $f:\mathrm{\Sigma }A\to B$ such that $f(𝖭)\equiv n$ and $f(𝖲)\equiv s$, and for all $a:A$ we have $f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\right)=m(a)$.Similarly, the induction principle says that given $P:\mathrm{\Sigma }A\to 𝒰$ together with

• a point $n:P(𝖭)$,

• a point $s:P(𝖲)$, and

• for each $a:A$, a path $m(a):n{=}_{\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)}^{P}s$,

there exists a function $f:{\prod }_{(x:\mathrm{\Sigma }A)}P(x)$ such that $f(𝖭)\equiv n$ and $f(𝖲)\equiv s$ and for each $a:A$ we have ${\mathrm{𝖺𝗉𝖽}}_f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\right)=m(a)$.

Our first observation about suspension is that it gives another way to define the circle.

Lemma 6.5.1.

$\mathrm{\Sigma }\mathrm{𝟐}\simeq {𝕊}^1$.

Proof.

Define $f:\mathrm{\Sigma }\mathrm{𝟐}\to {𝕊}^1$ by recursion such that $f(𝖭):\equiv \mathrm{𝖻𝖺𝗌𝖾}$ and $f(𝖲):\equiv \mathrm{𝖻𝖺𝗌𝖾}$, while $f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\right):=\mathrm{𝗅𝗈𝗈𝗉}$ but $f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})\right):={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$.Define $g:{𝕊}^1\to \mathrm{\Sigma }\mathrm{𝟐}$ by recursion such that $g(\mathrm{𝖻𝖺𝗌𝖾}):\equiv 𝖭$ and $g\left(\mathrm{𝗅𝗈𝗈𝗉}\right):=\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\mathrm{𝗆𝖾𝗋𝗂𝖽}{(1_{\mathrm{𝟐}})}^{-1}$.We now show that $f$ and $g$ are quasi-inverses.

First we show by induction that $g(f(x))=x$ for all $x:\mathrm{\Sigma }\mathrm{𝟐}$.If $x\equiv 𝖭$, then $g(f(𝖭))\equiv g(\mathrm{𝖻𝖺𝗌𝖾})\equiv 𝖭$, so we have ${\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}:g(f(𝖭))=𝖭$.If $x\equiv 𝖲$, then $g(f(𝖲))\equiv g(\mathrm{𝖻𝖺𝗌𝖾})\equiv 𝖭$, and we choose the equality $\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}}):g(f(𝖲))=𝖲$.It remains to show that for any $y:\mathrm{𝟐}$, these equalities are preserved as $x$ varies along $\mathrm{𝗆𝖾𝗋𝗂𝖽}(y)$, which is to say that when ${\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}$ is transported along $\mathrm{𝗆𝖾𝗋𝗂𝖽}(y)$ it yields $\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})$.By transport in path spaces and pulled back fibrations, this means we are to show that

$$g{\left(f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(y)\right)\right)}^{-1}{\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}\mathrm{𝗆𝖾𝗋𝗂𝖽}(y)=\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}}).$$

Of course, we may cancel ${\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}$.Now by $\mathrm{𝟐}$-induction, we may assume either $y\equiv 0_{\mathrm{𝟐}}$ or $y\equiv 1_{\mathrm{𝟐}}$.If $y\equiv 0_{\mathrm{𝟐}}$, then we have

$g{\left(f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\right)\right)}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})$$=g{\left(\mathrm{𝗅𝗈𝗈𝗉}\right)}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})$

$={(\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\mathrm{𝗆𝖾𝗋𝗂𝖽}{(1_{\mathrm{𝟐}})}^{-1})}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})$

$=\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})\mathrm{𝗆𝖾𝗋𝗂𝖽}{(0_{\mathrm{𝟐}})}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})$

$=\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})$

while if $y\equiv 1_{\mathrm{𝟐}}$, then we have

$g{\left(f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})\right)\right)}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})$$=g{\left({\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}\right)}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})$

$=\mathrm{𝗋𝖾𝖿𝗅}_{𝖭}{}^{-1}\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})$

$=\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}}).$

Thus, for all $x:\mathrm{\Sigma }\mathrm{𝟐}$, we have $g(f(x))=x$.

Now we show by induction that $f(g(x))=x$ for all $x:{𝕊}^1$.If $x\equiv \mathrm{𝖻𝖺𝗌𝖾}$, then $f(g(\mathrm{𝖻𝖺𝗌𝖾}))\equiv f(𝖭)\equiv \mathrm{𝖻𝖺𝗌𝖾}$, so we have ${\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}:f(g(\mathrm{𝖻𝖺𝗌𝖾}))=\mathrm{𝖻𝖺𝗌𝖾}$.It remains to show that this equality is preserved as $x$ varies along $\mathrm{𝗅𝗈𝗈𝗉}$, which is to say that it is transported along $\mathrm{𝗅𝗈𝗈𝗉}$ to itself.Again, by transport in path spaces and pulled back fibrations, this means to show that

$$f{\left(g\left(\mathrm{𝗅𝗈𝗈𝗉}\right)\right)}^{-1}{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}\mathrm{𝗅𝗈𝗈𝗉}={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}.$$

However, we have

$f\left(g\left(\mathrm{𝗅𝗈𝗈𝗉}\right)\right)$$=f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\mathrm{𝗆𝖾𝗋𝗂𝖽}{(1_{\mathrm{𝟐}})}^{-1}\right)$

$=f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(0_{\mathrm{𝟐}})\right)f{\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(1_{\mathrm{𝟐}})\right)}^{-1}$

$=\mathrm{𝗅𝗈𝗈𝗉}{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$

so this follows easily.∎

Topologically, the two-point space $\mathrm{𝟐}$ is also known as the 0-dimensional sphere, ${𝕊}^0$.(For instance, it is the space of points at distance $1$ from the origin in ${ℝ}^1$, just as the topological 1-sphere is the space of points at distance $1$ from the origin in ${ℝ}^2$.)Thus, Lemma 6.5.1 (http://planetmath.org/65suspensions#Thmprelem1) can be phrased suggestively as $\mathrm{\Sigma }{𝕊}^0\simeq {𝕊}^1$.In fact, this pattern continues: we can define all the spheres inductively by

$${𝕊}^0:\equiv \mathrm{𝟐}\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}{𝕊}^{n+1}:\equiv \mathrm{\Sigma }{𝕊}^n.$$(6.5.2)

We can even start one dimension lower by defining ${𝕊}^{-1}:\equiv \mathrm{𝟎}$, and observe that $\mathrm{\Sigma }\mathrm{𝟎}\simeq \mathrm{𝟐}$.

To prove carefully that this agrees with the definition of ${𝕊}^n$ from the previous section would require making the latter more explicit.However, we can show that the recursive definition has the same universal property that we would expect the other one to have.If $(A,a_0)$ and $(B,b_0)$ are pointed types (with basepoints often left implicit), let ${\mathrm{𝖬𝖺𝗉}}_{*}(A,B)$ denote the type of based maps:

$${\mathrm{𝖬𝖺𝗉}}_{*}(A,B):\equiv \sum _{f:A\to B}(f(a_0)=b_0).$$

Note that any type $A$ gives rise to a pointed type $A_{+}:\equiv A+\mathrm{𝟏}$ with basepoint $\mathrm{𝗂𝗇𝗋}(\star )$; this is called adjoining a disjoint basepoint.

Lemma 6.5.3.

For a type $A$ and a pointed type $\mathrm{(}B\mathrm{,}{b}_{\mathrm{0}}\mathrm{)}$, we have

$${\mathrm{𝖬𝖺𝗉}}_{*}(A_{+},B)\simeq (A\to B)$$

Note that on the right we have the ordinary type of unbased functions from $A$ to $B$.

Proof.

From left to right, given $f:A_{+}\to B$ with $p:f(\mathrm{𝗂𝗇𝗋}(\star ))=b_0$, we have $f\circ \mathrm{𝗂𝗇𝗅}:A\to B$.And from right to left, given $g:A\to B$ we define $g^{\prime }:A_{+}\to B$ by $g^{\prime }(\mathrm{𝗂𝗇𝗅}(a)):\equiv g(a)$ and $g^{\prime }(\mathrm{𝗂𝗇𝗋}(u)):\equiv b_0$.We leave it to the reader to show that these are quasi-inverse operations.∎

In particular, note that $\mathrm{𝟐}\simeq {\mathrm{𝟏}}_{+}$.Thus, for any pointed type $B$ we have

$${\mathrm{𝖬𝖺𝗉}}_{*}(\mathrm{𝟐},B)\simeq (\mathrm{𝟏}\to B)\simeq B.$$

Now recall that the loop space operation $\mathrm{\Omega }$ acts on pointed types, with definition $\mathrm{\Omega }(A,a_0):\equiv (a_0{=}_A{a}_0,{\mathrm{𝗋𝖾𝖿𝗅}}_{a_0})$.We can also make the suspension $\mathrm{\Sigma }$ act on pointed types, by $\mathrm{\Sigma }(A,a_0):\equiv (\mathrm{\Sigma }A,𝖭)$.

Lemma 6.5.4.

For pointed types $\mathrm{(}A\mathrm{,}{a}_{\mathrm{0}}\mathrm{)}$ and $\mathrm{(}B\mathrm{,}{b}_{\mathrm{0}}\mathrm{)}$ we have

$${\mathrm{𝖬𝖺𝗉}}_{*}(\mathrm{\Sigma }A,B)\simeq {\mathrm{𝖬𝖺𝗉}}_{*}(A,\mathrm{\Omega }B).$$

Proof.

From left to right, given $f:\mathrm{\Sigma }A\to B$ with $p:f(𝖭)=b_0$, we define $g:A\to \mathrm{\Omega }B$ by

$$g(a):\equiv p^{-1}f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a_0)}^{-1}\right)p.$$

Then we have

$g(a_0)$$\equiv p^{-1}f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a_0)\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a_0)}^{-1}\right)p$

$=p^{-1}f\left({\mathrm{𝗋𝖾𝖿𝗅}}_{𝖭}\right)p$

$=p^{-1}p$

$={\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}.$

Thus, denoting this path by $q:g(a_0)={\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}$, we have $(g,q):{\mathrm{𝖬𝖺𝗉}}_{*}(A,\mathrm{\Omega }B)$.

On the other hand, from right to left, given $g:A\to \mathrm{\Omega }B$ and $q:g(a_0)={\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}$, we define $f:\mathrm{\Sigma }A\to B$ by $\mathrm{\Sigma }$-recursion, such that $f(𝖭):\equiv b_0$ and $f(𝖲):\equiv b_0$ and

$$f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\right):=g(a).$$

Then we can simply take $p$ to be ${\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}:f(𝖭)=b_0$.

Now given $(f,p)$, by passing back and forth we obtain $(f^{\prime },p^{\prime })$ where $f^{\prime }$ is defined by $f^{\prime }(𝖭)\equiv b_0$ and $f^{\prime }(𝖲)\equiv b_0$ and

$$f^{\prime }\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\right)=p^{-1}f\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\mathrm{𝗆𝖾𝗋𝗂𝖽}{(a_0)}^{-1}\right)p,$$

while $p^{\prime }\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}$.To show $f=f^{\prime }$, by function extensionality it suffices to show $f(x)=f^{\prime }(x)$ for all $x:\mathrm{\Sigma }A$, so we can use the induction principle of suspension.First, we have

$$f(𝖭)\stackrel{𝑝}{=}{b}_0\equiv f^{\prime }(𝖭).$$(6.5.5)

Second, we have

HoTT_fig_6.5.1.png

And thirdly, as $x$ varies along $\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)$ we must show that the following diagram of paths commutes (invoking the definition of $f^{\prime }\left(\mathrm{𝗆𝖾𝗋𝗂𝖽}(a)\right)$):

HoTT_fig_6.5.2.png

This is clear.Thus, to show that $(f,p)=(f^{\prime },p^{\prime })$, it remains only to show that $p$ is identified with $p^{\prime }$ when transported along this equality $f=f^{\prime }$.Since the type of $p$ is $f(𝖭)=b_0$, this means essentially that when $p$ is composed on the left with the inverse of the equality (6.5.5), it becomes $p^{\prime }$.But this is obvious, since (6.5.5) is just $p$ itself, while $p^{\prime }$ is reflexivity.

On the other side, suppose given $(g,q)$.By passing back and forth we obtain $(g^{\prime },q^{\prime })$ with

$g^{\prime }(a)$$=\mathrm{𝗋𝖾𝖿𝗅}_{b_0}{}^{-1}g(a)g{(a_0)}^{-1}{\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}$

$=g(a)g{(a_0)}^{-1}$

$=g(a)$

using $q:g(a_0)={\mathrm{𝗋𝖾𝖿𝗅}}_{b_0}$ in the last equality.Thus, $g^{\prime }=g$ by function extensionality, so it remains to show that when transported along this equality $q$ is identified with $q^{\prime }$.At $a_0$, the induced equality $g(a_0)=g^{\prime }(a_0)$ consists essentially of $q$ itself, while the definition of $q^{\prime }$ involves only canceling inverses and reflexivities.Thus, some tedious manipulations of naturality finish the proof.∎

In particular, for the spheres defined as in (6.5.2) we have

$${\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^n,B)\simeq {\mathrm{𝖬𝖺𝗉}}_{*}({𝕊}^{n-1},\mathrm{\Omega }B)\simeq \mathrm{\cdots }\simeq {\mathrm{𝖬𝖺𝗉}}_{*}(\mathrm{𝟐},{\mathrm{\Omega }}^{n}B)\simeq {\mathrm{\Omega }}^{n}B.$$

Thus, these spheres ${𝕊}^n$ have the universal property that we would expect from the spheres defined directly in terms of $n$-fold loop spaces as in §6.4 (http://planetmath.org/64circlesandspheres).