Theorem 1.20 (first part): $\Phi:\ast_\alpha\pi_1(A_\alpha)\to\pi_1(X)$ is surjective

Read-back: Hatcher.vanKampenHom_surjective

Setting and binders. Let $X$ be an arbitrary topological space (no separation, compactness, or other axioms are assumed) and let $\iota$ be an arbitrary index type (it may be finite, infinite, or empty). The data of the theorem are:

• a family of subsets $A_\alpha \subseteq X$, one for each $\alpha \in \iota$;
• a point $x_0 \in X$;
• a proof $h_{x_0}$ that $x_0 \in A_\alpha$ for every $\alpha \in \iota$.

Each $A_\alpha$ is regarded as a topological space with the subspace topology inherited from $X$, and $x_0$, viewed as a point of $A_\alpha$ (this is what the auxiliary definition basept produces: the pair "$x_0$ together with the proof $x_0 \in A_\alpha$"), serves as the basepoint of $A_\alpha$. Because the hypothesis $h_{x_0}$ is required for every $\alpha$, the case in which some $A_\alpha$ does not contain $x_0$ is excluded.

Hypotheses. In addition to $h_{x_0}$, the theorem assumes all of the following:

1. (hopen) For every $\alpha \in \iota$, the set $A_\alpha$ is open in $X$.
2. (hpc) For every $\alpha \in \iota$, the set $A_\alpha$ is path-connected in the following exact sense: there exists a point $a \in A_\alpha$ such that for every $y \in A_\alpha$ there is a continuous map $\gamma : [0,1] \to X$ with $\gamma(0) = a$, $\gamma(1) = y$, and $\gamma(t) \in A_\alpha$ for all $t \in [0,1]$. (In particular this forces $A_\alpha \neq \emptyset$, which is already guaranteed by $x_0 \in A_\alpha$.)
3. (hcover) The union $\bigcup_{\alpha \in \iota} A_\alpha$ equals the whole space $X$.
4. (hinter) For every ordered pair $(\alpha, \beta) \in \iota \times \iota$ — including the diagonal pairs $\alpha = \beta$, for which the condition reduces to hypothesis 2 — the intersection $A_\alpha \cap A_\beta$ is path-connected in the same sense as in item 2: there exists $a \in A_\alpha \cap A_\beta$ joined to every point of $A_\alpha \cap A_\beta$ by a path staying inside $A_\alpha \cap A_\beta$. (Since $x_0 \in A_\alpha \cap A_\beta$, these intersections are all nonempty.) No hypothesis is stated about intersections of three or more of the sets.

Edge case. If $\iota$ is empty, then $\bigcup_{\alpha} A_\alpha = \emptyset$, whereas $X$ contains the point $x_0$, so hypothesis 3 cannot hold; the hypotheses are jointly unsatisfiable in that case and the theorem says nothing. For nonempty $\iota$ the hypotheses are consistent (e.g. a single set $A_\alpha = X$ when $X$ is path-connected).

The objects in the conclusion. The conclusion is a statement about a specific group homomorphism, built as follows.

• For a topological space $Y$ and a point $y \in Y$, the fundamental group $\pi_1(Y, y)$ used here is the group of endomorphisms of the object $y$ in the fundamental groupoid of $Y$. Concretely, its elements are equivalence classes of loops at $y$ — continuous maps $\gamma : [0,1] \to Y$ with $\gamma(0) = \gamma(1) = y$ — under homotopy relative to the endpoints $\{0,1\}$; the identity is the class of the constant loop; and the product $a \cdot b$ of two classes is the class of the concatenation "first $b$, then $a$" (the endomorphism-monoid convention $a \cdot b = b \gg a$, where $\gg$ denotes concatenation in the order written). Inverses are given by reversing loops.

• For each $\alpha \in \iota$, the homomorphism

$$j_\alpha : \pi_1(A_\alpha, x_0) \longrightarrow \pi_1(X, x_0)$$

(the definition inclHom) is the homomorphism induced, via the general "map of fundamental groups along a continuous map with a specified equation on basepoints", by the inclusion map $A_\alpha \hookrightarrow X$, $a \mapsto a$, together with the (definitionally trivial) fact that the inclusion sends the basepoint $x_0 \in A_\alpha$ to $x_0 \in X$. On representatives, $j_\alpha$ sends the class of a loop $\gamma$ in $A_\alpha$ to the class of the same loop regarded as a loop in $X$ (after a basepoint-recasting along the trivial equation $x_0 = x_0$).

• The group $F$ (the definition FreeProd) is

$$F \;=\; \mathop{\ast}_{\alpha \in \iota} \pi_1(A_\alpha, x_0),$$

the free product of the family of groups $\pi_1(A_\alpha, x_0)$, $\alpha \in \iota$, in Mathlib's sense: the quotient of the free monoid on the disjoint union $\coprod_{\alpha} \pi_1(A_\alpha, x_0)$ of the underlying sets by the monoid congruence generated by the relations "$(\alpha, 1) \sim$ empty word" and "$(\alpha, g)\,(\alpha, g') \sim (\alpha, g g')$" for all $\alpha$ and $g, g' \in \pi_1(A_\alpha, x_0)$. It carries the group structure whose inverse reverses a word and inverts each letter. Each $\pi_1(A_\alpha, x_0)$ maps into $F$ by the canonical inclusion $\mathrm{of}_\alpha$ sending $g$ to the one-letter word $(\alpha, g)$. When $\iota$ is empty, $F$ is the trivial group.

• The homomorphism

$$\Phi : F \longrightarrow \pi_1(X, x_0)$$

(the definition vanKampenHom) is the unique monoid homomorphism obtained from the family $(j_\alpha)_{\alpha \in \iota}$ by the universal property of the free product, i.e. the unique homomorphism with $\Phi(\mathrm{of}_\alpha(g)) = j_\alpha(g)$ for all $\alpha \in \iota$ and all $g \in \pi_1(A_\alpha, x_0)$. On a general word $(\alpha_1, g_1)(\alpha_2, g_2)\cdots(\alpha_n, g_n)$ it takes the value $j_{\alpha_1}(g_1)\, j_{\alpha_2}(g_2) \cdots j_{\alpha_n}(g_n)$ in $\pi_1(X, x_0)$, and it sends the empty word to the identity. Note that $\Phi$ depends only on the data $A$, $x_0$, $h_{x_0}$; none of the hypotheses 1–4 enters its construction.

Conclusion. The theorem asserts that $\Phi$ is surjective in the literal sense:

$$\forall\, c \in \pi_1(X, x_0),\ \exists\, w \in F \text{ such that } \Phi(w) = c.$$

That is: every homotopy class of loops in $X$ based at $x_0$ is equal to $\Phi(w)$ for some element $w$ of the free product of the groups $\pi_1(A_\alpha, x_0)$; equivalently, every such class can be written as a finite product $j_{\alpha_1}(g_1)\cdots j_{\alpha_n}(g_n)$ (with $n \ge 0$) of images of classes of loops based at $x_0$ lying in single sets $A_{\alpha_k}$. Nothing is asserted about the kernel of $\Phi$, about injectivity, or about any relations among the $j_\alpha$; the statement is purely the existence of a preimage for each element of $\pi_1(X, x_0)$.

Hypothesis usage. Hypotheses 1 (openness), 2 (path-connectedness of each $A_\alpha$), 3 (covering), and 4 (path-connectedness of each pairwise intersection) appear only as assumptions; the conclusion's statement does not mention them, and they would be available only to a proof. The hypothesis $h_{x_0}$ is used in forming the basepoints and hence in the very statement of the conclusion.