Theorem 1.20 (van Kampen): $\Phi$ is surjective with kernel $N$

Read-back of Hatcher.vanKampen.

Setting and binders. Let $X$ be a topological space (an arbitrary type in an arbitrary universe, equipped with a topology; no separation, compactness, or other axioms are assumed). Let $\iota$ be an arbitrary index type (any universe, any cardinality, possibly empty). Let $A : \iota \to \mathcal{P}(X)$ be a family of subsets $A_\alpha \subseteq X$, and let $x_0 \in X$ be a point. Each subset $A_\alpha$, and each intersection $A_\alpha \cap A_\beta$, is regarded as a topological space with the subspace topology inherited from $X$. The theorem takes the following hypotheses:

• $(\mathrm{hx}_0)$ for every $\alpha \in \iota$, $x_0 \in A_\alpha$;
• $(\mathrm{hopen})$ for every $\alpha \in \iota$, $A_\alpha$ is open in $X$;
• $(\mathrm{hpc})$ for every $\alpha \in \iota$, $A_\alpha$ is path-connected in the following sense: there exists a point $x \in A_\alpha$ such that for every $y \in A_\alpha$ there is a continuous path $\gamma : [0,1] \to X$ with $\gamma(0) = x$, $\gamma(1) = y$, and $\gamma(t) \in A_\alpha$ for all $t$ (this notion in particular requires $A_\alpha \neq \varnothing$, which is already forced by $(\mathrm{hx}_0)$);
• $(\mathrm{hcover})$ $\bigcup_{\alpha \in \iota} A_\alpha = X$;
• $(\mathrm{hinter})$ for every pair $\alpha, \beta \in \iota$ (the case $\alpha = \beta$ is included), $A_\alpha \cap A_\beta$ is path-connected in the same sense;
• $(\mathrm{htriple})$ for every triple $\alpha, \beta, \gamma \in \iota$ (repeated indices included, e.g. $\alpha = \beta = \gamma$ or $\gamma = \beta$), $(A_\alpha \cap A_\beta) \cap A_\gamma$ is path-connected in the same sense.

Degenerate cases: if $\iota = \varnothing$ then $\bigcup_\alpha A_\alpha = \varnothing$, while $x_0 \in X$ witnesses $X \neq \varnothing$, so $(\mathrm{hcover})$ cannot hold; hence the hypotheses are jointly satisfiable only when $\iota$ is nonempty. Because the quantifiers in $(\mathrm{hinter})$ and $(\mathrm{htriple})$ range over all tuples including repeated indices, $(\mathrm{htriple})$ with $\gamma = \beta$ restates $(\mathrm{hinter})$, and $(\mathrm{hinter})$ with $\beta = \alpha$ restates $(\mathrm{hpc})$. No finiteness, countability, or distinctness condition on $\iota$ or on the family is imposed.

