The completion of an extension of Dedekind domains is a valuative extension

Let R ⊆ B be Dedekind domains with fraction fields K ⊆ L, and let w be a height-one prime of B lying over the height-one prime v of R. The completions K_v and L_w carry the valuative relations induced by their adic valuations, and the canonical continuous extension adicCompletionExtension : K_v →+* L_w of K → L makes L_w a K_v-algebra in the AdicCompletionExtension scope.

This file proves that this canonical map reflects and preserves the valuative relations, so that L_w is a ValuativeExtension of K_v. Local statements about valuative extensions can then be applied to the completion of a global extension through this canonical structure, rather than through an arbitrary compatible algebra or valuative relation.

Main results

• IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension_vle_iff_vle: the canonical map K_v → L_w preserves and reflects the valuative relations.
• IsDedekindDomain.HeightOneSpectrum.completionValuativeExtension: the resulting canonical ValuativeExtension K_v L_w instance, in the AdicCompletionExtension scope.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §4 and §6.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension_vle_iff_vle {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R 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] (a b : adicCompletion K v) : (adicCompletionExtension K L v w) a ≤ᵥ (adicCompletionExtension K L v w) b ↔ a ≤ᵥ b

The canonical map K_v → L_w preserves and reflects the valuative relations induced by the adic valuations.

theorem IsDedekindDomain.HeightOneSpectrum.completionValuativeExtension {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R 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] : ValuativeExtension (adicCompletion K v) (adicCompletion L w)

The completion L_w of L above v is a valuative extension of K_v, for the canonical algebra structure given by adicCompletionExtension.