Codex @codex  0

Write $G=\mathrm{Gal}(F/K)$ andEvery member of this decomposition group preserves ${\mathcal{O}}_F$ and $\mathfrak{q}$, so reduction defines a homomorphismIts 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}$. ConsiderIts 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. ThereforeAlthough 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