Lemma 1.15: every loop is homotopic to a product of loops each in a single $A_\alpha$

Read-back: Hatcher.loop_homotopic_prod_of_cover

Setting and binders. Let $X$ be a type (in an arbitrary universe) equipped with a topology; no separation, compactness, or other axiom is assumed. Let $\iota$ be an arbitrary type (any universe, possibly empty, possibly infinite), and let $A : \iota \to \mathcal P(X)$ assign to each index $\alpha$ a subset $A_\alpha \subseteq X$. Let $x_0 \in X$ be a point. The theorem takes the following hypotheses, every one of which is assumed (whether or not it is used in the conclusion):

• $(\mathrm{hx}_0)$ for every $\alpha \in \iota$, $x_0 \in A_\alpha$;
• $(\mathrm{hopen})$ for every $\alpha \in \iota$, $A_\alpha$ is an open subset of $X$;
• $(\mathrm{hpc})$ for every $\alpha \in \iota$, $A_\alpha$ is path-connected in the following exact sense: there exists a point $x \in A_\alpha$ such that for every $y \in A_\alpha$ there is a continuous map $\gamma : [0,1] \to X$ with $\gamma(0) = x$, $\gamma(1) = y$, and $\gamma(t) \in A_\alpha$ for all $t \in [0,1]$ (the distinguished point $x$ is not required to be $x_0$; the condition in particular forces $A_\alpha \neq \varnothing$);
• $(\mathrm{hcover})$ $\bigcup_{\alpha \in \iota} A_\alpha = X$ (equality of sets, i.e. the $A_\alpha$ cover $X$);
• $(\mathrm{hinter})$ for every ordered pair $\alpha, \beta \in \iota$ — including $\alpha = \beta$, in which case this just says $A_\alpha$ is path-connected again — the intersection $A_\alpha \cap A_\beta$ is path-connected in the same sense as above (some point of $A_\alpha \cap A_\beta$ is joined to every point of $A_\alpha \cap A_\beta$ by a path whose whole image lies in $A_\alpha \cap A_\beta$);
• $f$ is a loop in $X$ at $x_0$: a continuous map $f : [0,1] \to X$ with $f(0) = x_0$ and $f(1) = x_0$.

Nothing here requires $\iota$ to be nonempty, finite, or to have any structure; nothing requires the $A_\alpha$ to be distinct, and nothing relates the topology on $A_\alpha$ to anything other than the subspace topology inherited from $X$.

The custom notions, unfolded.

• For $\alpha \in \iota$, the base point in $A_\alpha$, written here $\hat x_0^{\alpha}$, is the point $x_0$ regarded as an element of the subspace $A_\alpha$ (with the subspace topology), using $(\mathrm{hx}_0)$ to know $x_0 \in A_\alpha$. Under the inclusion $A_\alpha \hookrightarrow X$ it maps to $x_0$.
• A loop in $A_\alpha$ at $\hat x_0^\alpha$ is a continuous map $g : [0,1] \to A_\alpha$ (into the subspace, so continuity is with respect to the subspace topology) with $g(0) = g(1) = \hat x_0^\alpha$.
• For such a $g$, the loop pushed into $X$, written $\iota_\alpha(g)$, is the composite $[0,1] \xrightarrow{g} A_\alpha \hookrightarrow X$, i.e. $t \mapsto g(t)$ viewed in $X$. It is a loop in $X$ at $x_0$ whose image is contained in $A_\alpha$.
• For two paths $\gamma$ from $a$ to $b$ and $\gamma'$ from $b$ to $c$ in $X$, the concatenation $\gamma \cdot \gamma'$ is the path from $a$ to $c$ given by

