Synthetic Homotopy Theory, Encode-Decode, and the Freudenthal¶
Job: develop the encode-decode (\(\pi_1(S^1)=\mathbb{Z}\)), the Freudenthal / Blakers–Massey, the fiber sequences / long exact, and the Eilenberg–MacLane / cohomology — with the \(\pi_1(S^1)\) / Freudenthal as the worked example.
Core¶
The encode-decode and \(\pi_1(S^1)\)¶
| Encode-decode / \(\pi_1\) / \(C:S^1\to\mathcal{U}\) | Description |
|---|---|
| Encode-decode | \(\pi_1(S^1)=\mathbb{Z}\) via \(C:S^1\to\mathcal{U}\), \(C(\mathsf{base})=\mathbb{Z}\), transport around \(\mathsf{loop}=\) succ (the foundations) |
| Winding | \(\mathbb{Z}\) the winding number (the foundations) |
The Freudenthal and the Blakers–Massey¶
| Freudenthal / \(\pi_{n+k}\) / Blakers–Massey | Description |
|---|---|
| Freudenthal | \(\pi_{n+k}(S^n)\) the suspension, \(\pi_{n+k}(\Sigma X)\) (the foundations) |
| Blakers–Massey | the connectivity: \(\pi_{i+j-1}(X\times_B Y)\to\pi_{i+j-1}(\Sigma\Omega B)\) (the foundations) |
The fiber sequences and the long exact¶
| Fiber / \(F\to E\to B\) / long exact | Description |
|---|---|
| Fiber sequence | \(F\to E\to B\), \(\Omega B\to F\) (the foundations) |
| Long exact | \(\pi_n(F)\to\pi_n(E)\to\pi_n(B)\to\pi_{n-1}(F)\) (the foundations) |
The Eilenberg–MacLane and the cohomology¶
| \(K(G,n)\) / HIT / \(H^n\) | Description |
|---|---|
| Eilenberg–MacLane \(K(G,n)\) | the HIT (the foundations) |
| Cohomology | \(H^n(X;G)=[X,K(G,n)]\) the synthetic (the foundations) |
See it¶
\(\pi_1(S^1)=\mathbb{Z}\) via encode-decode and the Freudenthal suspension. The encode-decode: the \(C:S^1\to\mathcal{U}\) the \(C(\mathsf{base})=\mathbb{Z}\), the \(\mathsf{encode}:(\mathsf{base}=x)\to C(x)\) by transport, the \(\mathsf{decode}:\mathbb{Z}\to\Omega S^1\) by iterating \(\mathsf{loop}\) (the foundations). The Freudenthal: the \(\pi_{n+k}(S^n)\) the suspension (the \(\Sigma\), the foundations). The key point: the \(\pi_1(S^1)=\mathbb{Z}\) the encode-decode, the Freudenthal the \(\pi_{n+k}\).
Check¶
Show that \(\pi_1(S^1)=\mathbb{Z}\) via the encode-decode method.
The \(C:S^1\to\mathcal{U}\): the \(C(\mathsf{base})=\mathbb{Z}\), the transport around \(\mathsf{loop}\) = successor (the \(\mathsf{loop}_*:C(\mathsf{base})\to C(\mathsf{base})\), \(n\mapsto n+1\)). The \(\mathsf{encode}:(\mathsf{base}=x)\to C(x)\) by transport (the \(p:\mathsf{base}=x\), the \(p_*:C(\mathsf{base})\to C(x)\), \(n\mapsto p_*(n)\)). The \(\mathsf{decode}:C(\mathsf{base})=\mathbb{Z}\to\Omega S^1=\mathsf{base}=\mathsf{base}\) by iterating \(\mathsf{loop}\) (\(n\mapsto\mathsf{loop}^n\)). The \(\mathsf{encode}\circ\mathsf{decode}=\mathrm{id}\) and \(\mathsf{decode}\circ\mathsf{encode}=\mathrm{id}\) (the encode-decode, the foundations). So the \(\pi_1(S^1)=\mathbb{Z}\).
Explain the Freudenthal suspension theorem and the Blakers–Massey.
The Freudenthal: the \(\pi_{n+k}(S^n)\) the suspension (the \(\Sigma X\), the \(\pi_{n+k}(\Sigma X)\cong\pi_{n+k-1}(X)\) for \(k\le n-2\), the stable range, the foundations). The Blakers–Massey: the \(X\times_B Y\to\Sigma\Omega B\) the connectivity (the \(i\)-conn \(+\) \(j\)-conn \(\Rightarrow\) \((i+j-1)\)-conn, the foundations). The fiber sequence: the \(F\to E\to B\) the \(\Omega B\to F\), the \(\pi_n(F)\to\pi_n(E)\to\pi_n(B)\to\pi_{n-1}(F)\) (the foundations). So the Freudenthal the suspension, the Blakers–Massey the connectivity.
Pitfalls¶
- The encode-decode the transport (\(C:S^1\to\mathcal{U}\), the foundations) — the encode-decode the transport, the \(\mathbb{Z}\) the winding.
- The Freudenthal the stable range (\(k\le n-2\), the foundations) — the Freudenthal the stable, the non-stable the open.
- The fiber sequence the long exact (\(\pi_n(F)\to\pi_n(E)\to\pi_n(B)\to\pi_{n-1}(F)\), the foundations) — the fiber the long exact, the foundations.
- The \(K(G,n)\) the HIT (the foundations) — the \(K(G,n)\) the synthetic, the \(H^n=[X,K(G,n)]\) the cohomology.
Refs¶
- HoTT Book, §8; the encode-decode / the Freudenthal / the Blakers–Massey
- Rijke, Introduction to Homotopy Type Theory (2022); the synthetic homotopy
- Licata–Finster, "Eilenberg–MacLane spaces in homotopy type theory" (2014); the \(K(G,n)\)
- Brunerie, On the homotopy groups of spheres (2016); the synthetic \(\pi_n(S^n)\)
Next¶
HoTT index · Foundations · Cubical & Computational · Models & Semantics · Univalent Categories · Topology