Continuity of map of local fields K_v -> L_w coming from number fields

[kbuzzard]

Let A be a Dedekind domain with field of fractions K, let L/K be a finite separable extension and let B be the integral closure of A in L.

If w is a finite place of L lying over v of K, then the map K -> L "obviously" extends to a map of completions K_v -> L_w. At the time of writing, Andrew Yang has reduced this claim to the assertion about the relationship between the v-adic and w-adic valuations on K, which should easily follow from IsDedekindDomain.HeightOneSpectrum.valuation_comap. The goal of this issue is to check this, i.e. to assume valuation_comap and fill in the sorry in adicCompletion_comap_ringHom in the file FLT.DededkindDomain.FiniteAdeleRing.BaseChange. It should hopefully be a relatively straightforward wrestle with WithZero (Multiplicative ℤ).

[YaelDillies]

claim

[YaelDillies]

propose #215