Frobenius automorphism and cyclotomic extension There is a lemma from a lecture I attended where I scribbled down notes and try to make sense of the proof afterwards and there is a spot at which I am stuck. First I have to set up some notations and refresh memory on Frobenius element.
Let $l,p$ be distinct odd primes, $L = \mathbb{Q}(\zeta_l)$, $K$ be the unique quadractic subfield contained in $L$. (To see what $K$ is, we know that $Gal(L/\mathbb{Q}) =(\mathbb{Z}/l\mathbb{Z})^*$ has a unique subgroup $H$ of index 2, and by Galois theory, $K$ would then be $L^H$).
By definition, $Frob_p$ is defined as follows. We know $p$ is unramified in $L$. If $\mathfrak{q}\subseteq O_L$ is any prime ideal containing $p\cdot O_L$, then the decomposition group at $\mathfrak{q}$ defined as $G_\mathfrak{q}:=\{\sigma\in Gal(L/\mathbb{Q}) : \sigma(\mathfrak{q})=\mathfrak{q}\}$ is isomorphic to $Gal((O_L/\mathfrak{q})/\mathbb{F}_p)$. The latter has Frobenius element $x\mapsto x^p$. The corresponding element in $G_\mathfrak{q}$ is denoted $Frob_p$. Note that $Frob_p$ does not depend on the choice of $\mathfrak{q}$ because the extension is Abelian.
Lemma: $Frob_p\in Gal(L/\mathbb{Q})$ is in $H$ if and only if $p$ splits in $K$.
Proof: Let $\mathfrak{p}_1 \subseteq O_K$ be a prime factor of $p\cdot O_K$. Then $Frob_p\in H$ $\Leftrightarrow$ $Frob_p$ acts trivially on $O_K$ $\Leftrightarrow$ $x\mapsto x^p$ is identity on $O_K/\mathfrak{p}_1$ $\Leftrightarrow$ $O_K/\mathfrak{p}_1 = \mathbb{F}_p$ $\Leftrightarrow$ $p$ splits in $K$.
The line that I do not get is "$Frob_p$ acts trivially on $O_K$ $\Leftrightarrow$ $x\mapsto x^p$ is identity on $O_K/\mathfrak{p}_1$". I think I have the forward implication, but could someone enlighten me on the backward implication?
 A: I think you're missing the following useful observation:  $Frob_p$ is characterized by the property $Frob_p x \equiv x^p \pmod{\mathfrak{q}}$ for all $x$ in $O_L$.  That $Frob_p$ has this property follows from your definition.  To see that it is determined among all automorphisms of $L$ by this property, note that if for some automorphism $\sigma$ of $L$ we have $\sigma x \equiv x^p \pmod{\mathfrak{q}}$, then letting $x$ be in $\mathfrak{q}$, we see that $\sigma$ fixes $\mathfrak{q}$, hence is in the decomposition group of $\mathfrak{q}$.  Now as you point out, this group is isomorphic to the Galois group of $O_L/\mathfrak{q}$ over $\mathbb{F}_p$, so there is a unique such automorphism that acts as Frobenius.
Examine the above paragraph and note that nothing depends on the upper field being $L$ -- it could be any abelian extension of $\mathbb{Q}$.  In particular, there is a $Frob_p$ automorphism of $K/\mathbb{Q}$.  In fact, by the above characterization, this $Frob_p$ is the restriction to $K$ of the $Frob_p$ for $L/\mathbb{Q}$.
$\implies$: Choose the $\mathfrak{q}$ to lie above $\mathfrak{p}_1$.  If $Frob_p$ acts trivially on $O_K$, then the $Frob_p$ for $K/\mathbb{Q}$ is the identity automorphism.  In particular, $x = Frob_p x \equiv x^p \pmod{\mathfrak{p}_1}$ for all $x$ in $O_K$, so $x \mapsto x^p$ is the identity on $O_K/\mathfrak{p}_1$.
$\impliedby$: If $x \mapsto x^p$ is the identity on $O_K/\mathfrak{p}_1$, then the identity automorphism of $K$ has the property that characterizes the $Frob_p$ for $K/\mathbb{Q}$.  Thus, this $Frob_p$ is the identity on $K$, so the $Frob_p$ for $L$ is trivial on $O_K$.
