Homotopy theory · The Lumenary

MotivationH

A map that cannot be undone

In 1931 Heinz Hopf wrote down a map $h : S^3 \to S^2$ and proved that it cannot be deformed to a constant map. This was a surprise. Homology sees nothing: $H_3(S^2) = 0$ , so every map $S^3 \to S^2$ induces zero on $H_3$ . Yet Hopf's map is essential, and the reason is geometric: the preimages of any two points of $S^2$ are two circles in $S^3$ that are linked, like two rings of a chain.

Homotopy theory studies spaces and maps up to continuous deformation. Its basic invariants, the homotopy groups $\pi_n(X)$ , are defined just like the fundamental group, with $n$ -spheres in place of loops. They are easy to define and fiendishly hard to compute — not even the homotopy groups of spheres are known in general:

$\pi_{n+k}(S^n)$	$n = 1$	$n = 2$	$n = 3$	$n = 4$	$n = 5$	$n \ge 6$
$k = 0$	$\Z$	$\Z$	$\Z$	$\Z$	$\Z$	$\Z$
$k = 1$	$0$	$\Z$	$\Z/2$	$\Z/2$	$\Z/2$	$\Z/2$
$k = 2$	$0$	$\Z/2$	$\Z/2$	$\Z/2$	$\Z/2$	$\Z/2$
$k = 3$	$0$	$\Z/2$	$\Z/12$	$\Z \oplus \Z/12$	$\Z/24$	$\Z/24$

(Toda, 1962.) This lesson develops the tools that produce such tables: fibrations and their long exact sequences, the Hopf fibration, and the theorems of Hurewicz, Whitehead and Freudenthal that connect homotopy to homology and stabilise it. It assumes the fundamental group and covering spaces and algebraic topology (homology and CW complexes).

IntuitionH

Room to move

An element of $\pi_n(X, x_0)$ is a map from the cube $I^n$ to $X$ sending the whole boundary to the base point — an $n$ -dimensional "balloon" pinned at $x_0$ — up to deformation. Two such maps are added by placing their cubes side by side along the first coordinate and squashing. For $n = 1$ this is concatenation of loops, which is not commutative in general.

For $n \ge 2$ there is room to move. Shrink $f$ into the bottom-left corner and $g$ into the top-right corner (the rest of the cube goes to $x_0$ ), slide them past each other, and expand again: $f + g$ becomes $g + f$ .

Why π₂ is abelian. The sum f + g (left) is deformed by shrinking each map into a smaller square, sliding the squares past each other through the region that maps to the base point, and expanding again, giving g + f (right).

The second idea is that homotopy groups behave well for fibrations — maps $p : E \to B$ that look, up to homotopy, like projections of a product, though they may be globally twisted. A fibration with fibre $F$ gives a long exact sequence linking $\pi_\bullet(F)$ , $\pi_\bullet(E)$ and $\pi_\bullet(B)$ . Covering spaces are fibrations with discrete fibres; the Hopf map is a fibration with fibre $S^1$ , and its exact sequence computes $\pi_3(S^2)$ .

DefinitionsH

Definitions

Spaces have base points, maps preserve them, and homotopies fix them; $[X, Y]_*$ denotes based homotopy classes of based maps.

Definition— homotopy groups

For $n \ge 0$ , $\pi_n(X, x_0)$ is the set of homotopy classes of maps $f : (I^n, \partial I^n) \to (X, x_0)$ , homotopies being through such maps. Equivalently, since $I^n / \partial I^n \cong S^n$ , $\pi_n(X, x_0) = [(S^n, *), (X, x_0)]_*$ . For $n \ge 1$ it is a group under

(f + g)(s_1, \dots, s_n) = \begin{cases} f(2 s_1, s_2, \dots, s_n) & s_1 \le \tfrac12, \\ g(2 s_1 - 1, s_2, \dots, s_n) & s_1 \ge \tfrac12, \end{cases}

with identity the constant map and inverse $f(1 - s_1, s_2, \dots, s_n)$ . $\pi_0(X)$ is the set of path components and $\pi_1$ is the fundamental group. A based map $\varphi : X \to Y$ induces homomorphisms $\varphi_*[f] = [\varphi \circ f]$ .

