Adic valuations and completions transport along an isomorphism of Dedekind domains

An isomorphism e : R ≃+* R' of Dedekind domains induces an isomorphism σ = IsFractionRing.ringEquivOfRingEquiv e : K ≃+* K' of their fraction fields, and carries a height one prime v of R to the height one prime of R' with underlying ideal Ideal.map e v.asIdeal. This file proves that σ intertwines the two adic valuations: for a height one prime w of R' with w.asIdeal = Ideal.map e v.asIdeal,

w.valuation K' (σ f) = v.valuation K f

for every f : K. Equivalently, ord at w of σ f is ord at v of f, which is the algebraic content of the Galois descent div (σ f) = σ_* (div f) for divisors on a curve.

A field isomorphism σ : K ≃+* K' with this property is an isometry for the two adic valuations, so it extends by continuity to an isomorphism of adic completions adicCompletionCongr v w σ hσ : K_v ≃+* K'_w. For a Galois extension of global fields this is how an automorphism permuting the places above a given place acts on their completions.

Main results

• IsDedekindDomain.HeightOneSpectrum.intValuation_ringEquiv and IsDedekindDomain.HeightOneSpectrum.valuation_ringEquivOfRingEquiv: the integer-valued and the fraction-field adic valuations transport.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr: the induced isomorphism of adic completions, with adicCompletionCongr_algebraMap (it extends σ), continuous_adicCompletionCongr, its universal property eq_adicCompletionCongr_of_continuous, its identity, composition, and inverse laws, and valued_adicCompletionCongr (it preserves the valuations).

The ideal-level input this rests on — that Ideal.map e preserves divisibility and factorisation multiplicities, and that Mathlib's equivOfRingEquiv is Ideal.map e on underlying ideals — is not valuation theory and lives in TauCeti/RingTheory/DedekindDomain/Ideal.lean.

Implementation notes

The hypothesis on the two primes is stated as the equation w.asIdeal = Ideal.map e v.asIdeal rather than as w = equivOfRingEquiv e v, so that a call site holding some independently constructed w — a place of a curve, say — does not first have to identify it with the transport. asIdeal_equivOfRingEquiv discharges the hypothesis whenever w is that transport, so nothing is lost in the other direction.

valuation_ringEquivOfRingEquiv_algebraMap is private: it is the algebraMap special case used to reduce the general statement to a quotient of two elements of R, and the reusable restriction result is intValuation_ringEquiv.

Provenance

Adapted from AINTLIB (Apache-2.0), commit 513e83879e2f, projects/HasseWeil/HasseWeil/WeilPairing/DivisorGalois.lean: the proofs of intValuation_map_ringEquiv, valuation_map_ringEquiv_algebraMap and valuation_map_ringEquiv are that file's, with the vocabulary adapted to this repository's interfaces. The ideal-level lemmas adapted from the same source are attributed in TauCeti/RingTheory/DedekindDomain/Ideal.lean. The completion section is not from that source; it follows the pattern of adicCompletionExtension in TauCeti/RingTheory/DedekindDomain/AdicCompletionExtension.lean.

References

• J. H. Silverman, The Arithmetic of Elliptic Curves, II.3 (the Galois action on divisors).

theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] (e : R ≃+* R') {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} (hvw : w.asIdeal = Ideal.map e v.asIdeal) (r : R) : w.intValuation (e r) = v.intValuation r

The integer adic valuation transports along a ring isomorphism. If the height one prime w of R' is the image of the height one prime v of R under e, then the w-adic valuation of e r is the v-adic valuation of r.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_ringEquivOfRingEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] (e : R ≃+* R') {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} (hvw : w.asIdeal = Ideal.map e v.asIdeal) (f : K) : (valuation K' w) ((IsFractionRing.ringEquivOfRingEquiv e) f) = (valuation K v) f

The adic valuation of the fraction field transports along a ring isomorphism. With σ = IsFractionRing.ringEquivOfRingEquiv e the induced isomorphism of fraction fields, and w the image of v under e, the w-adic valuation of σ f is the v-adic valuation of f. This is the algebraic engine of divisor Galois descent.

theorem IsDedekindDomain.HeightOneSpectrum.uniformContinuous_withValCongr {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] (v : HeightOneSpectrum R) (w : HeightOneSpectrum R') (σ : K ≃+* K') (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) : UniformContinuous ⇑(WithVal.congr (valuation K v) (valuation K' w) σ)

A field isomorphism carrying the v-adic valuation to the w-adic valuation is uniformly continuous for the two adic uniformities.

noncomputable def IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] (v : HeightOneSpectrum R) (w : HeightOneSpectrum R') (σ : K ≃+* K') (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) : adicCompletion K v ≃+* adicCompletion K' w

The isomorphism of adic completions K_v ≃+* K'_w extending a field isomorphism σ : K ≃+* K' that carries the v-adic valuation to the w-adic valuation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.toCompletion_adicCompletionCongr {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) (x : adicCompletion K v) : ((v.adicCompletionCongr w σ hσ) x).toCompletion = UniformSpace.Completion.map (⇑(WithVal.congr (valuation K v) (valuation K' w) σ)) x.toCompletion

On the underlying uniform-space completions, adicCompletionCongr is the completion of σ.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr_algebraMap {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) (x : K) : (v.adicCompletionCongr w σ hσ) ((algebraMap K (adicCompletion K v)) x) = (algebraMap K' (adicCompletion K' w)) (σ x)

adicCompletionCongr extends σ.

theorem IsDedekindDomain.HeightOneSpectrum.continuous_adicCompletionCongr {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) : Continuous ⇑(v.adicCompletionCongr w σ hσ)

adicCompletionCongr is continuous.

theorem IsDedekindDomain.HeightOneSpectrum.eq_adicCompletionCongr_of_continuous {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) {f : adicCompletion K v →+* adicCompletion K' w} (hf : Continuous ⇑f) (hfK : ∀ (x : K), f ((algebraMap K (adicCompletion K v)) x) = (algebraMap K' (adicCompletion K' w)) (σ x)) : f = (v.adicCompletionCongr w σ hσ).toRingHom

adicCompletionCongr is the only continuous ring homomorphism K_v →+* K'_w extending σ.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {v : HeightOneSpectrum R} : v.adicCompletionCongr v 1 ⋯ = RingEquiv.refl (adicCompletion K v)

adicCompletionCongr for the identity is the identity.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr_trans {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) {R'' : Type u_5} {K'' : Type u_6} [CommRing R''] [IsDedekindDomain R''] [Field K''] [Algebra R'' K''] [IsFractionRing R'' K''] (u : HeightOneSpectrum R'') (τ : K' ≃+* K'') (hτ : ∀ (y : K'), (valuation K'' u) (τ y) = (valuation K' w) y) : (v.adicCompletionCongr w σ hσ).trans (w.adicCompletionCongr u τ hτ) = v.adicCompletionCongr u (σ.trans τ) ⋯

Transporting completions along two field isomorphisms is transport along their composite.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionCongr_symm {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) : (v.adicCompletionCongr w σ hσ).symm = w.adicCompletionCongr v σ.symm ⋯

The inverse of adicCompletionCongr is the completion of the inverse isomorphism.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionCongr {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] {K : Type u_3} {K' : Type u_4} [Field K] [Field K'] [Algebra R K] [IsFractionRing R K] [Algebra R' K'] [IsFractionRing R' K'] {v : HeightOneSpectrum R} {w : HeightOneSpectrum R'} {σ : K ≃+* K'} (hσ : ∀ (x : K), (valuation K' w) (σ x) = (valuation K v) x) (x : adicCompletion K v) : Valued.v ((v.adicCompletionCongr w σ hσ) x) = Valued.v x

adicCompletionCongr preserves the valuations of the completions.