The valuative relation on an adic completion

Let R be a Dedekind domain with fraction field K and let v be a height-one prime of R. The completion K_v already carries the adic valuation Valued.v, with values in ℤᵐ⁰. This file equips K_v with the valuative relation that valuation induces, checks that its existing topology is the valuative topology and that the relation is nontrivial, and identifies the ring of integers and the residue field of the valuative relation with the ones K_v already has. When K_v is a nonarchimedean local field, the steps of its unit filtration are read off from Valued.v.

Main results

• IsDedekindDomain.HeightOneSpectrum.not_isSquare_adicCompletion_of_valuation_eq_exp_of_not_even: an element of odd order of vanishing at v is a nonsquare in the completion, which is the form a prime of a prescribed modulus supplies; the value of an element in the multiplicative value group of the adic valuation is read off through IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_eq_one_iff in TauCeti.RingTheory.DedekindDomain.AdicValuation.Basic.

• IsDedekindDomain.HeightOneSpectrum.integer_eq_adicCompletionIntegers: the ring of integers of the valuative relation is 𝒪_v; mem_adicCompletionIntegers_iff_valuation_le_one is the membership form, valuation_integers_adicCompletionIntegers packages it as Valuation.Integers, and mem_maximalIdeal_integer_pow_iff reads the powers of its maximal ideal as valuation bounds.

• IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletion: the residue field of the valuative relation is R ⧸ v; residueFieldEquivAdicCompletion_apply_mk describes it on a quotient representative.

• IsDedekindDomain.HeightOneSpectrum.natCard_residueField_adicCompletion_eq_absNorm: when R is infinite, that residue field has Ideal.absNorm v.asIdeal elements.

• IsDedekindDomain.HeightOneSpectrum.isNonarchimedeanLocalField_adicCompletion: an adic completion with finite residue field is a nonarchimedean local field.

• IsDedekindDomain.HeightOneSpectrum.normalizedValuationWithZero_adicCompletion: the zero-preserving normalized valuation of such a completion is the inverse of its adic valuation.

• IsDedekindDomain.HeightOneSpectrum.compactSpace_adicCompletionIntegers: the local integer ring of an adic completion carrying a nonarchimedean local-field structure is compact.

• IsDedekindDomain.HeightOneSpectrum.mem_unitFiltration_adicCompletion_iff: the unit filtration U(K_v, n) consists of the units u of 𝒪_v with Valued.v (u - 1) ≤ exp (-n); its depth-zero step is Valued.v u = 1 (mem_unitFiltration_zero_adicCompletion_iff), which unitsMap_algebraMap_mem_unitFiltration_zero_iff reads on the units of K.

Implementation notes

The valuative relation is the one induced by Valued.v, so Valued.v is Valuation.Compatible with it and the generic comparison lemmas Valuation.vle_iff_le and Valuation.vle_one_iff translate between the two languages; no comparison API specific to K_v is introduced.

The residue-field comparison rests on residueFieldEquivAdicCompletionIntegers, which compares R ⧸ v with the residue field of 𝒪_v; only the passage from 𝒪_v to the ring of integers of the valuative relation is added here.

@[instance_reducible]

noncomputable instance IsDedekindDomain.HeightOneSpectrum.instValuativeRelAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ValuativeRel (adicCompletion K v)

The valuative relation on an adic completion induced by its canonical adic valuation.

Equations

• v.instValuativeRelAdicCompletion = ValuativeRel.ofValuation Valued.v

instance IsDedekindDomain.HeightOneSpectrum.instCompatibleValuedAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Valued.v.Compatible

The canonical adic valuation is compatible with the valuative relation it induces.

instance IsDedekindDomain.HeightOneSpectrum.isValuativeTopologyAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsValuativeTopology (adicCompletion K v)

The topology of an adic completion is induced by its canonical valuative relation.

instance IsDedekindDomain.HeightOneSpectrum.isNontrivialAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ValuativeRel.IsNontrivial (adicCompletion K v)

The canonical valuative relation on an adic completion is nontrivial.