Definition— n-connected; weak homotopy equivalence

$X$ is $n$ -connected if $\pi_k(X, x_0) = 0$ for $0 \le k \le n$ (so $0$ -connected means path connected and $1$ -connected means simply connected). A map $\varphi : X \to Y$ is a weak homotopy equivalence if it induces bijections $\pi_n(X, x_0) \to \pi_n(Y, \varphi(x_0))$ for all $n \ge 0$ and all base points.

Definition— fibration

A map $p : E \to B$ has the homotopy lifting property for a space $X$ if for every homotopy $G : X \times I \to B$ and every map $\tilde g_0 : X \to E$ with $p \circ \tilde g_0 = G_0$ there is a homotopy $\tilde G : X \times I \to E$ with $p \circ \tilde G = G$ and $\tilde G_0 = \tilde g_0$ . It is a (Hurewicz) fibration if this holds for all spaces $X$ , and a Serre fibration if it holds for all discs $D^n$ (equivalently, all CW complexes). The fibre over $b_0$ is $F = p^{-1}(b_0)$ , and we write $F \to E \to B$ .

Definition— fibre bundle

A fibre bundle with fibre $F$ is a map $p : E \to B$ such that every point of $B$ has a neighbourhood $U$ with a homeomorphism $p^{-1}(U) \cong U \times F$ over $U$ . Every fibre bundle is a Serre fibration (Hatcher, Proposition 4.48), and a fibre bundle over a paracompact base is a Hurewicz fibration (Hurewicz, 1955).

Definition— suspension and loop space

The reduced suspension $\Sigma X$ is $X \times I$ with $X \times \{0, 1\} \cup \{x_0\} \times I$ collapsed to a point; $\Sigma S^n \cong S^{n+1}$ . The loop space $\Omega X$ is the space of based loops in $X$ (compact-open topology). They are adjoint: $[\Sigma X, Y]_* \cong [X, \Omega Y]_*$ , and in particular $\pi_{n+1}(Y) \cong \pi_n(\Omega Y)$ .

Definition— Eilenberg–MacLane space

For a group $G$ and $n \ge 1$ (with $G$ abelian if $n \ge 2$ ), an Eilenberg–MacLane space $K(G, n)$ is a connected CW complex with $\pi_n \cong G$ and $\pi_k = 0$ for $k \neq n$ .

Worked examplesH

Examples

Example— Easy cases

If $X$ is contractible, $\pi_n(X) = 0$ for all $n$ .
$\pi_n(X \times Y, (x_0, y_0)) \cong \pi_n(X, x_0) \times \pi_n(Y, y_0)$ : a map into a product is a pair of maps, and likewise for homotopies.
$\pi_n(S^n) \cong \Z$ for $n \ge 1$ , detected by the degree (proved below via Hurewicz). The identity map generates.
$\pi_k(S^n) = 0$ for $k \lt n$ (Theorem 5).

Example— Spheres are not determined by dimension

Higher homotopy groups do not vanish above the dimension: $\pi_3(S^2) \cong \Z$ (Theorem 7), and Serre showed in the early 1950s that $\pi_k(S^n)$ is non-zero for infinitely many $k$ when $n \ge 2$ . So a $2$ -dimensional CW complex can have non-zero homotopy groups in infinitely many degrees, whereas its homology vanishes above degree $2$ .

Example— Eilenberg–MacLane spaces you know

$K(\Z, 1) = S^1$ : its universal cover $\R$ is contractible, so $\pi_n(S^1) = 0$ for $n \ge 2$ (Corollary 4).
$K(\pi_1(M_g), 1) = M_g$ for a closed orientable surface of genus $g \ge 1$ , whose universal cover is the plane.
$K(\Z/2, 1) = \R P^\infty$ , covered by the contractible sphere $S^\infty$ .
$K(\Z, 2) = \C P^\infty$ , from the fibration $S^1 \to S^\infty \to \C P^\infty$ and the long exact sequence.

ProofH

Homotopy groups and fibrations

Theorem— Theorem 1 (higher homotopy groups are abelian)

For $n \ge 1$ , $\pi_n(X, x_0)$ is a group, and for $n \ge 2$ it is abelian.

