Theorem 1.20 (isomorphism form): $\ast_\alpha\pi_1(A_\alpha)/N\cong\pi_1(X)$ induced by $\Phi$

Read-back: Hatcher.vanKampen_mulEquiv

Data and hypotheses

The statement is universally quantified over the following (all of them are arguments of the theorem; the first two are implicit, the rest explicit):

• a type $X$ equipped with a topology (no separation, compactness, or other axioms are assumed);
• an arbitrary index type $\iota$ (no finiteness, countability, nonemptiness, or decidable-equality assumption);
• 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$;
• $h_{\mathrm{open}}$: every $A_\alpha$ is open in $X$;
• $h_{\mathrm{pc}}$: every $A_\alpha$ is path-connected in the following sense (Mathlib's IsPathConnected for a subset $F \subseteq X$): 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 this forces $F \neq \varnothing$;
• $h_{\mathrm{cover}}$: the set equality $\bigcup_{\alpha \in \iota} A_\alpha = X$ (every point of $X$ lies in some $A_\alpha$);
• $h_{\mathrm{inter}}$: for all pairs $\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 all triples $\alpha, \beta, \gamma \in \iota$ (including repeated indices), the set $(A_\alpha \cap A_\beta) \cap A_\gamma$ is path-connected in the above sense.

Edge cases the quantifiers silently include: if $\iota$ is empty, then $h_{x_0}, h_{\mathrm{open}}, h_{\mathrm{pc}}, h_{\mathrm{inter}}, h_{\mathrm{triple}}$ are all vacuously true, but $h_{\mathrm{cover}}$ asserts $\varnothing = X$, which is impossible because $x_0 \in X$; so with $\iota = \varnothing$ the hypotheses are contradictory and the theorem says nothing. Since $x_0$ lies in every $A_\alpha$, all the sets $A_\alpha$, $A_\alpha \cap A_\beta$, $(A_\alpha\cap A_\beta)\cap A_\gamma$ are automatically nonempty. The hypotheses $h_{\mathrm{pc}}$ and $h_{\mathrm{inter}}$ are special cases of $h_{\mathrm{triple}}$ with repeated indices (the sets coincide), so they carry no extra content beyond $h_{\mathrm{triple}}$.

The objects appearing in the conclusion

Fundamental group. For a topological space $Y$ and a point $y \in Y$, $\pi_1(Y, y)$ denotes Mathlib's FundamentalGroup Y y: the group of endomorphisms of the object $y$ in the fundamental groupoid of $Y$. Concretely its elements are equivalence classes of continuous paths $\gamma : [0,1] \to Y$ with $\gamma(0)=\gamma(1)=y$, where two such loops are identified when there is a homotopy between them that fixes the endpoints $\{0,1\}$ throughout. The identity is the class of the constant loop, inversion is path reversal, and the product is defined by

$$p \cdot q \;=\; \text{(class of)}\; q \text{ followed by } p ,$$

i.e. Mathlib's p * q = q.trans p: the right-hand factor is traversed first.

Basepoints in subspaces. For $\alpha \in \iota$, the subset $A_\alpha$ is regarded as a topological space with the subspace topology, and $x_0$ is regarded as a point of it (this is basept, which is just the pair $(x_0, h_{x_0}(\alpha))$). Likewise $x_0$ is regarded as a point of the subspace $A_\alpha \cap A_\beta$ (this is basept₂). Below, $\pi_1(A_\alpha, x_0)$ and $\pi_1(A_\alpha\cap A_\beta, x_0)$ refer to fundamental groups of these subspaces at these basepoints.

Induced homomorphisms. Mathlib's FundamentalGroup.mapOfEq f h, for a continuous map $f : Y \to Z$ and a proof $h : f(y) = z$, 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$ (then transported along the equality $h$ of basepoints; here every such equality holds by definition, so the transport is trivial). Three instances are used:

• $\iota_\alpha : \pi_1(A_\alpha, x_0) \to \pi_1(X, x_0)$ (inclHom), induced by the inclusion map $A_\alpha \hookrightarrow X$ (the underlying map is the subtype projection, which is continuous);
• $i_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\alpha, x_0)$ (interHomLeft), induced by the inclusion $A_\alpha\cap A_\beta \hookrightarrow A_\alpha$;
• $j_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, x_0) \to \pi_1(A_\beta, x_0)$ (interHomRight), induced by the inclusion $A_\alpha\cap A_\beta \hookrightarrow A_\beta$.

In each case a loop in the smaller space is sent to the same loop viewed in the larger space. When $\alpha = \beta$, the maps $i_{\alpha\alpha}$ and $j_{\alpha\alpha}$ have the same underlying continuous map and hence coincide.

