6.5 Suspensions


The suspension of a type A is the universalPlanetmathPlanetmathPlanetmath 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 Σ⁒A defined by the following generatorsPlanetmathPlanetmath:11There is an unfortunate clash of notation with dependent pair types, which of course are also written with a Σ. However, context usually disambiguates.

  • β€’

    a point 𝖭:Σ⁒A,

  • β€’

    a point 𝖲:Σ⁒A, and

  • β€’

    a function 𝗆𝖾𝗋𝗂𝖽:Aβ†’(𝖭=Σ⁒A𝖲).

The names are intended to suggest a β€œglobe” of sorts, with a north pole, a south pole, and an A’s worth of meridians from one to the other. Indeed, as we will see, if A=π•Š1, then its suspension is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the surface of an ordinary sphere, π•Š2.

The recursion principle for Σ⁒A says that given a type B together with

  • β€’

    points n,s:B and

  • β€’

    a function m:A→(n=s),

we have a function f:Σ⁒Aβ†’B such that f⁒(𝖭)≑n and f⁒(𝖲)≑s, and for all a:A we have f(𝗆𝖾𝗋𝗂𝖽(a))=m(a). Similarly, the inductionMathworldPlanetmath principle says that given P:Σ⁒A→𝒰 together with

  • β€’

    a point n:P⁒(𝖭),

  • β€’

    a point s:P⁒(𝖲), and

  • β€’

    for each a:A, a path m⁒(a):n=𝗆𝖾𝗋𝗂𝖽⁒(a)Ps,

there exists a function f:∏(x:Ξ£A)P⁒(x) such that f⁒(𝖭)≑n and f⁒(𝖲)≑s and for each a:A we have 𝖺𝗉𝖽f(𝗆𝖾𝗋𝗂𝖽(a))=m(a).

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

Lemma 6.5.1.

Ξ£β’πŸβ‰ƒπ•Š1.

Proof.

Define f:Ξ£β’πŸβ†’π•Š1 by recursion such that f(𝖭):β‰‘π–»π–Ίπ—Œπ–Ύ and f(𝖲):β‰‘π–»π–Ίπ—Œπ–Ύ, while f(𝗆𝖾𝗋𝗂𝖽(0𝟐)):=π—…π—ˆπ—ˆπ—‰ but f(𝗆𝖾𝗋𝗂𝖽(1𝟐)):=π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ. Define g:π•Š1β†’Ξ£β’πŸ by recursion such that g(π–»π–Ίπ—Œπ–Ύ):≑𝖭 and g(π—…π—ˆπ—ˆπ—‰):=𝗆𝖾𝗋𝗂𝖽(0𝟐)\centerdot𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)-1. We now show that f and g are quasi-inverses.

First we show by induction that g⁒(f⁒(x))=x for all x:Σ⁒𝟐. If x≑𝖭, then g⁒(f⁒(𝖭))≑g⁒(π–»π–Ίπ—Œπ–Ύ)≑𝖭, so we have 𝗋𝖾𝖿𝗅𝖭:g⁒(f⁒(𝖭))=𝖭. If x≑𝖲, then g⁒(f⁒(𝖲))≑g⁒(π–»π–Ίπ—Œπ–Ύ)≑𝖭, and we choose the equality 𝗆𝖾𝗋𝗂𝖽⁒(1𝟐):g⁒(f⁒(𝖲))=𝖲. It remains to show that for any y:𝟐, these equalities are preserved as x varies along 𝗆𝖾𝗋𝗂𝖽⁒(y), which is to say that when 𝗋𝖾𝖿𝗅𝖭 is transported along 𝗆𝖾𝗋𝗂𝖽⁒(y) it yields 𝗆𝖾𝗋𝗂𝖽⁒(1𝟐). By transport in path spaces and pulled back fibrations, this means we are to show that

g(f(𝗆𝖾𝗋𝗂𝖽(y)))-1⁒\centerdot⁒𝗋𝖾𝖿𝗅𝖭⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(y)=𝗆𝖾𝗋𝗂𝖽⁒(1𝟐).

Of course, we may cancel 𝗋𝖾𝖿𝗅𝖭. Now by 𝟐-induction, we may assume either y≑0𝟐 or y≑1𝟐. If y≑0𝟐, then we have