Proof

The group axioms are checked exactly as for $\pi_1$ , using reparametrisations in the first coordinate. For $n \ge 2$ define a second operation $+_2$ by concatenating in the second coordinate; write $+_1$ for the first. Both have the constant map $c$ as identity. They satisfy the interchange law

(f +_1 g) +_2 (h +_1 k) = (f +_2 h) +_1 (g +_2 k)

on the nose: both sides are the map on $I^n$ that is $f$ , $g$ , $h$ , $k$ on the four quarters $\{s_1 \le \tfrac12, s_2 \le \tfrac12\}$ , $\{s_1 \ge \tfrac12, s_2 \le \tfrac12\}$ , $\{s_1 \le \tfrac12, s_2 \ge \tfrac12\}$ , $\{s_1 \ge \tfrac12, s_2 \ge \tfrac12\}$ , suitably rescaled. Now the Eckmann–Hilton argument, which uses nothing but the two unit laws and the interchange law (writing $e$ for the common unit $[c]$ ):

a +_1 b = (a +_2 e) +_1 (e +_2 b) = (a +_1 e) +_2 (e +_1 b) = a +_2 b,

a +_1 b = (e +_2 a) +_1 (b +_2 e) = (e +_1 b) +_2 (a +_1 e) = b +_2 a = b +_1 a .

(In general one first shows that the two units agree, by the same trick: $e_1 = e_1 +_1 e_1 = (e_2 +_2 e_1) +_1 (e_1 +_2 e_2) = (e_2 +_1 e_1) +_2 (e_1 +_1 e_2) = e_2 +_2 e_2 = e_2$ .) So the two operations coincide on $\pi_n$ and are commutative.

∎

For $n = 1$ there is only one coordinate, the argument has nothing to work with, and indeed $\pi_1$ of the figure eight is a non-abelian free group.

Theorem— Theorem 2 (covering spaces are fibrations)

A covering map $p : \tilde X \to X$ has the homotopy lifting property for all spaces, with unique lifts.

This is the homotopy lifting theorem for covering spaces from the fundamental group lesson (Hatcher, Proposition 1.30): lift along each slice $\{x\} \times I$ using unique path lifting, and check continuity locally using evenly covered neighbourhoods.

Theorem— Theorem 3 (long exact sequence of a fibration)

Let $p : E \to B$ be a Serre fibration, $b_0 \in B$ , $F = p^{-1}(b_0)$ and $e_0 \in F$ . There is a long exact sequence

\cdots \to \pi_n(F, e_0) \xrightarrow{i_*} \pi_n(E, e_0) \xrightarrow{p_*} \pi_n(B, b_0) \xrightarrow{\partial} \pi_{n-1}(F, e_0) \to \cdots \to \pi_0(F) \to \pi_0(E) \to \pi_0(B),

where the last three terms are only pointed sets and exactness there means that preimages of the base point are images.

Proof

The boundary map. Represent $[f] \in \pi_n(B, b_0)$ by $f : I^n \to B$ with $f(\partial I^n) = b_0$ , and view $I^n = I^{n-1} \times I$ as a homotopy of maps $I^{n-1} \to B$ . Lift it, starting from the constant map $e_0$ on $I^{n-1} \times \{0\}$ and remaining $e_0$ on $\partial I^{n-1} \times I$ ; such relative lifts exist for Serre fibrations, because $(I^{n-1} \times I,\ I^{n-1} \times \{0\} \cup \partial I^{n-1} \times I)$ is homeomorphic to $(I^{n-1} \times I,\ I^{n-1} \times \{0\})$ . The lift $\tilde f$ maps the top face $I^{n-1} \times \{1\}$ into $p^{-1}(b_0) = F$ and its boundary to $e_0$ , and $\partial [f]$ is its class in $\pi_{n-1}(F, e_0)$ . Well-definedness follows by lifting homotopies one dimension higher.

