$\newcommand{\gal}{\operatorname{Gal}}$This question is about showing the two definitions of Krull topology over an infinite Galois group are the same. I would greatly appreciate any feedback on the proof, as I got a little confused while writing it.
Notation and setup:
$L/K$ is some algebraic field extension, and it is Galois: there is some set $I$ and an $I$-index family of fields $E_i$, where $K\subseteq E_i\subseteq L$ and $E_i/K$ is a finite Galois extension, such that: $$L=\bigcup_{i\in I}E_i$$
It is not too hard to see that $\gal(L/K)$ is isomorphic to $G:=\varprojlim_I\gal(E_i/K)$, where the categorical limit is taken with respect to the obvious projections $\gal(E/K)\to\gal(E'/K)$ for $E'\subseteq E$. If one equips each, finite, $\gal(E_i/K)$ with the discrete topology, using results from category theory we immediately find that $G$ is a compact Hausdorff topological group.
I am reading from two different sources: one endows $\gal(L/K)$ with the Krull topology and the other endows $\gal(L/K)$ with the topology inherited by identification with $G$. I'm confident these are the same, but I want to demonstrate they are the same. I've thought about this, and I have a solution - I'm asking for a solution verification. In particular I want to know if my approach is correct - links to other solutions are welcome, but I don't think they would count as duplicates.
The definition of Krull topology that my first source is using is this:
Given $\sigma\in\gal(L/K)$, the neighbourhood base at $\sigma$ is given by cosets $\sigma\gal(L/F)$ where $L/F/K$ and $F/K$ is a finite extension.
My proof of topological equivalence:
It suffices to show the neighbourhood bases contain each other, at the origin, since both topologies define topological groups which are homogeneous.
A basic neighbourhood of the identity in $\prod_{i\in I}\gal(E_i/K)$ consists of a choice of a finite $J\subseteq I$ and open neighbourhoods $U_j$ of the identity in $\gal(E_j/K)$, for all $j\in J$, and one selects the whole of $\gal(E_i/K)$ for $i\in I\setminus J$. Since the topology at each coordinate is finite discrete, that amounts to a choice of elements $\{\tau_{j,k}\}_{k=1}^{n_j}\subseteq\gal(E_j/K)$ for each $j$, where $\tau_{j,1}=1$. We make this a neighbourhood in $G$ by intersecting it with $G$: take the compositum $\hat E$ of all $E_j$, $j\in J$, and let $Q\subseteq\gal(\hat E/K)$ be the set of all $\sigma\in\gal(\hat E/K)$ for which $\sigma|_{E_j}=\tau_{j,k}$ for all $j\in J$ and some $k$. Then let $\overline{Q}$ denote all $\sigma\in G$ for which $\sigma|_{\hat E}\in Q$ - this is the corresponding basic neighbourhood of $(1)\in G$.
We can identify $\overline{Q}$ with a subset of $\gal(L/K)$. This subset is contained within the subgroup $\overline{\langle Q\rangle}$ of $\gal(L/K)$, which is the Galois group of some fixed field $F$ where $F\subseteq\hat E$, so $F/K$ is indeed a finite extension.
In the reverse direction, given a subgroup $\gal(L/F)$ we can construct a corresponding basic neighbourhood of the identity in $G$ very simply, with $J=\{j_0\}$ a singleton where $E_{j_0}\supseteq F$ and the neighbourhood induced by $U_{j_0}=\gal(E_{j_0}/F)$.
Thus, both neighbourhood bases contain one another, so the topology they induce at the identity is the same - hence the topology they induce is the same everywhere.
Is that right?