The free product. $\mathcal F := \operatorname{\ast}_{\alpha\in\iota} \pi_1(A_\alpha, x_0)$ (FreeProd) is Mathlib's Monoid.CoprodI of the family $\alpha \mapsto \pi_1(A_\alpha, x_0)$: the quotient of the free monoid on the alphabet of pairs $(\alpha, g)$ with $\alpha\in\iota$, $g \in \pi_1(A_\alpha,x_0)$, by the smallest monoid congruence such that the one-letter word $(\alpha, 1)$ equals the empty word and the two-letter word $(\alpha, g)(\alpha, g')$ equals the one-letter word $(\alpha, g g')$. Because each factor is a group, $\mathcal F$ is a group. For each $\alpha$ there is a homomorphism $\mathrm{of}_\alpha : \pi_1(A_\alpha, x_0) \to \mathcal F$ (Monoid.CoprodI.of) sending $g$ to the class of the one-letter word $(\alpha, g)$. Given a family of homomorphisms $\varphi_\alpha : \pi_1(A_\alpha, x_0) \to H$ into a monoid $H$, Monoid.CoprodI.lift $\varphi$ is the unique homomorphism $\mathcal F \to H$ with $(\mathrm{lift}\,\varphi)(\mathrm{of}_\alpha\, g) = \varphi_\alpha(g)$; on the class of a word $(\alpha_1,g_1)\cdots(\alpha_n,g_n)$ it gives $\varphi_{\alpha_1}(g_1)\cdots\varphi_{\alpha_n}(g_n)$. If $\iota$ were empty $\mathcal F$ would be the trivial group (but see the edge-case remark above).

The map $\Phi$. $\Phi : \mathcal F \to \pi_1(X, x_0)$ (vanKampenHom) is $\mathrm{lift}$ of the family $(\iota_\alpha)_\alpha$; so $\Phi(\mathrm{of}_\alpha\, g) = \iota_\alpha(g)$ for every $\alpha$ and $g \in \pi_1(A_\alpha,x_0)$, and $\Phi$ of a word is the product in $\pi_1(X,x_0)$ (with the multiplication convention above) of the images of its letters.

The relators and the normal subgroup. The set $R \subseteq \mathcal F$ (vanKampenRelators) is

$$R \;=\; \bigl\{\, \mathrm{of}_\alpha\bigl(i_{\alpha\beta}(\omega)\bigr)\cdot \mathrm{of}_\beta\bigl(j_{\alpha\beta}(\omega)\bigr)^{-1} \;:\; \alpha,\beta\in\iota,\ \omega \in \pi_1(A_\alpha\cap A_\beta, x_0) \,\bigr\},$$

where the pairs $(\alpha,\beta)$ range over all ordered pairs, including $\alpha=\beta$ (for which the element is the identity, since $i_{\alpha\alpha} = j_{\alpha\alpha}$). The subgroup $N \le \mathcal F$ (vanKampenNormal) is Mathlib's Subgroup.normalClosure of $R$: the subgroup generated by the set of all conjugates $c\, r\, c^{-1}$ with $r \in R$, $c \in \mathcal F$. It is the smallest normal subgroup of $\mathcal F$ containing $R$. The accompanying instance records that $N$ is normal, meaning: for every $n \in N$ and every $c \in \mathcal F$, $c\,n\,c^{-1} \in N$.

The quotient group. $\mathcal F / N$ is Mathlib's quotient of the group $\mathcal F$ by the subgroup $N$: the set of left cosets, i.e. the quotient of $\mathcal F$ by the relation $g \sim g' \iff g^{-1}g' \in N$, endowed with the group structure induced from $\mathcal F$ (well defined because $N$ is normal). The canonical projection $g \mapsto [g]$ (QuotientGroup.mk) is a surjective group homomorphism $\mathcal F \to \mathcal F/N$.

Group isomorphism. $G \simeq^{*} H$ (MulEquiv) means a bijection $e : G \to H$ satisfying $e(ab) = e(a)\,e(b)$ for all $a,b$ (its inverse is then automatically multiplicative). Applying $e$ to an element means applying the underlying function.

The conclusion

Under all the hypotheses above, the theorem asserts:

$$\exists\, e : \mathcal F / N \;\simeq^{*}\; \pi_1(X, x_0) \quad\text{such that}\quad \forall\, g \in \mathcal F,\ \ e\bigl([g]\bigr) = \Phi(g).$$

That is: there exists (plain existence, not unique existence) a group isomorphism $e$ from the quotient $\bigl(\operatorname{\ast}_{\alpha} \pi_1(A_\alpha,x_0)\bigr)/N$ onto $\pi_1(X,x_0)$ such that, for every element $g$ of the free product (not merely for generators), the value of $e$ on the coset of $g$ equals $\Phi(g)$; in other words, $e \circ (\text{projection}) = \Phi$ as maps $\mathcal F \to \pi_1(X,x_0)$. Because the projection is surjective, the displayed condition is the same as requiring that $\Phi$ be surjective onto $\pi_1(X,x_0)$ with kernel exactly $N$ (no more and no less), and that $e$ be the map induced by $\Phi$ on cosets. The statement does not itself provide $e$, $\Phi$'s surjectivity, or a description of $\ker\Phi$ beyond what is implied by this existence claim.