theorem IsDedekindDomain.HeightOneSpectrum.integer_eq_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (ValuativeRel.valuation (adicCompletion K v)).integer = (adicCompletionIntegers K v).toSubring

The ring of integers of the valuative relation is the canonical ring of integers 𝒪_v.

noncomputable def IsDedekindDomain.HeightOneSpectrum.integerEquivAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ↥(ValuativeRel.valuation (adicCompletion K v)).integer ≃+* ↥(adicCompletionIntegers K v)

The ring of integers of the valuative relation of K_v is the canonical ring of integers 𝒪_v, as a ring isomorphism: the two are the same subring of K_v, carrying different instances. The codomain is written as v.adicCompletionIntegers K and not as its toSubring, whose coercion is the same type but carries no IsLocalRing instance.

Equations

• v.integerEquivAdicCompletionIntegers = RingEquiv.subringCongr ⋯

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_integerEquivAdicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : ↥(ValuativeRel.valuation (adicCompletion K v)).integer) : ↑(v.integerEquivAdicCompletionIntegers x) = ↑x

The identification of the two rings of integers is the identity on elements of K_v.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_integerEquivAdicCompletionIntegers_symm {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : ↥(adicCompletionIntegers K v)) : ↑(v.integerEquivAdicCompletionIntegers.symm x) = ↑x

The inverse identification of the two rings of integers is the identity on elements of K_v.

theorem IsDedekindDomain.HeightOneSpectrum.mem_maximalIdeal_integer_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) {x : ↥(ValuativeRel.valuation (adicCompletion K v)).integer} {n : ℕ} : x ∈ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation (adicCompletion K v)).integer ^ n ↔ Valued.v ↑x ≤ WithZero.exp (-↑n)

An element of the ring of integers of the valuative relation on K_v lies in the n-th power of its maximal ideal exactly when its valuation is at most exp (-n). This is mem_maximalIdeal_pow_iff, read through integerEquivAdicCompletionIntegers.

theorem IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers_iff_valuation_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : adicCompletion K v) : x ∈ adicCompletionIntegers K v ↔ (ValuativeRel.valuation (adicCompletion K v)) x ≤ 1

An element of K_v lies in 𝒪_v exactly when the valuation of the valuative relation is at most 1. This is Mathlib's mem_adicCompletionIntegers, which is stated for the adic valuation Valued.v, read through the valuative relation.

theorem IsDedekindDomain.HeightOneSpectrum.valuation_integers_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : (ValuativeRel.valuation (adicCompletion K v)).Integers ↥(adicCompletionIntegers K v)

𝒪_v is a ring of integers of K_v. The canonical ring of integers satisfies Valuation.Integers for the valuation of the valuative relation of K_v, which is the form in which the theory of local fields consumes a ring of integers.

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_mem_integer_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : R) : (algebraMap R (adicCompletion K v)) a ∈ (ValuativeRel.valuation (adicCompletion K v)).integer

An element of R lands in the ring of integers of the valuative relation on K_v.

noncomputable def IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : R ⧸ v.asIdeal ≃+* IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer

The residue field of the valuative relation on K_v is the residue field R ⧸ v of v.

Equations

• v.residueFieldEquivAdicCompletion = v.residueFieldEquivAdicCompletionIntegers.trans (IsLocalRing.ResidueField.mapEquiv v.integerEquivAdicCompletionIntegers.symm)

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.residueFieldEquivAdicCompletion_apply_mk {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : R) : v.residueFieldEquivAdicCompletion ((Ideal.Quotient.mk v.asIdeal) a) = (IsLocalRing.residue ↥(ValuativeRel.valuation (adicCompletion K v)).integer) ⟨(algebraMap R (adicCompletion K v)) a, ⋯⟩

The residue-field equivalence on a quotient representative. This is the characterization consumers should use; the construction of the equivalence is an implementation detail and should not be unfolded.

theorem IsDedekindDomain.HeightOneSpectrum.natCard_residueField_adicCompletion_eq_absNorm {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Infinite R] : Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation (adicCompletion K v)).integer) = Ideal.absNorm v.asIdeal