g(f(𝗆𝖾𝗋𝗂𝖽(0𝟐)))-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(0𝟐) =g(π—…π—ˆπ—ˆπ—‰)-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(0𝟐)
=(𝗆𝖾𝗋𝗂𝖽⁒(0𝟐)⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)-1)-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(0𝟐)
=𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(0𝟐)-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(0𝟐)
=𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)

while if y≑1𝟐, then we have

g(f(𝗆𝖾𝗋𝗂𝖽(1𝟐)))-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(1𝟐) =g(π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ)-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)
=𝗋𝖾𝖿𝗅𝖭-1⁒\centerdot⁒𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)
=𝗆𝖾𝗋𝗂𝖽⁒(1𝟐).

Thus, for all x:Σ⁒𝟐, we have g⁒(f⁒(x))=x.

Now we show by induction that f⁒(g⁒(x))=x for all x:π•Š1. If xβ‰‘π–»π–Ίπ—Œπ–Ύ, then f⁒(g⁒(π–»π–Ίπ—Œπ–Ύ))≑f⁒(𝖭)β‰‘π–»π–Ίπ—Œπ–Ύ, so we have π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ:f⁒(g⁒(π–»π–Ίπ—Œπ–Ύ))=π–»π–Ίπ—Œπ–Ύ. It remains to show that this equality is preserved as x varies along π—…π—ˆπ—ˆπ—‰, which is to say that it is transported along π—…π—ˆπ—ˆπ—‰ to itself. Again, by transport in path spaces and pulled back fibrations, this means to show that

f(g(π—…π—ˆπ—ˆπ—‰))-1⁒\centerdotβ’π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύβ’\centerdotβ’π—…π—ˆπ—ˆπ—‰=π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ.

However, we have

f(g(π—…π—ˆπ—ˆπ—‰)) =f(𝗆𝖾𝗋𝗂𝖽(0𝟐)\centerdot𝗆𝖾𝗋𝗂𝖽⁒(1𝟐)-1)
=f(𝗆𝖾𝗋𝗂𝖽(0𝟐))\centerdotf(𝗆𝖾𝗋𝗂𝖽(1𝟐))-1
=π—…π—ˆπ—ˆπ—‰β’\centerdotβ’π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ

so this follows easily. ∎

Topologically, the two-point space 𝟐 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 Ξ£β’π•Š0β‰ƒπ•Š1. In fact, this pattern continues: we can define all the spheres inductively by

π•Š0:β‰‘πŸβ€ƒβ€ƒandβ€ƒβ€ƒπ•Šn+1:β‰‘Ξ£π•Šn. (6.5.2)

We can even start one dimensionMathworldPlanetmathPlanetmath lower by defining π•Š-1:β‰‘πŸŽ, and observe that Ξ£β’πŸŽβ‰ƒπŸ.

To prove carefully that this agrees with the definition of π•Šn from the previous sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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,a0) and (B,b0) are pointed types (with basepoints often left implicit), let 𝖬𝖺𝗉*⁒(A,B) denote the type of based maps:

𝖬𝖺𝗉*(A,B):β‰‘βˆ‘f:Aβ†’B(f(a0)=b0).

Note that any type A gives rise to a pointed type A+:≑A+𝟏 with basepoint 𝗂𝗇𝗋⁒(⋆); this is called adjoining a disjoint basepoint.

Lemma 6.5.3.

For a type A and a pointed type (B,b0), we have

