----
$\pi_{1}$ denotes the [[fundamental group]] of a space; $*$ its [[fundamental groupoid|path concatenation]] operation.
> [!theorem] Theorem. ([[The Galois Correspondence for Covering Spaces]])
> Let $\widetilde{X}$ be a [[covering space]] of the [[topological space]] $X$. The [[homomorphism of fundamental groups induced by a continuous map|pushforward morphism]] $p_{*}:\pi_{1}(\widetilde{X}, \tilde{x}_{0}) \to \pi_{1}(X,x_{0})$ [[pushforward morphism of covering map is an embedding|is injective]] and determines a [[subgroup]] $p_{*}\big( \pi_{1}(\widetilde{X},\tilde{x}_{0} ) \big) \leq \pi_{1}(X,x_{0})$. Thus there is a function $\left\{ \begin{align}
> &\text{based covering maps} \\
> & p: (\widetilde{X}, \tilde{x}_{0}) \to (X,x_{0})
> \end{align} \right\} \xrightarrow{f_{\tilde{x}_{0}}} \{ \text{subgroups of } \pi_{1}(X, x_{0}) \}.$
> If we suppose $X$ is [[path-connected]], then for $\tilde{x}_{0}' \in \widetilde{X}$ there exists a [[parameterized curve]] $\gamma$ from $\tilde{x}_{0}$ to $\tilde{x}_{0}'$, and we have $[p \circ \gamma]^{-1} * p_{*}(\pi_{1}(\widetilde{X}, \tilde{x}_{0})) * [p \circ \gamma] = p_{*}(\pi_{1}(\widetilde{X}, \tilde{x}_{0})),$
> i.e., the [[subgroup|subgroups]] obtained from these two [[pointed set|basepoints]] are [[conjugate]]. Thus there is a function
> $\{ \text{covering maps }p:\widetilde{X} \to X \} \xrightarrow{f} \left\{ \begin{align}
> &\text{conjugacy classes of} \\
> &\text{subgroups of } \pi_{1}(X,x_{0})
> \end{align} \right\}.$
> The claim is that under certain conditions, declaring $p_{1} \sim p_{2}$ if and only if $p_{1}$ is [[isomorphism of covering spaces|isomorphic]] to $p_{2}$ and [[quotient set|quotienting]] accordingly turns these maps into [[bijection|bijections]] (in the flavor of [[the canonical decomposition of a set function]]):
>
> ```tikz
> \usepackage{tikz-cd}
> \usepackage{amsmath}
>
> \begin{document}
> \begin{tikzcd}
> \left\{
> \begin{array}{c}
> \text{based covering maps} \\
> p: (\widetilde{X}, \tilde{x}_0) \to (X, x_0)
> \end{array}
> \right\} \arrow[r, "f_{\tilde{x}_0}", two heads] \arrow[d, "\pi"', two heads]
> & \{ \text{subgroups of } \pi_1(X, x_0) \} \\
> \frac{\left\{
> \begin{array}{c}
> \text{based covering maps} \\
> p: (\widetilde{X}, \tilde{x}_0) \to (X, x_0)
> \end{array}
> \right\}}{\{p_1 \sim p_2 \iff p_1 \cong p_2 \}} \arrow[ru, "\exists ! g_{\tilde{x}_0}"', hook, two heads]
> &
> \end{tikzcd}
> \end{document}
> ```
> and
> ```tikz
> \usepackage{tikz-cd} \usepackage{amsmath} \begin{document} \begin{tikzcd} \left\{ \text{covering maps } p: \widetilde{X} \to X \right\} \arrow[r, "f", two heads] \arrow[d, "\pi"', two heads] & \left\{ \begin{array}{c} \text{conjugacy classes of} \\ \text{subgroups of } \pi_1(X, x_0) \end{array} \right\} \\ \frac{\left\{ \text{covering maps } p: \widetilde{X} \to X \right\}}{\left\{ p_1 \sim p_2 \iff p_1 \cong p_2 \right\}}. \arrow[ru, "\exists ! g"', hook, two heads] & \end{tikzcd} \end{document}
> ```
>
> These conditions and their implications are as follows.
>
> **Existence — Surjectivity.** Suppose further that $X$ is [[path-connected]], [[locally connected, locally path-connected|locally path-connected]], and [[semilocally simply connected]]. Then $f_{\widetilde{x}_{0}}$ is a [[surjection]]: for any [[subgroup]] $H \leq \pi_{1}(X,x_{0})$ there is a [[pointed set|based]] [[covering space|covering map]] $p:(\widetilde{X}, \tilde{x}_{0}) \to (X,x_{0})$ such that the [[homomorphism of fundamental groups induced by a continuous map|pushforward]] image $p_{*}(\pi_{1}(\widetilde{X}, \tilde{x}_{0}))$ equals $H$.
>
> **Based Uniqueness.** Suppose that $p_{1}: (\widetilde{X}_{1}, \tilde{x}_{1}) \to (X,x_{0}) \text{ and } p_{2}:(\widetilde{X}_{2}, \tilde{x}_{2}) \to (X,x_{0})$
> are [[path-connected]] [[covering space|covering spaces]]. Then there is a [[pointed set|based]] [[isomorphism of covering spaces]] $h: (\widetilde{X}_{1}, \tilde{x}_{1}) \to (\widetilde{X}_{2}, \tilde{x}_{2}),$
> ```tikz
> \usepackage{tikz-cd}
> \usepackage{amsmath}
> \begin{document}
> % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAAoAdTgdy1jwNYwABoBfAPoBGUgAJug4QA9JUgJQgxpdJlz5CKAEzkqtRizZde-GIpijJx+ZzvAVEwxq07seAkRkpU3pmVkQOEVIlCWIvUxgoAHN4IlAAMwAnCABbJDIQHAgkYzNQtjRpEGoGOgAjGAYABV0-AxAMrESACxxNbRBMnKQZAqLEEpCLcIrDPvSs3MR8wuHqSbCQLs0KMSA
> \begin{tikzcd}
> {(\widetilde{X}_1, \tilde{x}_1)} \arrow[rd, "p_1"'] \arrow[rr, "h \text{ a homeomorphism}"] & & {(\widetilde{X}_2, \tilde{x}_2)} \arrow[ld, "p_2"] \\
> & {(X,x_0)} &
> \end{tikzcd}
> \end{document}
> ```
> if and only if the [[homomorphism of fundamental groups induced by a continuous map|pushforward images]] agree: $(p_{1})_{*}\big( \pi_{1}(\widetilde{X}_{1}, \tilde{x}_{1}) \big)=(p_{2})_{*}\big( \pi_{1}(\widetilde{X}_{2}, \tilde{x}_{2}) \big) \leq \pi_{1}(X,x_{0}).$
>
> [!proof]- Proof. ([[The Galois Correspondence for Covering Spaces]])
>
>
> **Existence.** First we show $f_{\tilde{x}_{0}}$ is a [[surjection]]. Note that the hypotheses supplied imply the existence of a [[universal cover]], by [[constructing universal covers]]. Let $q: \overline{X} \to X$ be the [[universal cover]] constructed in that theorem, whose underlying set consists of all [[homotopy|homotopy classes]] of [[parameterized curve|paths]] starting at $x_{0}$. Define a [[relation]] $\sim_{H}$ on $\overline{X}$ by $[\gamma] \sim_{H} [\gamma'] \iff \gamma(1)=\gamma'(1) \text{ and } [\gamma * \overline{\gamma'}] \in H \subset \pi_{1}(X,x_{0}), $
> where $*$ denotes [[fundamental groupoid|path concatenation]] and $\overline{\gamma}$ the [[parameterized curve|reverse path]] of $\gamma$. We claim $\sim_{H}$ is an [[equivalence relation]]. Indeed,
>
> 1. $[\gamma] \sim_{H} [\gamma]$ since $[e_{x_{0}}] \in H$;
> 2. $[\gamma] \sim_{H} [\gamma'] \implies [\gamma'] \sim_{H} [\gamma]$ since if $[\gamma * \overline{\gamma'}] \in H$ then, since $H$ is a [[group]], its inverse loop $[\gamma' * \overline{\gamma}]$ is also.
> 3. If $[\gamma] \sim_{H} [\gamma']$ and $[\gamma'] \sim_{H} [\gamma'']$, then so is $[\gamma * \overline{\gamma''}]$, by the fact that $H$ is stable under composition (concatenation).
>
> Let us define $\widetilde{X}_{H} := \overline{X} / \sim_{H}$ to be the [[quotient space]], and $p_{H}:\widetilde{X}_{H} \to X$ to be the map $[\overline{x}]_{\sim_{H}} \mapsto p( \overline{x} )$ induced by the [[universal property]] of [[universal property of the quotient topology|quotient topology]]:
>
> ```tikz
> \usepackage{tikz-cd}
> \usepackage{amsmath}
> \begin{document}
> % https://tikzcd.yichuanshen.de/#N4Igdg9gJgpgziAXAbVABwnAlgFyxMJZABgBpiBdUkANwEMAbAVxiRAB12IaYAnBrGBjAAGgF8QY0uky58hFGQCMVWoxZtOAdyyw8DWKLEACAPTHO2ALYB9ABKTpIDNjwEiS0iur1mrRCAikqowUADm8ESgAGa8EFZIZCA4EEgATD7q-s6OMXEJiEkpSJ5qfprsaFgg1Ax0AEYwDAAKsm4KILxYYQAWOLkgsfEl1MWIGSACQmxQdHA9oTVlGgGcMAAeWHA4cMYAhMZo9kt1jS1t8mxdvf1iFGJAA
> \begin{tikzcd}
> \overline{X} \arrow[rd, "p"] \arrow[d, "\pi"'] & \\
> \overline{X} / \sim_H \arrow[r, "\exists ! p_H"', dashed] & X
> \end{tikzcd}
> \end{document}
> ```
>
> Now recall the notation from [[constructing universal covers]], namely the sets$(\alpha, U):= \left\{ [\gamma] \in \widetilde{X} : \begin{align}
> & [\gamma]=[\alpha * \alpha'] \text{ for some path } \\
> & \alpha' \text{ in } U \text{ starting at } \alpha(1)
> \end{align} \right\},$
> which form a [[basis for a topology|basis]] [[topology generated by a basis|generating]] the [[topology generated by a basis|topology]] on $\overline{X}$. We note that if $[\gamma] \in (\alpha, U)$ and $[\gamma'] \in (\beta, U)$ have $[\gamma] \sim_{H} [\gamma']$, then in fact the entire sets $(\alpha, U)$ and $(\beta, U)$ are identified by $\sim_{H}$, since $[\gamma * \eta] \sim_{H} [\gamma' * \eta]$ for $\eta$ a [[parameterized curve]] in $U$ [^1] . Thus $p_{H}$ is a [[covering space|covering map]]. [^2]
>
> It remains, but will suffice, to show $(p_{H})_{*}(\pi_{1}(\widetilde{X}_{H}, \big[ [e_{x_{0}}]_{\sim_{H}} \big]))=H$. If $[\gamma] \in H$, then [[the homotopy lifting lemma|the]] [[lifting|lift]] $\overline{\gamma}$ of $\gamma$ to $\overline{X}$ starting at $[e_{x_{0}}]$ ends at $[\gamma]$. So the [[lifting|lift]] to $\widetilde{X}_{H}$ ends at $\big[ [\gamma] \big]_{\sim_{H}}$, which equals $[ [e_{x_{0}}]]_{\sim_{H}}$ (just check with the definition of $\sim_{H}$) and so is a [[parameterized curve|loop]]. Thus $\supset$ is shown. For the reverse containment, consider that if $[\gamma]=(p_{H})_{*}([\tilde{\gamma}])$ for $\tilde{\gamma}$ a [[parameterized curve|loop]] in $\widetilde{X}_{H}$, then $[\gamma] \sim [e_{x_{0}}]$ so $[\gamma] \in H$. This shows $\subset$, and the lemma is done.
>
> **Based Uniqueness.** One direction is easy: if $h$ exists, then $h_{*}$ is a [[group isomorphism]] and we have $(p_{1})_{*}=(p_{2})_{*} \circ h_{*}$ so the images agree. [^3] Conversely, suppose $(p_{1})_{*}\big( \pi_{1}(\widetilde{X}_{1}, \tilde{x}_{1}) \big)=(p_{2})_{*}\big( \pi_{1} (\widetilde{X}_{2}, \tilde{x}_{2}) \big)=:H$.
---
####
[^1]: To check this: $[\gamma * \eta * \overline{\gamma' * \eta}]=[\gamma * \eta * \overline{\eta} * \overline{\gamma'}]=[\gamma * \overline{\gamma'}]$.
[^2]: Here is a concrete (if verbose) verification. Denote $\pi\big(( \alpha, U) \big):=[(\alpha, U)]$. The definition of $p_{H}$ is that for all inputs $[(\alpha, U)]$, $p_{H}|_{[\alpha, U]}([(\alpha, U)])=p |_{(\alpha, U)} \big( (\alpha, U) \big)$; the latter is a [[homeomorphism]] onto $U$ and thus the former is too. So all we have to show is that $p_{H}^{-1}(U)$ takes the form $\coprod_{\delta} [(\alpha, U)]_{\delta}.$
With $p ^{-1}(U)=\coprod_{\varepsilon} (\alpha ,U)_{\varepsilon}$, we know $\begin{align}
p_{H}^{-1}(U) := & \big\{ \big[ [\gamma] \big]_{\sim_{H}} : p([\gamma]) \in U \big\} \\
= & \big\{ \big[ [\gamma] \big]_{\sim_{H}} : [\gamma] \in p ^{-1}(U) \big\} \\
= & \big\{ \big[ [\gamma] \big]_{\sim_{H}} : [\gamma] \in (\alpha,U)_{\varepsilon} \text{ for some index } \varepsilon\big\} \\
= & \bigcup_{\varepsilon}^{} [(\alpha, U)_{\varepsilon}].
\end{align}$
We claim this union (for nontrivial $H$, at least) contains redundant sets, and indeed is disjoint. For if both $\big[[\gamma]\big]_{\sim_{H}} \in [(\alpha, U)_{i}]$ and $\big[[\gamma]\big]_{\sim_{H}} \in [(\alpha, U)_{j}]$, then there exists $[\gamma] \in (\alpha, U)_{i}$ and $[\gamma'] \in (\alpha, U)_{j}$ for which $[\gamma] \sim_{H} [\gamma']$, implying (as we have already seen) that $(\alpha, U)_{i}$ and $(\alpha, U)_{j}$ are identified under $\pi$.
[^3]: Explicitly, the idea is that $(p_{1})_{*}=p_{2_{*}} \circ h_{*}$ and $(p_{2})_{*}=(p_{1})_{*} \circ h_{*}^{-1}$; now substitute the latter into the former.
-----
#### References
> [!backlink]
> ```dataview
TABLE rows.file.link as "Further Reading"
FROM [[]]
FLATTEN file.tags
GROUP BY file.tags as Tag
> [!frontlink]
> ```dataview
> TABLE rows.file.link as "Further Reading"
> FROM outgoing([[]])
> FLATTEN file.tags as Tag
> WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom"
> GROUP BY Tag
> ```