If R is infinite, the residue field of K_v has cardinality the absolute norm of v.

instance IsDedekindDomain.HeightOneSpectrum.isNonarchimedeanLocalField_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R ⧸ v.asIdeal)] : IsNonarchimedeanLocalField (adicCompletion K v)

An adic completion with finite residue field is a nonarchimedean local field.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.normalizedValuationWithZero_adicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [Finite (R ⧸ v.asIdeal)] (x : adicCompletion K v) : (TauCeti.normalizedValuationWithZero (adicCompletion K v)) x = (Valued.v x)⁻¹

The zero-preserving normalized valuation of the completion K_v is the inverse of its adic valuation Valued.v.

instance IsDedekindDomain.HeightOneSpectrum.compactSpace_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [IsNonarchimedeanLocalField (adicCompletion K v)] : CompactSpace ↥(adicCompletionIntegers K v)

The ring of integers in an adic completion that is a nonarchimedean local field is compact.

theorem IsDedekindDomain.HeightOneSpectrum.mem_unitFiltration_adicCompletion_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [IsNonarchimedeanLocalField (adicCompletion K v)] {n : ℕ} {u : (adicCompletion K v)ˣ} : u ∈ TauCeti.unitFiltration (adicCompletion K v) n ↔ Valued.v ↑u = 1 ∧ Valued.v (↑u - 1) ≤ WithZero.exp (-↑n)

The unit filtration of K_v in terms of the adic valuation. A unit u of K_v lies in the n-th step U(K_v, n) of the unit filtration exactly when it is a unit of 𝒪_v and u ≡ 1 to level n, that is, Valued.v u = 1 and Valued.v (u - 1) ≤ exp (-n).

theorem IsDedekindDomain.HeightOneSpectrum.mem_unitFiltration_zero_adicCompletion_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [IsNonarchimedeanLocalField (adicCompletion K v)] {u : (adicCompletion K v)ˣ} : u ∈ TauCeti.unitFiltration (adicCompletion K v) 0 ↔ Valued.v ↑u = 1

The units of 𝒪_v in terms of the adic valuation. A unit u of K_v lies in the depth-zero step U(K_v, 0) of the unit filtration exactly when Valued.v u = 1.

theorem IsDedekindDomain.HeightOneSpectrum.unitsMap_algebraMap_mem_unitFiltration_zero_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) [IsNonarchimedeanLocalField (adicCompletion K v)] (a : Kˣ) : (Units.map ↑(algebraMap K (adicCompletion K v))) a ∈ TauCeti.unitFiltration (adicCompletion K v) 0 ↔ (valuation K v) ↑a = 1

Units of K of valuation one in the completion. The image in K_v of a unit a of K lies in the depth-zero step U(K_v, 0) of the unit filtration exactly when a has v-adic valuation one.

theorem IsDedekindDomain.HeightOneSpectrum.not_isSquare_adicCompletion_of_valuation_eq_exp_of_not_even {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : K) (n : ℤ) (hn : ¬Even n) (ha : (valuation K v) a = WithZero.exp n) : ¬IsSquare ((algebraMap K (adicCompletion K v)) a)

An element of odd order of vanishing at v is a nonsquare in the completion K_v.

The hypothesis v.valuation K a = WithZero.exp n with ¬ Even n says that the valuation exponent of a at v is n, that is, that its order of vanishing is the odd integer -n. This is the nonsquare criterion a finite place of a prescribed set needs: an element that vanishes there to odd order remains a nonsquare in the completion.

The value group of HeightOneSpectrum.valuation is WithZero (Multiplicative ℤ), whose multiplicative identity 1 is the value zero, that is, order of vanishing zero, so an order of vanishing 1 is written WithZero.exp (-1), the value of a generator of v.asIdeal; the passage between the two conventions is neg_log_valuation_eq_one_iff in TauCeti.RingTheory.DedekindDomain.AdicValuation.Basic.