Canonical maps between number-field completions

Let L/K be an extension of number fields, and let w be a finite place of L above a finite place v of K. The embedding K → L extends uniquely to a continuous map K_v → L_w. This file packages that map as the algebra homomorphism completionAlgHom, provides the algebra and topological scalar structures it induces in the AdicCompletionExtension scope, and proves its compatibility in towers.

The underlying continuous ring homomorphism is IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension. Packaging it over K is what makes the completion map usable by scalar extension and tensor-product constructions without choosing an unrelated algebra structure on L_w over K_v.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.completionAlgHom: the canonical K-algebra homomorphism K_v → L_w.

Main results

• IsDedekindDomain.HeightOneSpectrum.continuous_completionAlgHom: continuity of the canonical map.
• IsDedekindDomain.HeightOneSpectrum.eq_completionAlgHom_of_continuous: its continuous universal property.
• IsDedekindDomain.HeightOneSpectrum.completionAlgHom_comp: compatibility in a tower of number fields.
• IsDedekindDomain.HeightOneSpectrum.completionAlgHom_vle_iff_vle: the canonical map preserves and reflects the valuative relations of the completions.

In the AdicCompletionExtension scope, L_w is moreover a ValuativeExtension of K_v (completionValuativeExtension), and Mathlib's finiteness instance for completions of number fields applies to the canonical algebra structure, so Module.Finite K_v L_w holds for it by instance search.

References

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

noncomputable def IsDedekindDomain.HeightOneSpectrum.completionAlgHom {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : adicCompletion K v →ₐ[K] adicCompletion L w

The canonical map K_v → L_w for a finite place w of L above a finite place v of K, as a K-algebra homomorphism.

Equations

• v.completionAlgHom w = { toRingHom := IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension K L v w, commutes' := ⋯ }

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_eq_completionAlgHom {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : algebraMap (adicCompletion K v) (adicCompletion L w) = (v.completionAlgHom w).toRingHom

The algebra map of the canonical completion algebra is completionAlgHom.

theorem IsDedekindDomain.HeightOneSpectrum.continuous_completionAlgHom {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Continuous ⇑(v.completionAlgHom w)

The canonical map between completions is continuous.

theorem IsDedekindDomain.HeightOneSpectrum.eq_completionAlgHom_of_continuous {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (f : adicCompletion K v →+* adicCompletion L w) (hf : Continuous ⇑f) (hcomp : ∀ (x : K), f ((algebraMap K (adicCompletion K v)) x) = (algebraMap L (adicCompletion L w)) ((algebraMap K L) x)) : f = (v.completionAlgHom w).toRingHom

A continuous ring homomorphism K_v → L_w extending K → L is the canonical completion map.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.completionAlgHom_self {K : Type u_1} [Field K] [NumberField K] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) : have x := ⋯; v.completionAlgHom v = AlgHom.id K (adicCompletion K v)

The canonical map from a completion to itself is the identity.

theorem IsDedekindDomain.HeightOneSpectrum.completionIsScalarTower {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : IsScalarTower K (adicCompletion K v) (adicCompletion L w)

The global field, its completion, and the completion of an extension form a scalar tower for the canonical completion algebra.

theorem IsDedekindDomain.HeightOneSpectrum.completionContinuousSMul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : ContinuousSMul (adicCompletion K v) (adicCompletion L w)

Scalar multiplication by K_v on L_w is continuous for the canonical completion algebra.

theorem IsDedekindDomain.HeightOneSpectrum.completionAlgHom_comp {K : Type u_1} [Field K] [NumberField K] {M : Type u_2} {L : Type u_3} [Field M] [NumberField M] [Algebra K M] [Field L] [NumberField L] [Algebra K L] [Algebra M L] [IsScalarTower K M L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (u : HeightOneSpectrum (NumberField.RingOfIntegers M)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [u.asIdeal.LiesOver v.asIdeal] [w.asIdeal.LiesOver u.asIdeal] : (AlgHom.restrictScalars K (u.completionAlgHom w)).comp (v.completionAlgHom u) = v.completionAlgHom w

Canonical completion maps compose in a tower of number fields.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.completionAlgHom_vle_iff_vle {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (a b : adicCompletion K v) : (v.completionAlgHom w) a ≤ᵥ (v.completionAlgHom w) b ↔ a ≤ᵥ b

The canonical map between completions preserves and reflects the valuative relations induced by the adic valuations.