Read-back: Hatcher definition bundle (van Kampen data)

Ambient data shared by every declaration

Every declaration below lives in a namespace called Hatcher and is parametrised by the following data, which are arguments to each declaration (the first two implicitly, the last three explicitly):

• a type $X$ equipped with a topology (no separation, connectedness, or path-connectedness assumption is made);
• an index type $\iota$ (arbitrary; it may be empty, finite, or infinite);
• a family $A : \iota \to \mathcal{P}(X)$ of subsets $A_\alpha \subseteq X$, one for each $\alpha \in \iota$ (no hypothesis is imposed on the $A_\alpha$: they need not be open, path-connected, or cover $X$, and distinct indices may give the same set);
• a point $x_0 \in X$;
• a proof $h_{x_0}$ that $x_0 \in A_\alpha$ for every $\alpha \in \iota$.

Throughout, a subset $S \subseteq X$ is regarded as a topological space in its own right by giving it the subspace topology inherited from $X$; its points are pairs (a point of $X$, a proof that it lies in $S$). The intersection $A_\alpha \cap A_\beta$ is likewise given the subspace topology.

Convention for fundamental groups used by the code. For a topological space $Y$ and a point $y \in Y$, the Mathlib object written $\pi_1(Y, y)$ below is the set of endpoint-preserving homotopy classes $[\gamma]$ of loops $\gamma : [0,1] \to Y$ with $\gamma(0) = \gamma(1) = y$, made into a group as follows:

• the identity element is the class of the constant loop at $y$;
• the inverse of $[\gamma]$ is the class of the reversed loop $t \mapsto \gamma(1-t)$;
• the product is reversed relative to concatenation order: for classes $p, q$,

$$p \cdot q \;=\; [\,\gamma_q \ast \gamma_p\,],$$

where $\gamma_q \ast \gamma_p$ denotes the loop that first traverses a representative of $q$ (on $[0, \tfrac12]$, at double speed) and then a representative of $p$ (on $[\tfrac12, 1]$, at double speed). Thus $p \cdot q$ is "$q$ first, then $p$."

(Internally $\pi_1(Y,y)$ is the endomorphism monoid of the object $y$ in the fundamental groupoid of $Y$, whose morphisms $y \to y'$ are homotopy classes of paths from $y$ to $y'$ and whose composition $p \ggg q$ is "$p$ then $q$"; the monoid product on endomorphisms is defined as $p \cdot q := q \ggg p$, which produces the reversal just stated.)

Induced homomorphisms. For a continuous map $f : Y \to Z$ and points $y \in Y$, $z \in Z$ together with a proof that $f(y) = z$, Mathlib's FundamentalGroup.mapOfEq is the group homomorphism $\pi_1(Y, y) \to \pi_1(Z, z)$ sending $[\gamma]$ to $[f \circ \gamma]$, where the loop $f \circ \gamma$ (based at $f(y)$) is re-labelled as a loop based at $z$ using the equation $f(y) = z$. In every use below the proof of $f(y) = z$ is the trivial one (the two sides are literally the same point), so the re-labelling does nothing and the map is simply $[\gamma] \mapsto [f \circ \gamma]$.

---

1. basept

For each $\alpha \in \iota$, $\mathrm{basept}_\alpha$ is the point $x_0$ regarded as an element of the subspace $A_\alpha$, i.e. the pair

$$\mathrm{basept}_\alpha := (x_0,\ h_{x_0}(\alpha)) \in A_\alpha,$$

where $h_{x_0}(\alpha)$ is the supplied proof that $x_0 \in A_\alpha$. Its underlying point of $X$ is $x_0$.

2. basept₂

For each pair $\alpha, \beta \in \iota$ (not required to be distinct), $\mathrm{basept}_{\alpha\beta}$ is the point $x_0$ regarded as an element of the subspace $A_\alpha \cap A_\beta$, i.e.

$$\mathrm{basept}_{\alpha\beta} := (x_0,\ (h_{x_0}(\alpha),\ h_{x_0}(\beta))) \in A_\alpha \cap A_\beta.$$

