Extension of a $p$-adic completion $K_v \to L_w$ along a finite extension of number fields

Let $p$ be a prime, let $K \subseteq L$ be number fields ($L$ an algebra over $K$), and let $v$ be a prime of $K$ above $p$. The statement asserts that there is a prime $w$ of $L$ above $p$ and a ring homomorphism

between the completions such that

1. $\iota$ is compatible with the inclusions: $\iota(x) = x$ for every $x \in K$, where $x$ is viewed in $K_v$ on the left and in $L \subseteq L_w$ on the right, and
2. there is a real constant $c > 0$ with $\|\iota(x)\|_w = \|x\|_v^{\,c}$ for all $x \in K_v$.

This is the existence of an extension of the $v$-adic absolute value of $K$ to $L$: the prime $w$ lies above $v$, the inclusion $K \to L$ is uniformly continuous for the $v$-adic and $w$-adic topologies because the valuations satisfy $|x|_w = |x|_v^{e(w|v)}$ on $K$, and it extends to the completions. The exponent $c$ is a positive integer determined by the ramification index and the normalizations of the two absolute values; only its positivity is used, so it is stated as an existential real number.

Use. Statements proved in $L_w$ (for instance Brumer's theorem for the field $L = K(\zeta_n)$) are transported to $K_v$ through $\iota$; the norm relation makes $\iota$ continuous and sends the ball $\|x - 1\|_v \le \|p\|_v^2$ into the ball $\|y - 1\|_w \le \|p\|_w^2$, so $\iota$ commutes with the $p$-adic logarithm (PadicLog.map_log). This is a step of the reduction of Leopoldt.exists_linearIndependent_log_conj_of_brumer.

Formalization Note. $K_v$ is v.1.adicCompletion K, with the norm of Definitions.Def_PrimesOverNorm (the one that makes $\|p\|_v < 1$). w is tied to v only through the compatibility of ι with the two algebraMaps. Mathlib (at this revision) has no ring homomorphism between adic completions of a finite extension; the building blocks are IsDedekindDomain.HeightOneSpectrum.valuation_liesOver, IsDedekindDomain.HeightOneSpectrum.uniformContinuous_algebraMap_liesOver, UniformSpace.Completion.mapRingHom and IsDedekindDomain.HeightOneSpectrum.adicCompletion.equiv; the infinite-place analogue NumberField.InfinitePlace.completionMap is a template. ‖x‖ ^ c with real c is the real power.