Fix the proof of Frobenius map restriction

tex/alg-NT/frobenius.tex

@@ -344,6 +344,8 @@ \section{Frobenius elements behave well with restriction}
 	\Frob_{\kP} \colon L \to L \]
 and want to know how these are related.
 
+Both maps $\Frob_{\kP}$ and $\Frob_{\kp}$ induce the power-of-$p$ map in the corresponding quotient field, hence we would expect them to be naturally the same.
+
 \begin{theorem}
 	[Restrictions of Frobenius elements]
 	Assume $L/\QQ$ and $K/\QQ$ are both Galois.
@@ -352,22 +354,13 @@ \section{Frobenius elements behave well with restriction}
 	i.e.\ for every $\alpha \in K$,
 	\[ \Frob_\kp(\alpha) = \Frob_{\kP}(\alpha). \]
 \end{theorem}
-%\begin{proof}
-%	We know
-%	\[ \Frob_{\kP}(\alpha) \equiv \alpha^p \pmod{\kP}
-%		\quad \forall \alpha \in \OO_L \]
-%	from the definition.
-%	\begin{ques}
-%		Deduce that
-%		\[ \Frob_{\kP}(\alpha) \equiv \alpha^p \pmod{\kp}
-%			\quad \forall \alpha \in \OO_K. \]
-%		(This is weaker than the previous statement in two ways!)
-%	\end{ques}
-%	Thus $\Frob_{\kP}$ restricted to $\OO_K$ satisfies the
-%	characterizing property of $\Frob_\kp$.
-%\end{proof}
 \begin{proof}
-	TODO: Broken proof. Needs repair.
+	First, $K/\QQ$ is normal, so $\Frob_{\kP}$ fixes the image of $K$, that is,
+	$\Frob_{\kP} \restrict{K} \in \Gal(K/\QQ)$ is well-defined.
+
+	We have the natural map $\phi \colon \OO_K \to \OO_L \to \OO_L/\kP$, and the quotient map $q\colon \OO_K \to \OO_K / \kp$. Since $\kP \subseteq \kP$, then $\phi$ factors through $\colon$ to give a natural field homomorphism $\OO_K / \kp \to \OO_L / \kP$.
+
+	Since field homomorphism are injective, $\Frob_{\kP}$ induces the power-of-$p$ map on $\OO_L / \kP$, and everything is commutative, the theorem follows.
 \end{proof}
 In short, the point of this section is that
 \begin{moral}