I wish to prove the existence of the Frobenius automorphism of an extension of algebraic number fields.
Let $E/K$ be a normal extension of algebraic number fields and let $\mathfrak{P} \subset \mathcal{O}_L$ be a prime ideal that does not ramify over $K$. Then there is a unique $K$-automorphism $\sigma_{\mathfrak{P}} \in \textrm{Gal}(E/K)$ satisfying: \begin{equation} \sigma_{\mathfrak{P}}(\alpha) \equiv \alpha^q\ (\textrm{mod}\ \mathfrak{P}) \qquad \forall \alpha \in \mathcal{O}_L \end{equation} with $q = [\mathcal{O}_E/\mathfrak{P} : \mathcal{O}_K/\mathfrak{p}]$. The decomposition group $G_{\mathfrak{P}} < G$ is cyclic and generated by $\sigma_{\mathfrak{P}}$ - the Frobenius automorphism.
I am aware of the existence of the Frobenius automorphism in the Galois group of an extension of finite fields:
Let $q=p^n$, $n,p \in \mathbb{N}$, $p$ prime, and let $\mathbb{F}_q$ and $\mathbb{F}_p$ be the unique finite fields with cardinality $q$ and $p$ respectively. Then $\mathbb{F}_q / \mathbb{F}_p$ is a Galois extension, and there exists an automorphism $\sigma \in \textrm{Gal}(\mathbb{F}_q / \mathbb{F}_p)$ satisfying $\sigma(\alpha)=\alpha^p$ for all $\alpha \in \mathbb{F}_q$.
Showing that $\sigma$, as defined above, is an automorphism, is simple. But here the behaviour of $\sigma$ on the entirety of $\mathbb{F}_q$ is given.
The problem in the case of number fields is that if we want $\sigma_{\mathfrak{P}} \in \textrm{Gal}(E/K)$ to satisfy \begin{equation} \sigma_{\mathfrak{P}}(\alpha) \equiv \alpha^q\ (\textrm{mod}\ \mathfrak{P}) \qquad \forall \alpha \in \mathcal{O}_L \end{equation} how can we control its behaviour on the rest of $L$ and ensure that $\sigma_{\mathfrak{P}}$ indeed is an automorphism on $L$?
The above appears as exercise 2 of chap. I §9 of J. Neukirch's $\textit{Algebraische Zahlentheorie}$.
$\textbf{Addendum:}$ I spent months trying to figure this out. It turns out there is a typo. See here.
Let $G_{\mathfrak{P}}$ be the corresponding decomposition group. We have a quotient morphism $q: G_{\mathfrak{P}} \rightarrow Gal((\mathcal{O}_E/\mathfrak{P})/(\mathcal{O}_K/\mathfrak{p}))$ and we want to prove it is an isomorphism.
Now, $G$ acts transitively over the set of prime ideals of $E$ above $\mathfrak{p}$. Let $r$ denote the cardinality of this set, and $G_{\mathfrak{P}}$ is the stabilizer of $\mathfrak{P}$.
Standard group action theory yields $|G_{\mathfrak{P}}|=|G|/r=[E:K]/r$. By standard study of number field extensions, and because there is no ramification, $[E:K]=r[(\mathscr{O}_E/\mathfrak{P}):(\mathcal{O}_K/\mathfrak{p})]$, so $q$ is a group morphism between two groups of same cardinality.
Therefore, we want to show that $q$ is injective, and we are done.
So let $\sigma \in G_{\mathfrak{P}}$ be in the kernel of $\sigma$: then $\sigma$ moves elements of $\mathcal{O}_E$ by elements of $\mathfrak{p}\mathcal{O}_E$. Assume that $\sigma \neq id$.
Let $n \geq 1$ be maximal such that for each $x \in \mathcal{O}_E$, $\sigma(x)-x \in \mathfrak{p}^n\mathcal{O}_E$.
Let $p$ be a uniformizer in $K$ for $\mathfrak{p}$, it is a uniformizer for $E$ and $\mathfrak{P}$ as well. Define, for $x \in \mathcal{O}_E$, $\tau(x)=\frac{\sigma(x)-x}{p^n} \in \mathcal{O}_E$. It is easy to see that $x \in \mathcal{O}_E^{\times} \longmapsto \tau(x)/x \in \mathcal{O}_E$ induces, by quotient, a morphism $(\mathcal{O}_E/\mathfrak{P})^{\times} \rightarrow \mathcal{O}_E/\mathfrak{P}$.
Because the cardinals are coprime, this morphism must be trivial, that is, $\sigma(x) \in x+p^n\mathfrak{P}$ for each $x \in \mathcal{O}_E^{\times}$. By multiplying by $p$ enough times, it follows that $(\sigma-id)(\mathcal{O}_E) \subset \mathfrak{p}^{n+1}$, a contradiction.
Therefore $q$ is injective and we are done.