Let $L/K$ be a Galois extension of algebraic number fields with rings of integers $\mathcal{O}_L$ and $\mathcal{O}_K$ respectively.
Let $\mathfrak{p} \subset \mathcal{O}_K$ be a prime ideal and $\mathfrak{P} \subset \mathcal{O}_L$ a prime above $\mathfrak{p}$.
It can be shown that there exists an automorphism $\varphi_{\mathfrak{P}} \in \textrm{Gal}(L/K)$ satisfying
$$ \varphi_{\mathfrak{P}}(x) \equiv x^q\ (\textrm{mod}\ \mathfrak{P}) \qquad \forall x \in \mathcal{O}_L \tag{1}, $$ where $q:=\lvert \mathcal{O}_K/\mathfrak{p} \rvert$.
This is the Frobenius automorphism of $L/K$ corresponding to the prime $\mathfrak{P}$.
I want to show that the element in $\textrm{Gal}(L/K)$ satisfying $(1)$ is unique.
My idea was to assume that $\sigma, \tau \in \textrm{Gal}(L/K)$ satisfy $(1)$, then define $\upsilon:=\sigma^{-1}\circ \tau$, so that
$$ \upsilon(x) \equiv x\ (\textrm{mod}\ \mathfrak{P})\qquad \forall x \in \mathcal{O}_L. \tag{2} $$ Or in other words:
$$ \mathfrak{P} \mid \upsilon(x)-x \qquad \forall x \in \mathcal{O}_L. \tag{3} $$ Then somehow deduce from (3) that
$$ \mathfrak{P} \mid \upsilon(x)-x \qquad \forall x \in L, \tag{4} $$ from which one would conclude that $$ \upsilon(x)-x = 0 \qquad \forall x \in L, \tag{5} $$
and thus find that $\upsilon = \textrm{Id} \in \textrm{Gal}(L/K)$, and hence $\sigma = \tau$.
But as I am sure you will agree, the above is more reminiscent of wishful thinking than actual mathematics.
Does anyone know if there is a standard "book proof" of the statement, or if one might prove it along lines similar to the above?
Many thanks.
Your proof is almost correct. The problem is that the fact that you are trying to prove is false: the Frobenius element need not be unique! For example, in the extension $\mathbb Q(\sqrt{2})/\mathbb Q$, if $\mathfrak p = (2)$ and $\mathfrak P = (\sqrt 2)$, then both elements of $\mathrm{Gal}(\mathbb Q(\sqrt{2})/\mathbb Q)$ are Frobenius elements. However, if $\mathfrak P/\mathfrak p$ is unramified, then the Frobenius element will be unique and your argument is a part of the proof.
Let $D=D_{\mathfrak {P/p}} = \{\sigma\in \mathrm{Gal}(L/K):\sigma(\mathfrak P)= \mathfrak P\}$ be the decomposition group. If $\sigma \in D$, then $\sigma$ acts on $\mathcal O_L$ and fixes $\mathfrak P$, so descends to an automorphism of $\mathcal O_L/\mathfrak P$. In this way, we get a homomorphism $$D_{\mathfrak{P/p}}\to \mathrm{Gal}(\mathbb F_\mathfrak P/\mathbb F_{\mathfrak p}).$$
This map is surjective, and any element in the preimage of the Frobenius element of $\mathrm{Gal}(\mathbb F_\mathfrak P/\mathbb F_{\mathfrak p})$ is a Frobenius element in $\mathrm{Gal}(L/K)$.
The kernel of this isomorphism, called the inertia group is $$I=I_{\mathfrak{P/p}} = \{\sigma \in \mathrm{Gal}(L/K) : \sigma(x) = x\pmod {\mathfrak P}\; \forall x\in\mathcal O_L\}.$$ Note that this group being trivial is exactly what you need to be able to deduce $(5)$ from $(4)$ in your sketch proof.
However, the inertia group need not be trivial: its order is exactly $e(\mathfrak {P/p})$, the ramification index of $\mathfrak{P/p}$. Hence, the Frobenius element is unique if and only if $\mathfrak{P/p}$ is unramified.