Exactness at $\pi_n(E)$ . First $p_* i_* = 0$ , since $p \circ i$ is constant. Conversely, let $f : (I^n, \partial I^n) \to (E, e_0)$ and suppose $p \circ f$ is null-homotopic through a homotopy $G : I^n \times I \to B$ with $G_0 = p \circ f$ , $G_1 \equiv b_0$ and $G(\partial I^n \times I) = b_0$ . Lift $G$ to $\tilde G$ with $\tilde G_0 = f$ and $\tilde G = e_0$ on $\partial I^n \times I$ . Then $\tilde G_1$ maps $I^n$ into $p^{-1}(b_0) = F$ with boundary at $e_0$ , and $\tilde G$ is a homotopy from $f$ to $\tilde G_1$ through maps of $(I^n, \partial I^n)$ . So $[f] = i_*[\tilde G_1]$ .

Exactness at the other two places is proved by the same lifting technique; equivalently, $p_* : \pi_n(E, F, e_0) \to \pi_n(B, b_0)$ is an isomorphism and the sequence is the long exact sequence of the pair $(E, F)$ (Hatcher, Theorem 4.41).

∎

Theorem— Corollary 4 (covering spaces)

If $p : \tilde X \to X$ is a covering map, then $p_* : \pi_n(\tilde X) \to \pi_n(X)$ is an isomorphism for $n \ge 2$ . In particular $\pi_n(S^1) = 0$ , $\pi_n(T^k) = 0$ for $n \ge 2$ , and $\pi_n(\R P^m) \cong \pi_n(S^m)$ for $n \ge 2$ .

Proof

The fibre is discrete, so $\pi_k(F) = 0$ for $k \ge 1$ , and the exact sequence $0 = \pi_n(F) \to \pi_n(\tilde X) \to \pi_n(X) \to \pi_{n-1}(F) = 0$ (for $n \ge 2$ ) gives the isomorphism. Apply it to $\R \to S^1$ , $\R^k \to T^k$ (contractible covers) and $S^m \to \R P^m$ .

∎

Theorem— Theorem 5 (spheres are highly connected)

$\pi_k(S^n) = 0$ for $0 \le k \lt n$ .

Proof

By the cellular approximation theorem (Hatcher, Theorem 4.8), every map between CW complexes is homotopic to a cellular one, i.e. one sending the $k$ -skeleton into the $k$ -skeleton; the homotopy can be taken relative to a subcomplex on which the map is already cellular, such as the base point. Give $S^k$ and $S^n$ the cell structures $e^0 \cup e^k$ and $e^0 \cup e^n$ . A cellular map $S^k \to S^n$ sends $S^k$ into the $k$ -skeleton of $S^n$ , which for $k \lt n$ is the single point $e^0$ . So every based map $S^k \to S^n$ is based-homotopic to a constant.

∎

ProofH

The Hopf fibration and π₃(S²)

Regard $S^3 = \{ (z, w) \in \C^2 : |z|^2 + |w|^2 = 1 \}$ and $S^2 \subset \C \times \R \cong \R^3$ . The Hopf map is

h(z, w) = \big( 2 z \bar w,\ |z|^2 - |w|^2 \big).

Theorem— Theorem 6 (the Hopf fibration)

$h$ maps $S^3$ onto $S^2$ ; its fibres are exactly the circles $\{ (\lambda z, \lambda w) : |\lambda| = 1 \}$ ; and $h$ is a fibre bundle with fibre $S^1$ . Under stereographic projection $S^2 \setminus \{(0, 1)\} \cong \C$ it is the map $(z, w) \mapsto z / w$ , so $h$ is the quotient map $S^3 \to \C P^1 \cong S^2$ .

Proof

Into $S^2$ : $|2 z \bar w|^2 + (|z|^2 - |w|^2)^2 = 4|z|^2|w|^2 + (|z|^2 - |w|^2)^2 = (|z|^2 + |w|^2)^2 = 1$ .

Constant on circles: $h(\lambda z, \lambda w) = (2 \lambda \bar\lambda z \bar w, |\lambda|^2(|z|^2 - |w|^2)) = h(z, w)$ when $|\lambda| = 1$ .

Fibres are exactly circles: suppose $h(z, w) = h(z', w')$ for two points of $S^3$ . The second coordinates and $|z|^2 + |w|^2 = |z'|^2 + |w'|^2 = 1$ give $|z| = |z'|$ and $|w| = |w'|$ ; the first gives $z \bar w = z' \bar w'$ . Put $\lambda = z' \bar z + w' \bar w$ . Then

