Theorem 1.20 (second part): $\ker\Phi\subseteq N$

Declaration Hatcher.ker_vanKampenHom_le. 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) and let $\iota$ be an arbitrary index type (possibly empty, possibly infinite, no decidable equality assumed). The following data and hypotheses are given:

• a family of subsets $A_\alpha \subseteq X$ indexed by $\alpha \in \iota$;
• a point $x_0 \in X$;
• $h_{x_0}$: for every $\alpha \in \iota$, $x_0 \in A_\alpha$;
• $h_{\mathrm{open}}$: for every $\alpha$, $A_\alpha$ is open in $X$;
• $h_{\mathrm{pc}}$: for every $\alpha$, $A_\alpha$ is path-connected, where "a set $F \subseteq X$ is path-connected" means (Mathlib's IsPathConnected): there exists a point $x \in F$ such that for every $y \in F$ there is a continuous path $\gamma : [0,1] \to X$ with $\gamma(0)=x$, $\gamma(1)=y$ and $\gamma(t) \in F$ for all $t$ (in particular $F$ is nonempty);
• $h_{\mathrm{cover}}$: $\bigcup_{\alpha \in \iota} A_\alpha = X$ (equality with the whole space, as sets);
• $h_{\mathrm{inter}}$: for every pair $\alpha, \beta \in \iota$ (including $\alpha = \beta$), the set $A_\alpha \cap A_\beta$ is path-connected in the above sense;
• $h_{\mathrm{triple}}$: for every triple $\alpha, \beta, \gamma \in \iota$ (coincidences allowed), the set $(A_\alpha \cap A_\beta) \cap A_\gamma$ is path-connected in the above sense.

Objects built from these data (all custom definitions, unfolded). For each $\alpha$, the space $A_\alpha$ is regarded as a topological space with the subspace topology, and its basepoint is $\mathrm{basept}_\alpha := x_0$ viewed as an element of $A_\alpha$ (via $h_{x_0}$). Likewise $A_\alpha \cap A_\beta$ carries the subspace topology with basepoint $\mathrm{basept}_{\alpha\beta} := x_0$ viewed as an element of $A_\alpha \cap A_\beta$. For a space $Y$ with point $y$, $\pi_1(Y,y)$ denotes Mathlib's FundamentalGroup Y y: its elements are equivalence classes of continuous loops $[0,1] \to Y$ based at $y$, two loops being identified iff they are homotopic through loops based at $y$ (homotopy relative to the endpoints); the group identity is the class of the constant loop, the inverse is path reversal, and the product is defined so that $p \cdot q$ is the class of "$q$ traversed first, then $p$" (i.e. $p \cdot q = q \ast p$ in concatenation order). Given a continuous map $f : Y \to Z$ with $f(y) = z$, Mathlib's FundamentalGroup.mapOfEq is the group homomorphism $\pi_1(Y,y) \to \pi_1(Z,z)$ sending the class of a loop $\gamma$ to the class of $f \circ \gamma$ (with the basepoint identification $f(y)=z$; here every such identification is a definitional equality). With this:

• $\mathrm{inclHom}_\alpha : \pi_1(A_\alpha, x_0) \to \pi_1(X, x_0)$ is the homomorphism induced by the subspace inclusion $A_\alpha \hookrightarrow X$ (composition of loops with the inclusion).
• $\mathrm{interHomLeft}_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\alpha, x_0)$ is induced by the inclusion $A_\alpha \cap A_\beta \hookrightarrow A_\alpha$, and $\mathrm{interHomRight}_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\beta, x_0)$ is induced by the inclusion $A_\alpha \cap A_\beta \hookrightarrow A_\beta$.
• $\mathrm{FreeProd} := \ast_{\alpha \in \iota}\, \pi_1(A_\alpha, x_0)$ is Mathlib's Monoid.CoprodI of the family of groups $\alpha \mapsto \pi_1(A_\alpha, x_0)$: the quotient of the free monoid on the alphabet $\{(\alpha, g) : \alpha \in \iota,\ g \in \pi_1(A_\alpha,x_0)\}$ by the congruence generated by $(\alpha, 1) \sim 1$ and $(\alpha, g)(\alpha, h) \sim (\alpha, gh)$; since every factor is a group this is a group (the free product of the groups $\pi_1(A_\alpha,x_0)$). For each $\alpha$, $\iota_\alpha :=$ Monoid.CoprodI.of $: \pi_1(A_\alpha,x_0) \to \mathrm{FreeProd}$ is the canonical homomorphism sending $g$ to the class of the one-letter word $(\alpha, g)$. Multiplication in $\mathrm{FreeProd}$ is concatenation of words (in the written order).
• $\Phi := \mathrm{vanKampenHom} : \mathrm{FreeProd} \to \pi_1(X, x_0)$ is Monoid.CoprodI.lift of the family $(\mathrm{inclHom}_\alpha)_\alpha$: the unique group homomorphism with $\Phi(\iota_\alpha(g)) = \mathrm{inclHom}_\alpha(g)$ for all $\alpha$ and all $g \in \pi_1(A_\alpha,x_0)$; concretely, a word $(\alpha_1,g_1)\cdots(\alpha_n,g_n)$ is sent to the product $\mathrm{inclHom}_{\alpha_1}(g_1)\cdots\mathrm{inclHom}_{\alpha_n}(g_n)$ computed in $\pi_1(X,x_0)$ (with that group's multiplication convention).
• $\mathrm{vanKampenRelators} \subseteq \mathrm{FreeProd}$ is the set

i.e. for every ordered pair $(\alpha,\beta)$ (including $\alpha=\beta$) and every based-homotopy class $\omega$ of loops in $A_\alpha \cap A_\beta$ at $x_0$, the element of the free product obtained as (the image of $\omega$ in $\pi_1(A_\alpha,x_0)$, placed in the $\alpha$-th factor) times (the inverse of the image of $\omega$ in $\pi_1(A_\beta,x_0)$, placed in the $\beta$-th factor).

• $N := \mathrm{vanKampenNormal}$ is Mathlib's Subgroup.normalClosure of $R$: the subgroup of $\mathrm{FreeProd}$ generated by the set of all conjugates $\{\, c\, r\, c^{-1} : r \in R,\ c \in \mathrm{FreeProd} \,\}$, equivalently the intersection of all subgroups of $\mathrm{FreeProd}$ containing every such conjugate; this is the smallest normal subgroup containing $R$.
• $\ker \Phi$ is Mathlib's MonoidHom.ker: the subgroup $\{\, w \in \mathrm{FreeProd} : \Phi(w) = 1 \,\}$, where $1 \in \pi_1(X,x_0)$ is the class of the constant loop at $x_0$.

Conclusion. Under all of the above hypotheses,

where $\le$ is the order on subgroups given by inclusion of underlying sets: every $w \in \mathrm{FreeProd}$ with $\Phi(w) = 1$ lies in $N$. Equivalently: every element of the free product $\ast_\alpha \pi_1(A_\alpha,x_0)$ that maps to the trivial class in $\pi_1(X,x_0)$ belongs to the normal closure of $R$. The statement asserts only this one inclusion ($\ker\Phi \subseteq N$); it does not assert the reverse inclusion $N \le \ker\Phi$, nor equality, nor surjectivity of $\Phi$, nor any isomorphism.

Edge cases made explicit. (i) If $\iota$ is empty, then $\bigcup_\alpha A_\alpha = \varnothing$, so $h_{\mathrm{cover}}$ forces $X = \varnothing$, which contradicts the existence of $x_0 \in X$; hence in that case the hypotheses are jointly unsatisfiable and the statement holds vacuously. (ii) The hypotheses $h_{\mathrm{inter}}$ and $h_{\mathrm{triple}}$ range over all pairs and triples of indices with repetitions allowed, so they include the statements "$A_\alpha \cap A_\alpha = A_\alpha$ is path-connected" and "$A_\alpha \cap A_\beta \cap A_\alpha$ is path-connected". (iii) The relator set $R$ includes the pairs $\alpha = \beta$, for which the relator is $\iota_\alpha(\omega')\,\iota_\alpha(\omega')^{-1} = 1$ with $\omega'$ the image of $\omega$ in $\pi_1(A_\alpha,x_0)$; it also includes both orderings $(\alpha,\beta)$ and $(\beta,\alpha)$ of each unordered pair. (iv) Nothing is assumed about the cardinality of $\iota$ beyond what $h_{\mathrm{cover}}$ and $x_0$ force; $X$ itself is not assumed path-connected, Hausdorff, or otherwise restricted. (v) The hypotheses $h_{\mathrm{open}}$ and $h_{\mathrm{cover}}$ are assumptions of the theorem; they do not appear in the definitions of $\Phi$, $R$, or $N$, which depend only on $A$, $x_0$, and $h_{x_0}$. (vi) The proof of this declaration is omitted (the body is sorry); the statement above is what is asserted, not what is proved.