Adic valuations on Dedekind domains

Let R be a Dedekind domain of Krull dimension 1, K its field of fractions and v a maximal ideal of R. In this file we prove that the v-adic completion of K is locally compact and its ring of integers is compact.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.ofFiniteCoeffs π n constructs a v-adic integer from an n-tuple of v-adic integers by using them as coefficients in a finite v-adic expansionin the uniformizer π.
• IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs π n gives the first n coefficients in the v-adic expansion in π of a v-adic integer modulo the nth power of the maximal ideal.

Main results

• IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.quotient_maximalIdeal_pow_finite : the quotient of the v-adic ring of integers by a power of the maximal ideal is finite.
• IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isCompact : the v-adic ring of integers is compact.
• IsDedekindDomain.HeightOneSpectrum.locallyCompactSpace : the v-adic Completion of K is locally compact.

References

• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [M.I. de Frutos-Fernández, F.A.E. Nuccio, A Formalization of Complete Discrete Valuation Rings and Local Fields][defrutosfernandez2023]

Tags

dedekind domain, dedekind ring, adic valuation

theorem IsDedekindDomain.HeightOneSpectrum.algebraMap_valuation_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : ↥(nonZeroDivisors R)) : Valued.v ((algebraMap R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ↑r) ≠ 0

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.isClosed_nhds_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (γ : (WithZero (Multiplicative ℤ))ˣ) : IsClosed {y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v y < ↑γ}

Open balls at zero are closed in the v-adic completion of K.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.hasBasis_nhds_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : (nhds 0).HasBasis (fun (γ : (WithZero (Multiplicative ℤ))ˣ) => γ ≤ 1) fun (γ : (WithZero (Multiplicative ℤ))ˣ) => {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v x < ↑γ}

There is a basis of neighbourhoods of zero in Kᵥ that are contained inside Oᵥ. Note: this is true of any DVR (but not of any Valued).

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.hasBasis_uniformity {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : (uniformity (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).HasBasis (fun (γ : (WithZero (Multiplicative ℤ))ˣ) => γ ≤ 1) fun (γ : (WithZero (Multiplicative ℤ))ˣ) => {p : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v × IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v (p.2 - p.1) < ↑γ}

There is a basis of uniformity of Kᵥ with radii less than or equal to one. Note: this is true of any DVR.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.exists_not_mem_of_nhds {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (γ : (WithZero (Multiplicative ℤ))ˣ) (y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : ∃ (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), Valued.v (x - y) > ↑γ

Given an integer γ and some centre y ∈ Kᵥ we can always find an element x ∈ Kᵥ outide of the open ball at y of radius γ.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.dvd_of_valued_le {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} {y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v} (h : Valued.v x ≤ Valued.v y) (hy : y ≠ 0) : ∃ (r : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)), ↑r * y = x

If x ∈ Kᵥ has valuation at most that of y ∈ Kᵥ, then x is an integral multiple of y.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.valuation_le_pow_of_maximalIdeal {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (n : ℕ) (hx : x ∈ Valued.maximalIdeal (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ^ n) : Valued.v ↑x ≤ ↑(Multiplicative.ofAdd (-↑n))

An element of a positive power n of the maximal ideal of the v-adic integers has valuation less than or equal to -n.

def IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.ofFiniteCoeffs {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} (π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (n : ℕ) : (Fin n → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

Takes an n-tuple (a₁, ..., aₙ) and creates a v-adic integer using the n-tuple as coefficients in a finite v-adic expansion in some fixed v-adic integer π as a₁ + a₂π + a₃π² + .... Note the definition does not require π to be a uniformizer.

Equations

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

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.finite_expansion {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (n : ℕ) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) : ∃ (a : Fin n → Valued.ResidueField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), x - (List.mapIdx (fun (i : ℕ) (j : Valued.ResidueField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) => Quotient.out' j * π ^ i) (List.ofFn a)).sum ∈ Valued.maximalIdeal (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ^ n

Given a uniformizer π of the v-adic integers and a v-adic integer x, there exists an n-tuple of representatives in the residue field of the v-adic integers such that x can be written as a finite v-adic expansion in π with coefficients given by the n-tuple.

def IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (n : ℕ) (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⧸ Valued.maximalIdeal (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ^ n → Fin n → Valued.ResidueField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

Given a uniformizer π of the v-adic integers and a v-adic integer x modulo a power of the maximal ideal, gives the coefficients of x in the finite v-adic expansion in π as an n-tuple of representatives in the residue field.

Equations

• IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs n hπ x = Classical.choose ⋯

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs_injective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (n : ℕ) (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) : Function.Injective (IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.toFiniteCoeffs n hπ)

instance IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.quotient_maximalIdeal_pow_finite {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v : IsDedekindDomain.HeightOneSpectrum R} {π : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)} (n : ℕ) (hπ : IsDedekindDomain.HeightOneSpectrum.AdicCompletion.IsUniformizer ↑π) : Finite (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⧸ Valued.maximalIdeal (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ^ n)

The quotient of the v-adic integers with a power of the maximal ideal is finite.

Equations

• ⋯ = ⋯

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isClosed {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsClosed ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

The v-adic integers are closed in the v-adic completion of K.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.finite_subcover_of_uniformity_basis {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {γ : (WithZero (Multiplicative ℤ))ˣ} (hγ : ↑γ ≤ 1) : ∃ (t : Set (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)), t.Finite ∧ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ⊆ ⋃ y ∈ t, {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | (x, y) ∈ {p : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v × IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v (p.2 - p.1) < ↑γ}}

There is a finite covering of the v-adic integers of open balls of radius less than one, obtained by using the finite representatives in the quotient of the v-adic integers by an appropriate power of the maximal ideal.

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.totallyBounded {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : TotallyBounded (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).carrier

The v-adic integers is a totally bounded set since they afford a finite subcover of open balls, obtained by using the finite representatives of the quotient of the v-adic integers by a power of the maximal ideal.

instance IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.instCompleteSpaceSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers_adeleRingLocallyCompact {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : CompleteSpace ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

Equations

• ⋯ = ⋯

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletionIntegers.isCompact {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsCompact (IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v).carrier

The v-adic integers is compact.

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

Equations

• ⋯ = ⋯

theorem IsDedekindDomain.HeightOneSpectrum.AdicCompletion.isCompact_nhds_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {γ : (WithZero (Multiplicative ℤ))ˣ} (hγ : γ ≤ 1) : IsCompact {y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v | Valued.v y < ↑γ}

Any open ball centred at zero in the v-adic completion of K is compact.

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

The v-adic completion of K is locally compact. Note: slow search for TopologicalAddGroup instance of v.adicCompletion K.

Equations

• ⋯ = ⋯