𝖬𝖺𝗉*(A+,B)≃(Aβ†’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+β†’B with p:f⁒(𝗂𝗇𝗋⁒(⋆))=b0, we have fβˆ˜π—‚π—‡π—…:Aβ†’B. And from right to left, given g:Aβ†’B we define gβ€²:A+β†’B by gβ€²(𝗂𝗇𝗅(a)):≑g(a) and gβ€²(𝗂𝗇𝗋(u)):≑b0. We leave it to the reader to show that these are quasi-inverse operationsMathworldPlanetmath. ∎

In particular, note that πŸβ‰ƒπŸ+. Thus, for any pointed type B we have

𝖬𝖺𝗉*(𝟐,B)≃(πŸβ†’B)≃B.

Now recall that the loop spaceMathworldPlanetmath operation Ξ© acts on pointed types, with definition Ξ©(A,a0):≑(a0=Aa0,𝗋𝖾𝖿𝗅a0). We can also make the suspension Ξ£ act on pointed types, by Ξ£(A,a0):≑(Ξ£A,𝖭).

Lemma 6.5.4.

For pointed types (A,a0) and (B,b0) we have

𝖬𝖺𝗉*⁒(Σ⁒A,B)≃𝖬𝖺𝗉*⁒(A,Ω⁒B).
Proof.

From left to right, given f:Σ⁒Aβ†’B with p:f⁒(𝖭)=b0, we define g:A→Ω⁒B by

g(a):≑p-1\centerdotf(𝗆𝖾𝗋𝗂𝖽(a)\centerdot𝗆𝖾𝗋𝗂𝖽⁒(a0)-1)\centerdotp.

Then we have

g⁒(a0) ≑p-1\centerdotf(𝗆𝖾𝗋𝗂𝖽(a0)\centerdot𝗆𝖾𝗋𝗂𝖽⁒(a0)-1)\centerdotp
=p-1\centerdotf(𝗋𝖾𝖿𝗅𝖭)\centerdotp
=p-1⁒\centerdot⁒p
=𝗋𝖾𝖿𝗅b0.

Thus, denoting this path by q:g⁒(a0)=𝗋𝖾𝖿𝗅b0, we have (g,q):𝖬𝖺𝗉*⁒(A,Ω⁒B).

On the other hand, from right to left, given g:A→Ω⁒B and q:g⁒(a0)=𝗋𝖾𝖿𝗅b0, we define f:Σ⁒Aβ†’B by Ξ£-recursion, such that f(𝖭):≑b0 and f(𝖲):≑b0 and

f(𝗆𝖾𝗋𝗂𝖽(a)):=g(a).

Then we can simply take p to be 𝗋𝖾𝖿𝗅b0:f⁒(𝖭)=b0.

Now given (f,p), by passing back and forth we obtain (fβ€²,pβ€²) where fβ€² is defined by f′⁒(𝖭)≑b0 and f′⁒(𝖲)≑b0 and

fβ€²(𝗆𝖾𝗋𝗂𝖽(a))=p-1\centerdotf(𝗆𝖾𝗋𝗂𝖽(a)\centerdot𝗆𝖾𝗋𝗂𝖽⁒(a0)-1)\centerdotp,

while p′≑𝗋𝖾𝖿𝗅b0. To show f=fβ€², by function extensionality it suffices to show f⁒(x)=f′⁒(x) for all x:Σ⁒A, so we can use the induction principle of suspension. First, we have

f⁒(𝖭)⁒=𝑝⁒b0≑f′⁒(𝖭). (6.5.5)

Second, we have

\includegraphics

HoTT_fig_6.5.1.png

And thirdly, as x varies along 𝗆𝖾𝗋𝗂𝖽⁒(a) we must show that the following diagram of paths commutes (invoking the definition of fβ€²(𝗆𝖾𝗋𝗂𝖽(a))):

\includegraphics

HoTT_fig_6.5.2.png

This is clear. Thus, to show that (f,p)=(fβ€²,pβ€²), it remains only to show that p is identified with pβ€² when transported along this equality f=fβ€². Since the type of p is f⁒(𝖭)=b0, this means essentially that when p is composed on the left with the inversePlanetmathPlanetmathPlanetmath of the equalityΒ (6.5.5), it becomes pβ€². But this is obvious, sinceΒ (6.5.5) is just p itself, while pβ€² is reflexivityMathworldPlanetmath.

On the other side, suppose given (g,q). By passing back and forth we obtain (gβ€²,qβ€²) with

g′⁒(a) =𝗋𝖾𝖿𝗅b0-1⁒\centerdot⁒g⁒(a)⁒\centerdot⁒g⁒(a0)-1⁒\centerdot⁒𝗋𝖾𝖿𝗅b0
=g⁒(a)⁒\centerdot⁒g⁒(a0)-1
=g⁒(a)

using q:g⁒(a0)=𝗋𝖾𝖿𝗅b0 in the last equality. Thus, gβ€²=g by function extensionality, so it remains to show that when transported along this equality q is identified with qβ€². At a0, the induced equality g⁒(a0)=g′⁒(a0) consists essentially of q itself, while the definition of qβ€² 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

𝖬𝖺𝗉*⁒(π•Šn,B)≃𝖬𝖺𝗉*⁒(π•Šn-1,Ω⁒B)≃⋯≃𝖬𝖺𝗉*⁒(𝟐,Ξ©n⁒B)≃Ω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).

Title 6.5 Suspensions
\metatable