How to define a morphism $\varphi:L\otimes_K\hat K\to\prod_i \hat L_i$ from completion of finite field extensions Let $L/K$ be a degree $n$ extension of fields, where $K$ has discrete valuation $v$, which can be prolonged to the discrete valuations $w_i$ on $L$. We can therefore define the completion of $K$ w.r.t. $v$ to be $\hat K$, and the completion of $L$ w.r.t. $w_i$ to be $\hat L_i$, then in Theorem II.3.1 of Serre's Local Fields, we have a homomorphism $$\varphi:L\otimes_K\hat K\to\prod_i\hat L_i$$which we then show to be an isomorphism. However, I don't see how this morphism is defined in the first place.
 A: The basic idea is to take $L$ to be $K[\alpha]\cong K[x]/(f(x))$ where $f(x)$ is the minimum polynomial of $\alpha$.  Then $L\otimes_K\hat K \cong K[x]/(f(x))\otimes_K\hat K \cong \hat K[x]/(f(x))$ and factor $f(x)$ in $\hat K[x]$.
A: In order to define the canonical morphism $\varphi:L\otimes_K\hat K\to\prod_i\hat L_i$, we will make use of the completion functor $\mathrm{comp}:\mathbf{DVF}\to\mathbf{DVF}$ acting on the category of discretely valued fields, with continuous field embeddings (that is to say, field extensions that prolong the discrete valuation) as morphisms. Then since we have a natural transformation $\mathrm{id}_{\mathbf{DVF}}\to\mathrm{comp}$ given by inclusion in the completion, we obtain the following commutative diagram:
$$
\require{AMScd}
\begin{CD}
(K,v) @>>> (\hat{K},\hat{v})\\
@VVV @VVV \\
(L,w_i) @>>> (\hat{L}_i,\hat{w}_i)
\end{CD}
$$
which allows us to define a ring morphism $\varphi:L\otimes_K \hat{K}\to\hat{L}_i$ for all $i$, which is $\hat{K}$-linear by construction. This gives us the morphism $$\varphi:L\otimes_K\hat K\to\prod_i\hat L_i.$$
