Normalized absolute values under extension of adic completions

Let R ⊆ B be Dedekind domains with finite quotients and fraction fields K ⊆ L. For height-one primes w ∣ v, the canonical map K_v → L_w raises the residue-cardinality normalized absolute value to the local degree [L_w : K_v]. In particular, this map need not preserve the norm.

The local degree is the product of the ramification index and inertia degree, as in IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletion; the residue cardinalities are related by IsDedekindDomain.HeightOneSpectrum.natCard_residueField_adicCompletion_eq_pow_inertiaDeg.

Main results

• IsDedekindDomain.HeightOneSpectrum.norm_adicCompletionExtension: the normalized absolute value under the canonical extension of completions.
• IsDedekindDomain.HeightOneSpectrum.norm_norm_adicCompletion: the field norm preserves normalized absolute values. This uses TauCeti.normalizedValuationWithZero_norm together with the residue-cardinality formula.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §8.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.norm_adicCompletionExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] [Ring.HasFiniteQuotients B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : adicCompletion K v) : ‖(adicCompletionExtension K L v w) x‖ = ‖x‖ ^ Module.finrank (adicCompletion K v) (adicCompletion L w)

The normalized absolute value of the image in L_w is the normalized absolute value in K_v raised to the local degree [L_w : K_v]. No Galois hypothesis is needed.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.norm_norm_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] [Ring.HasFiniteQuotients B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] (x : adicCompletion L w) : ‖(Algebra.norm (adicCompletion K v)) x‖ = ‖x‖

The field norm between adic completions preserves the residue-cardinality normalized absolute value. This differs from extension of scalars, which raises it to the local degree.