Solution (source code)

= Solution

Let $\mathcal G=\operatorname{Gal}(M_\infty/F)$. The <Galois group> sequence is
$$
1\longrightarrow X\longrightarrow\mathcal G\longrightarrow\Gamma\longrightarrow1.
$$
For $g\in\Gamma$ and $x\in X$, choose a lift $\widetilde g\in\mathcal G$ and define
$$
g\cdot x=\widetilde g\,x\,\widetilde g^{-1}.
$$
This is independent of the lift because $X$ is abelian. Write $X$ additively. As an abelian <pro-p group>, it is a compact $\mathbb Z_p$-<module>, with $a x$ defined by the limit of integer powers, and the conjugation action is continuous and $\mathbb Z_p$-linear. It extends to the <Iwasawa algebra>
$$
\Lambda=\mathbb Z_p[[\Gamma]]
=\varprojlim_{r,n}(\mathbb Z/p^r\mathbb Z)[\Gamma/\Gamma^{p^n}].
$$
Indeed, use the finite quotients of $X$ obtained by intersecting it with open normal subgroups of $\mathcal G$; on each quotient the action factors through one of these finite group rings. This defines the natural <compact Galois module> structure, even when $X$ is not finitely generated. Choosing $\gamma$ identifies $\Lambda$ with $\mathbb Z_p[[T]]$ through $T=\gamma-1$.

The subgroup $(\gamma-1)X$ is closed: it is the image of the compact group $X$ under a continuous map. Every element $(\gamma-1)x$ is a <commutator> of a lift of $\gamma$ with $x$. Consequently
$$
(\gamma-1)X\subseteq\overline{[\mathcal G,\mathcal G]}.
$$
Conversely, in the quotient by $(\gamma-1)X$, the lift of $\gamma$ centralizes the image of $X$. Its powers are dense in the procyclic subgroup they generate. Since these powers map densely onto $\Gamma$, compactness shows that $\mathcal G$ is generated by $X$ and that procyclic subgroup. The quotient is therefore abelian. Hence
$$
\boxed{\overline{[\mathcal G,\mathcal G]}=(\gamma-1)X.}
$$
One can also see this by choosing a lift of $\gamma$. Since $\mathcal G$ is a <pro-p group>, the closed subgroup generated by this lift is $\mathbb Z_p$, and its map to $\Gamma$ is an isomorphism. This gives a <semidirect product> splitting.

The maximal abelian subextension $M/F$ is the fixed field of the closed <commutator subgroup>. Because $F_\infty/F$ is abelian, $F_\infty\subseteq M$. Restriction of the <Galois correspondence> to $X$ now gives the \b[coinvariant formula]
$$
\boxed{\operatorname{Gal}(M/F_\infty)\cong X/(\gamma-1)X=X_\Gamma.}
$$
The closed image above is important: the formula is a quotient of compact groups, not a quotient by an unclosed abstract subgroup. This is <abelianization over a Zp-extension>.