8.9 A general statement of the encode-decode method

We have used the encode-decode method to characterize the path spaces of various types, including coproductsMathworldPlanetmath (\crefthm:path-coprod), natural numbersMathworldPlanetmath (\crefthm:path-nat), truncations (\crefthm:path-truncation), the circle (\crefcor:omega-s1), suspensionsMathworldPlanetmath (\autorefthm:freudenthal), and pushouts (\crefthm:van-Kampen). Variants of this technique are used in the proofs of many of the other theorems mentioned in the introduction to this chapter, such as a direct proof of Ο€n⁒(π•Šn), the Blakers–Massey theorem, and the construction of Eilenberg–Mac Lane spaces. While it is tempting to try to abstract the method into a lemma, this is difficult because slightly different variants are needed for different problems. For example, different variations on the same method can be used to characterize a loop spaceMathworldPlanetmath (as in \crefthm:path-coprod,cor:omega-s1) or a whole path space (as in \crefthm:path-nat), to give a completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath characterization of a loop space (e.g.Β Ξ©1⁒(π•Š1)) or only to characterize some truncation of it (e.g.Β van Kampen), and to calculate homotopy groupsMathworldPlanetmath or to prove that a map is n-connected (e.g.Β Freudenthal and Blakers–Massey).

However, we can state lemmas for specific variants of the method. The proofs of these lemmas are almost trivial; the main point is to clarify the method by stating them in generality. The simplest case is using an encode-decode method to characterize the loop space of a type, as in \crefthm:path-coprod and \crefcor:omega-s1.

Lemma 8.9.1 (Encode-decode for Loop Spaces).

Given a pointed type (A,a0) and a fibrationMathworldPlanetmath code:A→U, if

  1. 1.


  2. 2.


  3. 3.

    for all c:π–Όπ—ˆπ–½π–Ύβ’(a0), π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—π–Όπ—ˆπ–½π–Ύβ’(π–½π–Ύπ–Όπ—ˆπ–½π–Ύβ’(c),c0)=c, and

  4. 4.


then (a0=a0) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to code⁒(a0).


Define π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ:∏(x:A)(a0=x)β†’π–Όπ—ˆπ–½π–Ύ(x) by


We show that π–Ύπ—‡π–Όπ—ˆπ–½π–Ύa0 and π–½π–Ύπ–Όπ—ˆπ–½π–Ύa0 are quasi-inverses. The composition π–Ύπ—‡π–Όπ—ˆπ–½π–Ύa0βˆ˜π–½π–Ύπ–Όπ—ˆπ–½π–Ύa0 is immediate by assumptionPlanetmathPlanetmathΒ 3. For the other composition, we show


By path inductionMathworldPlanetmath, it suffices to show π–½π–Ύπ–Όπ—ˆπ–½π–Ύa0⁒(π–Ύπ—‡π–Όπ—ˆπ–½π–Ύao⁒𝗋𝖾𝖿𝗅)=𝗋𝖾𝖿𝗅. After reducing the π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—, it suffices to show π–½π–Ύπ–Όπ—ˆπ–½π–Ύa0⁒(c0)=𝗋𝖾𝖿𝗅, which is assumptionΒ 4. ∎

If a fiberwise equivalence between (a0=–) and π–Όπ—ˆπ–½π–Ύ is desired, it suffices to strengthen condition (iii) to


However, to calculate a loop space (e.g. Ω⁒(π•Š1)), this stronger assumption is not necessary.

Another variation, which comes up often when calculating homotopy groups, characterizes the truncation of a loop space:

Lemma 8.9.2 (Encode-decode for Truncations of Loop Spaces).

Assume a pointed type (A,a0) and a fibration code:Aβ†’U, where for every x, code⁒(x) is a k-type. Define


by truncation recursion (using the fact that code⁒(x) is a k-type), mapping α:a0=x to transportcode⁒(α,c0). Suppose:

  1. 1.


  2. 2.


  3. 3.

    π–Ύπ—‡π–Όπ—ˆπ–½π–Ύa0⁒(π–½π–Ύπ–Όπ—ˆπ–½π–Ύa⁒0⁒(c))=c for all c:π–Όπ—ˆπ–½π–Ύβ’(a0), and

  4. 4.


Then βˆ₯a0=a0βˆ₯k is equivalent to code⁒(a0).


That π–½π–Ύπ–Όπ—ˆπ–½π–Ύβˆ˜π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ is identityPlanetmathPlanetmath is immediate by 3. To prove π–Ύπ—‡π–Όπ—ˆπ–½π–Ύβˆ˜π–½π–Ύπ–Όπ—ˆπ–½π–Ύ, we first do a truncation induction, by which it suffices to show


The truncation induction is allowed because paths in a k-type are a k-type. To show this type, we do a path induction, and after reducing the π–Ύπ—‡π–Όπ—ˆπ–½π–Ύ, use assumptionΒ 4. ∎

Title 8.9 A general statement of the encode-decode method