Fundamental groups used. For a space $Y$ and point $y \in Y$, $\pi_1(Y, y)$ denotes the fundamental group as defined in Mathlib: its elements are homotopy classes (homotopies fixing both endpoints) of continuous loops $[0,1] \to Y$ based at $y$; the identity is the class of the constant loop; the inverse is the class of the reversed loop; and the product $p \cdot q$ is the class of the concatenation "first traverse $q$, then traverse $p$" (Mathlib's convention $p * q = q.\mathrm{trans}\,p$). The base points used are: in $A_\alpha$, the point $x_0$ regarded as an element of the subspace $A_\alpha$ (this is what the custom basept denotes; its membership witness is $(\mathrm{hx}_0)$ at $\alpha$); in $A_\alpha \cap A_\beta$, the point $x_0$ regarded as an element of that subspace (the custom basept₂). Write

$$G_\alpha := \pi_1(A_\alpha, x_0), \qquad G_{\alpha\beta} := \pi_1(A_\alpha \cap A_\beta, x_0), \qquad G := \pi_1(X, x_0).$$

The homomorphisms. The custom inclHom at $\alpha$ is the group homomorphism

$$i_\alpha : G_\alpha \to G$$

induced by the continuous inclusion $A_\alpha \hookrightarrow X$: it sends the class of a loop $\gamma$ in $A_\alpha$ based at $x_0$ to the class of the same loop regarded as a loop in $X$ (Mathlib's FundamentalGroup.mapOfEq applied to the inclusion and the identity $x_0 = x_0$; the "cast along equality" it performs is along a reflexive equation and changes nothing). Likewise the custom interHomLeft and interHomRight at $(\alpha, \beta)$ are the homomorphisms

$$\lambda_{\alpha\beta} : G_{\alpha\beta} \to G_\alpha, \qquad \rho_{\alpha\beta} : G_{\alpha\beta} \to G_\beta$$

induced respectively by the inclusions $A_\alpha \cap A_\beta \hookrightarrow A_\alpha$ and $A_\alpha \cap A_\beta \hookrightarrow A_\beta$ (each sends the class of a loop in the intersection to the class of the same loop viewed in the larger subspace).

The free product. The custom FreeProd is

$$F := \mathop{\ast}_{\alpha \in \iota} G_\alpha,$$

Mathlib's Monoid.CoprodI of the family $(G_\alpha)_{\alpha}$: the quotient of the free monoid on the alphabet $\{(\alpha, g) : \alpha \in \iota,\ g \in G_\alpha\}$ by the congruence generated by the relations $(\alpha, 1) \sim \text{(empty word)}$ and $(\alpha, g)(\alpha, h) \sim (\alpha, gh)$. Since every $G_\alpha$ is a group, $F$ is a group (the coproduct of the $G_\alpha$ in the category of groups). For $g \in G_\alpha$, Monoid.CoprodI.of $g$ denotes the image of the one-letter word $(\alpha, g)$ in $F$; write it $\jmath_\alpha(g) \in F$, so $\jmath_\alpha : G_\alpha \to F$ is the canonical homomorphism from the $\alpha$-th factor.

The custom vanKampenHom is the homomorphism

$$\Phi : F \to G$$

obtained by Mathlib's Monoid.CoprodI.lift from the family $(i_\alpha)_\alpha$: it is the unique group homomorphism $F \to G$ satisfying $\Phi(\jmath_\alpha(g)) = i_\alpha(g)$ for all $\alpha \in \iota$ and $g \in G_\alpha$; concretely, a word $(\alpha_1, g_1)(\alpha_2, g_2)\cdots(\alpha_n, g_n)$ is sent to the product $i_{\alpha_1}(g_1)\, i_{\alpha_2}(g_2) \cdots i_{\alpha_n}(g_n)$ in $G$ (with the product convention for $G$ stated above).

The relators and the normal subgroup. The custom vanKampenRelators is the subset

$$R := \bigl\{\, \jmath_\alpha(\lambda_{\alpha\beta}(\omega)) \cdot \jmath_\beta(\rho_{\alpha\beta}(\omega))^{-1} \;:\; \alpha, \beta \in \iota,\ \omega \in G_{\alpha\beta} \,\bigr\} \subseteq F,$$

where the product and inverse are those of the group $F$, and the pairs $(\alpha,\beta)$ range over all pairs including $\alpha = \beta$ (for $\alpha = \beta$ the element is $\jmath_\alpha(\lambda_{\alpha\alpha}(\omega))\,\jmath_\alpha(\rho_{\alpha\alpha}(\omega))^{-1}$, where $\lambda_{\alpha\alpha}$ and $\rho_{\alpha\alpha}$ are both induced by the inclusion $A_\alpha \cap A_\alpha \hookrightarrow A_\alpha$). The custom vanKampenNormal is

$$N := \text{the normal closure of } R \text{ in } F,$$

which Mathlib defines as the subgroup of $F$ generated by the set of all conjugates $\{\, c\, r\, c^{-1} : r \in R,\ c \in F \,\}$; equivalently, the smallest normal subgroup of $F$ containing $R$.

The conclusion. Under all the hypotheses above, the theorem asserts the conjunction of the following two statements:

1. $\Phi$ is surjective: for every $h \in G = \pi_1(X, x_0)$ there exists some $w \in F$ with $\Phi(w) = h$.

2. The kernel of $\Phi$ equals $N$ as subgroups of $F$:

$$\ker \Phi \;=\; N, \qquad\text{where } \ker \Phi = \{\, w \in F : \Phi(w) = 1 \,\}.$$

This is an equality of subgroups (both inclusions): every $w \in F$ with $\Phi(w) = 1$ lies in the normal closure $N$ of $R$, and every element of $N$ is sent by $\Phi$ to the identity of $\pi_1(X, x_0)$.

Taken together, the two conjuncts say exactly that $\Phi$ induces a group isomorphism $F / N \cong \pi_1(X, x_0)$, though the statement itself is phrased as "surjective" and "kernel equals $N$" rather than as an isomorphism. Nothing is asserted about the case where any hypothesis fails, and no statement is made about base points other than the single common point $x_0$.