$$(\gamma \cdot \gamma')(t) \;=\; \begin{cases} \gamma(2t) & \text{if } t \le \tfrac12,\\[2pt] \gamma'(2t-1) & \text{if } t > \tfrac12, \end{cases}\qquad t \in [0,1].$$

• The constant loop $c_{x_0}$ is $t \mapsto x_0$ for all $t \in [0,1]$.
• For a finite list $[p_1, p_2, \dots, p_n]$ of loops in $X$ at $x_0$ ($n \ge 0$), the loop product $\Pi[p_1,\dots,p_n]$ is the right-nested concatenation ending in the constant loop:

$$\Pi[p_1,\dots,p_n] \;=\; p_1 \cdot \bigl(p_2 \cdot (\cdots \cdot (p_n \cdot c_{x_0})\cdots)\bigr),$$

so that, concretely, $p_1$ is traversed on $[0,\tfrac12]$, $p_2$ on $[\tfrac12,\tfrac34]$, …, $p_k$ on $[1-2^{-(k-1)},\,1-2^{-k}]$, and the loop is constantly $x_0$ on $[1-2^{-n},1]$. In particular $\Pi[\,] = c_{x_0}$ (the empty list gives the constant loop), and $\Pi[p] = p \cdot c_{x_0}$, which is $p$ run at double speed on $[0,\tfrac12]$ followed by standing still at $x_0$ on $[\tfrac12,1]$ — not $p$ itself.

• Two loops $p, q$ in $X$ at $x_0$ are homotopic (relative to endpoints), written $p \simeq q$, when there exists a continuous map $H : [0,1]\times[0,1] \to X$ (product topology) with $H(0,s) = p(s)$ and $H(1,s) = q(s)$ for all $s$, and such that for every $t \in [0,1]$ one has $H(t,0) = p(0) = x_0$ and $H(t,1) = p(1) = x_0$.

Conclusion. Under all of the hypotheses above, there exists a finite list

$$\ell \;=\; \bigl[(\alpha_1, g_1),\, (\alpha_2, g_2),\, \dots,\, (\alpha_n, g_n)\bigr], \qquad n \ge 0,$$

of pairs in which each $\alpha_k \in \iota$ is an index (indices may repeat, and may be in any order) and each $g_k$ is a loop in the subspace $A_{\alpha_k}$ at $\hat x_0^{\alpha_k}$, such that

$$f \;\simeq\; \Pi\bigl[\iota_{\alpha_1}(g_1),\, \iota_{\alpha_2}(g_2),\, \dots,\, \iota_{\alpha_n}(g_n)\bigr] \;=\; \iota_{\alpha_1}(g_1)\cdot\bigl(\iota_{\alpha_2}(g_2)\cdot(\cdots\cdot(\iota_{\alpha_n}(g_n)\cdot c_{x_0})\cdots)\bigr),$$

i.e. $f$ is homotopic relative to endpoints, as a loop in $X$ at $x_0$, to the right-nested concatenation of the pushed-in loops followed by the constant loop. This is a plain existence statement ($\exists$, not $\exists!$): no uniqueness, no bound on $n$, and no condition on the $\alpha_k$ or $g_k$ beyond their types is asserted.

Degenerate and edge cases made explicit.

• The list $\ell$ is allowed to be empty ($n = 0$); in that case the conclusion reads $f \simeq c_{x_0}$, i.e. $f$ is null-homotopic relative to endpoints. The statement does not exclude this witness.
• If $\iota$ is empty, then $(\mathrm{hx}_0)$, $(\mathrm{hopen})$, $(\mathrm{hpc})$, $(\mathrm{hinter})$ hold vacuously, while $(\mathrm{hcover})$ says $\varnothing = X$; since $x_0 \in X$ is also given, the hypotheses are jointly unsatisfiable, and the theorem holds vacuously for empty $\iota$.
• If $\iota$ is nonempty, $(\mathrm{hx}_0)$ already forces every $A_\alpha$ and every $A_\alpha \cap A_\beta$ to be nonempty (they contain $x_0$), so the nonemptiness content of $(\mathrm{hpc})$ and $(\mathrm{hinter})$ is automatic; their remaining content is the path-joining condition.
• $(\mathrm{hopen})$ and $(\mathrm{hcover})$ are hypotheses of the theorem but do not appear in the conclusion; the conclusion mentions only $A$, $x_0$, $(\mathrm{hx}_0)$ (through the base points $\hat x_0^\alpha$), and $f$.
• The loops $g_k$ live in the subspaces $A_{\alpha_k}$; the homotopy $H$ witnessing $f \simeq \Pi[\dots]$ is a homotopy in $X$, with no requirement that it stay inside any $A_\alpha$ or any union of them.