Adic Completions

If A is a valued ring with field of fractions K there are two different complete rings containing A one might define, the first is 𝒪_v = {x ∈ K_v | v x ≤ 1} and the second is the v-adic completion of A. In the case when A is a Dedekind domain these definitions give isomorphic topological A-algebras. This file makes some progress towards this.

Main theorems

• FiniteAdeleRing.closureAlgebraMapIntegers_eq_integers : The closure of A in K_v is 𝒪_v.

• FiniteAdeleRing.closureAlgebraMapIntegers_eq_prodIntegers : If s is a set of primes of A, then the closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v.

theorem IsDedekindDomain.exists_ofAdd_natCast_of_le_one {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) (hx' : x ≤ 1) : ∃ (k : ℕ), ↑(Multiplicative.ofAdd (-↑k)) = x

theorem IsDedekindDomain.exists_ofAdd_natCast_lt {x : WithZero (Multiplicative ℤ)} (hx : x ≠ 0) : ∃ (k : ℕ), ↑(Multiplicative.ofAdd (-↑k)) < x

theorem IsDedekindDomain.ne_zero_of_some_le_intValuation {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} {m : Multiplicative ℤ} (h : ↑m ≤ v.intValuation a) : a ≠ 0

theorem IsDedekindDomain.intValuation_eq_coe_neg_multiplicity {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} (hnz : a ≠ 0) : v.intValuation a = ↑(Multiplicative.ofAdd (-↑(multiplicity v.asIdeal (Ideal.span {a}))))

theorem IsDedekindDomain.emultiplicity_eq_of_valuation_eq_ofAdd {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a : A} {k : ℕ} (hv : v.intValuation a = ↑(Multiplicative.ofAdd (-↑k))) : emultiplicity v.asIdeal (Ideal.span {a}) = ↑k

theorem IsDedekindDomain.exists_adicValued_mul_sub_le {A : Type u_1} [CommRing A] [IsDedekindDomain A] (v : HeightOneSpectrum A) {a b : A} {γ : WithZero (Multiplicative ℤ)} (hγ : γ ≠ 0) (hle : γ ≤ v.intValuation a) (hle' : v.intValuation b ≤ v.intValuation a) : ∃ (y : A), v.intValuation (y * a - b) ≤ γ

Given a, b ∈ A and v b ≤ v a we can find y in A such that y is close to a / b by the valuation v.

theorem IsDedekindDomain.exists_adicValued_sub_lt_of_adicValued_le_one {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) {x : WithVal (HeightOneSpectrum.valuation K v)} (γ : (WithZero (Multiplicative ℤ))ˣ) (hx : Valued.v x ≤ 1) : ∃ (a : A), Valued.v (↑((algebraMap A K) a) - ↑x) < ↑γ

theorem IsDedekindDomain.closureAlgebraMapIntegers_eq_integers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : closure ↑(algebraMap A (HeightOneSpectrum.adicCompletion K v)).range = ↑(HeightOneSpectrum.adicCompletionIntegers K v)

The closure of A in K_v is 𝒪_v.

theorem IsDedekindDomain.denseRange_of_integerAlgebraMap {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) : DenseRange ⇑(algebraMap A ↥(HeightOneSpectrum.adicCompletionIntegers K v))

A is dense in 𝒪_v.

theorem IsDedekindDomain.exists_adicValued_sub_lt_of_adicCompletionInteger {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] (v : HeightOneSpectrum A) (x : ↥(HeightOneSpectrum.adicCompletionIntegers K v)) (γ : (WithZero (Multiplicative ℤ))ˣ) : ∃ (a : A), Valued.v (↑((algebraMap A K) a) - ↑x) < ↑γ

An element of 𝒪_v can be approximated by an element of A.

theorem IsDedekindDomain.exists_forall_adicValued_sub_lt {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} (s : Finset ι) (e : ι → (WithZero (Multiplicative ℤ))ˣ) (valuation : ι → HeightOneSpectrum A) (injective : Function.Injective valuation) (x : (i : ι) → ↥(HeightOneSpectrum.adicCompletionIntegers K (valuation i))) : ∃ (a : A), ∀ i ∈ s, Valued.v (↑((algebraMap A K) a) - ↑(x i)) < ↑(e i)

An element of ∏_{v ∈ s} 𝒪_v, with s finite, can be approximated by an element of A.

theorem IsDedekindDomain.closureAlgebraMapIntegers_eq_prodIntegers {A : Type u_1} (K : Type u_2) [CommRing A] [Field K] [Algebra A K] [IsFractionRing A K] [IsDedekindDomain A] {ι : Type u_3} (valuation : ι → HeightOneSpectrum A) (injective : Function.Injective valuation) : closure ↑(algebraMap A ((i : ι) → HeightOneSpectrum.adicCompletion K (valuation i))).range = Set.univ.pi fun (i : ι) => (HeightOneSpectrum.adicCompletionIntegers K (valuation i)).carrier

The closure of A in ∏_{v ∈ s} K_v is ∏_{v ∈ s} 𝒪_v. s may be infinite.