Solution (source code)

= Solution

Write $G=\operatorname{Gal}(F/K)$ and
$$
D_{\mathfrak q}=\{\sigma\in G:\sigma\mathfrak q=\mathfrak q\}.
$$
Every member of this <decomposition group> preserves $\mathcal O_F$ and $\mathfrak q$, so reduction defines a homomorphism
$$
D_{\mathfrak q}\longrightarrow\operatorname{Gal}(k_{\mathfrak q}/k_{\mathfrak p}).
$$
Its kernel is the <inertia group>. We prove <surjectivity of decomposition group reduction> without presupposing a lift of Frobenius.

If the two <residue fields> coincide, surjectivity is immediate. Otherwise choose a nonzero $\overline a\in k_{\mathfrak q}$ generating it over $k_{\mathfrak p}$; a generator exists by the <primitive element theorem> for <finite fields>. Use the <Chinese remainder theorem> in $\mathcal O_F$ to choose $a$ whose residue is $\overline a$ at $\mathfrak q$ and zero at every other prime above $\mathfrak p$. Consider
$$
P(T)=\prod_{\sigma\in G}(T-\sigma a).
$$
Its coefficients are integral and fixed by $G$, hence lie in $\mathcal O_K$: an element of $K$ integral over $\mathcal O_K$ belongs to this integrally closed <ring of integers>.

Reduce at $\mathfrak q$. When $\sigma\notin D_{\mathfrak q}$, the chosen residue of $a$ at $\sigma^{-1}\mathfrak q$ is zero, so $\sigma a$ reduces to zero at $\mathfrak q$. When $\sigma\in D_{\mathfrak q}$, its residue is $\overline\sigma(\overline a)$, which is nonzero. Therefore
$$
\overline P(T)=T^{|G|-|D_{\mathfrak q}|}
\prod_{\sigma\in D_{\mathfrak q}}(T-\overline\sigma(\overline a)).
$$
Although this product is written in $k_{\mathfrak q}[T]$, its coefficients belong to $k_{\mathfrak p}$. Put $q=|k_{\mathfrak p}|$. The <finite-field Frobenius automorphism> $b\mapsto b^q$ therefore permutes its nonzero roots. In particular, $\overline a^q$ is $\overline\sigma(\overline a)$ for some $\sigma\in D_{\mathfrak q}$. Since $\overline a$ generates $k_{\mathfrak q}$, that $\overline\sigma$ agrees with Frobenius on the whole field. The <Galois group of a finite field extension> is cyclic and generated by Frobenius, so its generator lies in the image. Thus
$$
\boxed{D_{\mathfrak q}\twoheadrightarrow\operatorname{Gal}(k_{\mathfrak q}/k_{\mathfrak p}),\qquad
D_{\mathfrak q}/I_{\mathfrak q}\simeq\operatorname{Gal}(k_{\mathfrak q}/k_{\mathfrak p})}.
$$