Its underlying point of $X$ is $x_0$.

3. inclHom

For each $\alpha \in \iota$, $\mathrm{inclHom}_\alpha$ is a group homomorphism

$$\mathrm{inclHom}_\alpha : \pi_1(A_\alpha, \mathrm{basept}_\alpha) \longrightarrow \pi_1(X, x_0).$$

It is the homomorphism induced (in the sense of "Induced homomorphisms" above) by the continuous map $A_\alpha \to X$ that sends a point of the subspace $A_\alpha$ to its underlying point of $X$ (the subspace inclusion $j_\alpha$), together with the trivial proof that $j_\alpha(\mathrm{basept}_\alpha) = x_0$. Concretely, a homotopy class $[\gamma]$ of a loop $\gamma$ in $A_\alpha$ based at $x_0$ is sent to the homotopy class $[j_\alpha \circ \gamma]$ of the same loop viewed in $X$. The domain and codomain groups carry the reversed-product convention stated above, and this map respects it.

4. FreeProd

$\mathrm{FreeProd}$ is a type (introduced as an abbreviation, so it unfolds transparently): the Mathlib free product Monoid.CoprodI of the indexed family of groups

$$\alpha \longmapsto \pi_1(A_\alpha, \mathrm{basept}_\alpha), \qquad \alpha \in \iota.$$

Explicitly, Monoid.CoprodI of a family of monoids $(M_\alpha)_{\alpha \in \iota}$ is the quotient of the free monoid on the alphabet $\coprod_{\alpha \in \iota} M_\alpha$ (letters are pairs $(\alpha, m)$ with $m \in M_\alpha$) by the smallest monoid congruence such that

• the one-letter word $(\alpha, 1)$ is identified with the empty word, for every $\alpha$; and
• the two-letter word $(\alpha, m)(\alpha, m')$ is identified with the one-letter word $(\alpha, m \cdot m')$, for every $\alpha$ and $m, m' \in M_\alpha$.

Its multiplication is concatenation of words. Because each factor here is a group, Mathlib equips Monoid.CoprodI with a group structure (the inverse of a word is obtained by reversing it and inverting each letter in its own factor). So $\mathrm{FreeProd}$ is the free product $\ast_{\alpha \in \iota}\, \pi_1(A_\alpha, \mathrm{basept}_\alpha)$. If $\iota$ is empty, $\mathrm{FreeProd}$ is the trivial group.

For each $\alpha$, the canonical homomorphism from the $\alpha$-th factor into the free product, written Monoid.CoprodI.of and denoted $\mathrm{of}_\alpha$ below, sends $m \in \pi_1(A_\alpha, \mathrm{basept}_\alpha)$ to the class of the one-letter word $(\alpha, m)$.

5. vanKampenHom

$\Phi := \mathrm{vanKampenHom}$ is a group homomorphism

$$\Phi : \mathrm{FreeProd} = \ast_{\alpha \in \iota}\, \pi_1(A_\alpha, \mathrm{basept}_\alpha) \longrightarrow \pi_1(X, x_0),$$

namely the one obtained by Mathlib's universal-property map Monoid.CoprodI.lift from the family $(\mathrm{inclHom}_\alpha)_{\alpha\in\iota}$. It is the unique monoid homomorphism with $\Phi \circ \mathrm{of}_\alpha = \mathrm{inclHom}_\alpha$ for every $\alpha$. Concretely, the class of a word $(\alpha_1, g_1)(\alpha_2, g_2)\cdots(\alpha_n, g_n)$ is sent to the product

$$\mathrm{inclHom}_{\alpha_1}(g_1)\cdot \mathrm{inclHom}_{\alpha_2}(g_2)\cdots \mathrm{inclHom}_{\alpha_n}(g_n)$$

computed in $\pi_1(X, x_0)$ with the reversed-product convention above (so, as a loop, this is "$g_n$ first, then $g_{n-1}$, …, then $g_1$", each viewed in $X$); the empty word goes to the identity.

6. interHomLeft