\lambda z = z' |z|^2 + w' (z \bar w) = z' |z|^2 + w' z' \bar w' = z' (|z|^2 + |w'|^2) = z' (|z|^2 + |w|^2) = z',

and symmetrically (using $\bar z w = \bar z' w'$ ) $\lambda w = w'$ . Finally $1 = |z'|^2 + |w'|^2 = |\lambda|^2 (|z|^2 + |w|^2) = |\lambda|^2$ .

Stereographic form: projecting from $(0, 1)$ , a point $(v, t)$ goes to $v / (1 - t)$ ; here $1 - t = 1 - |z|^2 + |w|^2 = 2|w|^2$ , so $h(z, w) \mapsto 2 z \bar w / (2 |w|^2) = z / w$ . Onto, and locally trivial: over $U = S^2 \setminus \{(0, 1)\}$ , i.e. where $w \neq 0$ , the map $h^{-1}(U) \to U \times S^1$ , $(z, w) \mapsto (h(z, w), w / |w|)$ , is a homeomorphism with inverse $(q, \mu) \mapsto \mu\,(q, 1)/\sqrt{1 + |q|^2}$ in the stereographic coordinate $q = z / w$ ; this also shows that every $q \in \C$ is hit. Over $S^2 \setminus \{(0, -1)\}$ use $z / |z|$ instead.

∎

Theorem— Theorem 7 (Hopf, 1931)

$\pi_2(S^2) \cong \Z$ , and $\pi_n(S^2) \cong \pi_n(S^3)$ for $n \ge 3$ . In particular $\pi_3(S^2) \cong \Z$ , generated by the class of $h$ .

Proof

The long exact sequence of the fibration $S^1 \to S^3 \xrightarrow{h} S^2$ contains

\pi_n(S^1) \to \pi_n(S^3) \xrightarrow{h_*} \pi_n(S^2) \xrightarrow{\partial} \pi_{n-1}(S^1) .

For $n \ge 3$ both ends vanish by Corollary 4, so $h_*$ is an isomorphism — this is the algebraic lemma bijective_of_exact formalised below. For $n = 2$ the sequence reads $\pi_2(S^3) \to \pi_2(S^2) \to \pi_1(S^1) \to \pi_1(S^3)$ , with outer terms zero by Theorem 5, so $\pi_2(S^2) \cong \pi_1(S^1) \cong \Z$ . Finally $\pi_3(S^3) \cong \Z$ is generated by $[\mathrm{id}]$ (Corollary 9 below), and $h_*[\mathrm{id}] = [h]$ .

∎

The Hopf invariant gives a direct geometric reason. For a smooth map $f : S^3 \to S^2$ , the preimages of two regular values are disjoint closed curves (possibly with several components), and their linking number $H(f)$ does not depend on the choices and is a homotopy invariant; $H : \pi_3(S^2) \to \Z$ is an isomorphism with $H(h) = 1$ (Bott and Tu, §17). The experiment below computes the linking numbers of Hopf fibres numerically. The same construction with quaternions and octonions gives Hopf fibrations $S^3 \to S^7 \to S^4$ and $S^7 \to S^{15} \to S^8$ , and Adams proved (1960) that maps $S^{2n-1} \to S^n$ of Hopf invariant one exist only for $n = 2, 4, 8$ . This gives a homotopy-theoretic proof that finite-dimensional real division algebras exist only in dimensions $1, 2, 4, 8$ (first proved by Kervaire and by Bott and Milnor in 1958; for normed division algebras the result goes back to Hurwitz, 1898).

ProofH

Hurewicz, Whitehead, Freudenthal and Eilenberg–MacLane

These are the structural theorems of the subject. We state them precisely and show how they are used; their proofs occupy Chapter 4 of Hatcher.

Theorem— Theorem 8 (Whitehead, 1949)

A weak homotopy equivalence between connected CW complexes is a homotopy equivalence. More generally, if $\varphi : X \to Y$ is a map of CW complexes inducing isomorphisms on all $\pi_n$ , there is $\psi : Y \to X$ with $\psi\varphi \simeq \mathrm{id}_X$ and $\varphi\psi \simeq \mathrm{id}_Y$ .