For each pair $\alpha, \beta \in \iota$ (not required to be distinct), $\mathrm{interHomLeft}_{\alpha\beta}$ is a group homomorphism

$$\mathrm{interHomLeft}_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, \mathrm{basept}_{\alpha\beta}) \longrightarrow \pi_1(A_\alpha, \mathrm{basept}_\alpha).$$

It is the homomorphism induced by the continuous map $A_\alpha \cap A_\beta \to A_\alpha$ that sends a point $(x, (p_\alpha, p_\beta))$ of the intersection to the point $(x, p_\alpha)$ of $A_\alpha$ (this is Mathlib's Set.inclusion applied to the inclusion $A_\alpha \cap A_\beta \subseteq A_\alpha$: the identity on underlying points, discarding the membership proof for $A_\beta$), together with the trivial proof that this map sends $\mathrm{basept}_{\alpha\beta}$ to $\mathrm{basept}_\alpha$. Concretely, $[\gamma] \mapsto [\gamma]$ with the loop $\gamma$ re-viewed as a loop in $A_\alpha$.

7. interHomRight

For each pair $\alpha, \beta \in \iota$, $\mathrm{interHomRight}_{\alpha\beta}$ is a group homomorphism

$$\mathrm{interHomRight}_{\alpha\beta} : \pi_1(A_\alpha \cap A_\beta, \mathrm{basept}_{\alpha\beta}) \longrightarrow \pi_1(A_\beta, \mathrm{basept}_\beta),$$

induced by the continuous map $A_\alpha \cap A_\beta \to A_\beta$ sending $(x, (p_\alpha, p_\beta)) \mapsto (x, p_\beta)$ (Mathlib's Set.inclusion for $A_\alpha \cap A_\beta \subseteq A_\beta$), together with the trivial proof that $\mathrm{basept}_{\alpha\beta}$ is sent to $\mathrm{basept}_\beta$. Concretely, $[\gamma] \mapsto [\gamma]$ with $\gamma$ re-viewed as a loop in $A_\beta$. Note that the same intersection $A_\alpha \cap A_\beta$ (in that order) is the domain of both $\mathrm{interHomLeft}_{\alpha\beta}$ and $\mathrm{interHomRight}_{\alpha\beta}$.

8. vanKampenRelators

$R := \mathrm{vanKampenRelators}$ is a subset of $\mathrm{FreeProd}$, defined by

$$R = \Bigl\{\, g \in \mathrm{FreeProd} \;\Big|\; \exists\, \alpha \in \iota,\ \exists\, \beta \in \iota,\ \exists\, \omega \in \pi_1(A_\alpha \cap A_\beta, \mathrm{basept}_{\alpha\beta}),\quad g = \mathrm{of}_\alpha\bigl(\mathrm{interHomLeft}_{\alpha\beta}(\omega)\bigr) \cdot \bigl(\mathrm{of}_\beta(\mathrm{interHomRight}_{\alpha\beta}(\omega))\bigr)^{-1} \Bigr\}.$$

Here:

• $\alpha$ and $\beta$ range independently over all of $\iota$, including $\alpha = \beta$;
• $\omega$ ranges over all elements of $\pi_1(A_\alpha \cap A_\beta, x_0)$;
• $\mathrm{of}_\alpha(\cdot)$ places the image of $\omega$ in $\pi_1(A_\alpha, \mathrm{basept}_\alpha)$ into the $\alpha$-th factor of the free product, and $\mathrm{of}_\beta(\cdot)$ places the image of $\omega$ in $\pi_1(A_\beta, \mathrm{basept}_\beta)$ into the $\beta$-th factor;
• the product and inverse are those of the group $\mathrm{FreeProd}$; the inverse applies only to the second factor, so $g$ is the (class of the) two-letter word: first the letter $(\alpha, \mathrm{interHomLeft}_{\alpha\beta}(\omega))$, then the letter $(\beta, \mathrm{interHomRight}_{\alpha\beta}(\omega)^{-1})$.

If $\iota$ is empty then $R$ is empty. When $\alpha = \beta$, both homomorphisms coincide and the corresponding element of $R$ is the identity.

9. vanKampenNormal

$N := \mathrm{vanKampenNormal}$ is a subgroup of $\mathrm{FreeProd}$: the Mathlib normal closure Subgroup.normalClosure of the set $R$ above. By definition this is the subgroup generated by the set of all conjugates of elements of $R$,

$$N = \bigl\langle\, \{\, c\, r\, c^{-1} \;:\; r \in R,\ c \in \mathrm{FreeProd} \,\} \,\bigr\rangle,$$

i.e. the smallest subgroup of $\mathrm{FreeProd}$ containing every $c\,r\,c^{-1}$ with $r \in R$ and $c$ arbitrary. (Mathlib phrases "conjugates of $r$" as all $x$ with $\exists c,\ c\,r\,c^{-1} = x$.) If $R$ is empty, $N$ is the trivial subgroup.

10. vanKampenNormal_normal (instance)

This registers the fact that the subgroup $N = \mathrm{vanKampenNormal}$ is a normal subgroup of $\mathrm{FreeProd}$, i.e. for all $n \in N$ and all $c \in \mathrm{FreeProd}$, $c\,n\,c^{-1} \in N$. The proof is Mathlib's general fact that the normal closure of any set is normal. It introduces no new data.

11. loopIn

For each $\alpha \in \iota$ and each path $g$ in the subspace $A_\alpha$ from $\mathrm{basept}_\alpha$ to $\mathrm{basept}_\alpha$ (a Mathlib Path: a continuous map $g : [0,1] \to A_\alpha$ with $g(0) = g(1) = \mathrm{basept}_\alpha$, i.e. a loop in $A_\alpha$ at $x_0$), $\mathrm{loopIn}_\alpha(g)$ is a path in $X$ from $x_0$ to $x_0$, namely the composite $j_\alpha \circ g : [0,1] \to X$ of $g$ with the subspace inclusion $j_\alpha : A_\alpha \to X$ (Mathlib's Path.map, whose underlying function is literally $t \mapsto j_\alpha(g(t))$). This is an actual path, not a homotopy class. Its endpoints are $j_\alpha(\mathrm{basept}_\alpha)$, which is $x_0$ by definition.

12. loopProd

For a finite list $l = [p_1, p_2, \dots, p_n]$ of paths in $X$ from $x_0$ to $x_0$ (each $p_k : [0,1] \to X$ continuous with $p_k(0) = p_k(1) = x_0$), $\mathrm{loopProd}(l)$ is a single path in $X$ from $x_0$ to $x_0$, defined by a right fold with Mathlib's path concatenation Path.trans and the constant path $c_{x_0}$ (Mathlib's Path.refl) as the initial value:

$$\mathrm{loopProd}([p_1,\dots,p_n]) = p_1 \ast \bigl(p_2 \ast \bigl(\cdots \ast (p_n \ast c_{x_0})\bigr)\bigr),$$

where for paths $\gamma, \gamma'$ the concatenation $\gamma \ast \gamma'$ is the path

$$(\gamma \ast \gamma')(t) = \begin{cases} \gamma(2t) & t \le \tfrac12,\\ \gamma'(2t - 1) & t > \tfrac12 \end{cases}$$

("$\gamma$ first, then $\gamma'$", each at double speed). In particular:

• for the empty list, $\mathrm{loopProd}([\,]) = c_{x_0}$, the constant loop at $x_0$;
• for $n \ge 1$, the resulting loop traverses $p_1$ on $[0, \tfrac12]$, $p_2$ on $[\tfrac12, \tfrac34]$, and in general $p_k$ on $[1 - 2^{-(k-1)},\ 1 - 2^{-k}]$ for $k = 1, \dots, n$, and is constant at $x_0$ on the final interval $[1 - 2^{-n}, 1]$;
• the list order is the traversal order: $p_1$ is traversed first and $p_n$ last.

This is an actual parametrised path, not a homotopy class, and no relation to the group product of $\pi_1(X, x_0)$ (whose convention is "second factor first") is asserted by this definition.