The CW hypothesis matters. The Warsaw circle (the closed topologist's sine curve, closed up by an arc) has all homotopy groups trivial, so the map to a point is a weak homotopy equivalence; but it is not contractible (its Čech cohomology detects the "circle").

Theorem— Theorem 9 (Hurewicz, 1935)

Let $X$ be $(n - 1)$ -connected with $n \ge 2$ . Then $\tilde H_k(X) = 0$ for $k \lt n$ , and the Hurewicz map $\pi_n(X) \to H_n(X)$ , $[f] \mapsto f_*(\text{fundamental class of } S^n)$ , is an isomorphism. For $n = 1$ and path-connected $X$ , $\pi_1(X)^{\mathrm{ab}} \cong H_1(X)$ .

Theorem— Corollary 10

(a) $\pi_n(S^n) \cong \Z$ for $n \ge 1$ , generated by the identity; a map $S^n \to S^n$ is classified up to homotopy by its degree. (b) Homology Whitehead theorem: a map between simply connected CW complexes that induces isomorphisms on all homology groups is a homotopy equivalence.

Proof

(a) $S^n$ is $(n - 1)$ -connected by Theorem 5, so $\pi_n(S^n) \cong H_n(S^n) \cong \Z$ by Theorem 9 ( $n \ge 2$ ; for $n = 1$ use $\pi_1(S^1) \cong \Z$ ). The Hurewicz map sends $[f]$ to $\deg(f)$ times the generator. (b) Sketch: make $\varphi$ cellular and replace $Y$ by the mapping cylinder so that $\varphi$ is an inclusion of a subcomplex; then $H_\bullet(Y, X) = 0$ . The relative Hurewicz theorem for the simply connected pair $(Y, X)$ (Hatcher, Theorem 4.32) shows inductively that $\pi_n(Y, X) = 0$ for all $n$ , so $\varphi$ is a weak equivalence by the long exact sequence of the pair, and Theorem 8 applies.

∎

Simple connectivity cannot be dropped in (b): if $\Sigma$ is Poincaré's homology sphere, a degree-one map $\Sigma \to S^3$ (collapse the complement of a small ball) induces isomorphisms on all homology groups, but $\pi_1(\Sigma)$ has order $120$ , so it is not a homotopy equivalence.

Theorem— Theorem 11 (Freudenthal suspension theorem, 1937)

If $X$ is an $(n - 1)$ -connected CW complex, the suspension map $\pi_i(X) \to \pi_{i+1}(\Sigma X)$ is an isomorphism for $i \lt 2n - 1$ and surjective for $i = 2n - 1$ . In particular $\pi_{n+k}(S^n) \to \pi_{n+k+1}(S^{n+1})$ is an isomorphism for $n \gt k + 1$ .

So each column of the table in the motivation stabilises: the stable homotopy groups of spheres $\pi_k^s = \lim_n \pi_{n+k}(S^n)$ begin $\Z, \Z/2, \Z/2, \Z/24, 0, 0, \Z/2, \Z/240$ . For example, $\pi_3(S^2) \cong \Z \to \pi_4(S^3)$ is onto (the case $i = 2n - 1$ with $n = 2$ ), and $\pi_4(S^3) \cong \pi_5(S^4) \cong \dots \cong \Z/2$ , generated by the suspension of the Hopf map, usually called $\eta$ . The stable groups are the subject of stable homotopy theory.

Theorem— Theorem 12 (Eilenberg–MacLane spaces)

For every $n \ge 1$ and group $G$ (abelian if $n \ge 2$ ), a $K(G, n)$ exists and is unique up to homotopy equivalence. For CW complexes $X$ and abelian $G$ , there is a natural bijection $[X, K(G, n)] \cong H^n(X; G)$ , sending $f$ to $f^*(\iota)$ for a fundamental class $\iota \in H^n(K(G, n); G)$ .

Construction: start with a wedge of $n$ -spheres, one for each generator of $G$ , attach $(n+1)$ -cells to impose the relations (this gives $\pi_n \cong G$ by Hurewicz and cellular approximation), then attach cells of dimension $n + 2, n + 3, \dots$ to kill all higher homotopy groups. Uniqueness comes from Whitehead's theorem, and representability is Hatcher, Theorem 4.57. Thus cohomology is a homotopy-theoretic object: the cup product, for instance, is induced by maps $K(G, m) \wedge K(G', n) \to K(G \otimes G', m + n)$ . Dually, every connected CW complex is assembled from Eilenberg–MacLane spaces in a Postnikov tower, glued by cohomology classes ( $k$ -invariants).

Formal mathematicsF

Eckmann–Hilton and the Hopf map in Lean

The Eckmann–Hilton argument of Theorem 1 is proved independently, for any set with two unital operations satisfying the interchange law; the calc blocks are the displayed equations of the proof.

eckmann_hiltonLean 4Proved here from basic factsFormally verified

/-- **Eckmann–Hilton.** If a set carries two binary operations `m₁`, `m₂` with units `e₁`, `e₂`
that satisfy the interchange law `(a ·₂ b) ·₁ (c ·₂ d) = (a ·₁ c) ·₂ (b ·₁ d)`, then the units
agree, the operations agree, and the operation is commutative. For `πₙ` with `n ≥ 2`,
concatenation of cubes in two different coordinate directions gives two such operations. -/
theorem eckmann_hilton {M : Type*} (m₁ m₂ : M → M → M) (e₁ e₂ : M)
    (h₁l : ∀ a, m₁ e₁ a = a) (h₁r : ∀ a, m₁ a e₁ = a)
    (h₂l : ∀ a, m₂ e₂ a = a) (h₂r : ∀ a, m₂ a e₂ = a)
    (interchange : ∀ a b c d, m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
    e₁ = e₂ ∧ (∀ a b, m₁ a b = m₂ a b) ∧ (∀ a b, m₁ a b = m₁ b a) := by
  -- the units agree
  have he : e₁ = e₂ :=
    calc e₁ = m₁ e₁ e₁ := (h₁l e₁).symm
      _ = m₁ (m₂ e₂ e₁) (m₂ e₁ e₂) := by rw [h₂l, h₂r]
      _ = m₂ (m₁ e₂ e₁) (m₁ e₁ e₂) := interchange _ _ _ _
      _ = m₂ e₂ e₂ := by rw [h₁r, h₁l]
      _ = e₂ := h₂l e₂
  -- the operations agree
  have hm : ∀ a b, m₁ a b = m₂ a b := fun a b =>
    calc m₁ a b = m₁ (m₂ a e₂) (m₂ e₂ b) := by rw [h₂r, h₂l]
      _ = m₂ (m₁ a e₂) (m₁ e₂ b) := interchange _ _ _ _
      _ = m₂ a b := by rw [← he, h₁r, h₁l]
  refine ⟨he, hm, fun a b => ?_⟩
  -- and the operation is commutative
  calc m₁ a b = m₁ (m₂ e₂ a) (m₂ b e₂) := by rw [h₂l, h₂r]
    _ = m₂ (m₁ e₂ b) (m₁ a e₂) := interchange _ _ _ _
    _ = m₂ b a := by rw [← he, h₁l, h₁r]
    _ = m₁ b a := (hm b a).symm

Axioms used: No axiomsformal/Lumenary/HomotopyTheory.leanTry it in the Lean web editor

Mathlib defines $\pi_n$ with cubes exactly as in the lesson (HomotopyGroup.Pi n X x, notation π_ n X x), and proves commutativity for $n \ge 2$ by the same Eckmann–Hilton argument (EckmannHilton.commGroup), applied to concatenation in two different cube directions. It also identifies the cube version of $\pi_1$ with the fundamental group, and loops of loops with higher loops:

pi_commLean 4Applies a library theoremFormally verified

/-- **Higher homotopy groups are abelian:** `πₙ₊₂(X, x)` is commutative. This uses Mathlib's
instance `HomotopyGroup.commGroup`, which is built with `EckmannHilton.commGroup` from the
interchange law for concatenation in two different cube directions. -/
theorem pi_comm (n : ℕ) (X : Type*) [TopologicalSpace X] (x : X)
    (a b : π_ (n + 2) X x) : a * b = b * a :=
  mul_comm a b