The finite adele ring: separation, integral elements, and strong approximation

Mathlib's IsDedekindDomain.FiniteAdeleRing R K is the restricted product of the completions v.adicCompletion K over the height one primes v of a Dedekind domain R with fraction field K, with respect to the integer rings v.adicCompletionIntegers K. This file records basic facts about it that are not stated in Mathlib:

• the finite adele ring is Hausdorff, since each completion is;
• subtraction, multiplication, and the multiplicative unit are computed place by place;
• the product of the local integer rings embeds continuously as the integral finite adeles;
• an element of K is integral at every finite place exactly when it lies in R, so the integral finite adeles meet the diagonal copy of K in R;
• strong approximation: K is dense in the finite adele ring.

The third fact is the finite half of the discreteness of a number field in its adele ring. The fourth says that an element of K can be made close to a given finite adele a at finitely many places while differing from a by an integral element at every other place. Since the integral finite adeles are open, it implies that K and the integral finite adeles together span the finite adele ring additively. For a number field the infinite places are what is omitted here: K is discrete, not dense, in the full adele ring.

The proof clears denominators: a finite adele a has a common denominator d ∈ R, and the integral adele a * d is approximated by an element r ∈ R at finitely many places by the Chinese remainder theorem, with enough extra precision at the primes dividing d that r / d approximates a.

Main results

• IsDedekindDomain.FiniteAdeleRing.integralEmbedding: the continuous embedding of the product of the local integer rings into the finite adeles.
• IsDedekindDomain.FiniteAdeleRing.one_apply, sub_apply, and mul_apply: the corresponding operations are computed place by place.
• IsDedekindDomain.FiniteAdeleRing.continuous_ofAdicCompletion: the embedding of the completion at a finite place into the finite adeles is continuous.
• IsDedekindDomain.FiniteAdeleRing.forall_algebraMap_mem_adicCompletionIntegers_iff: the diagonal image of x : K is integral at every finite place if and only if x lies in R.
• IsDedekindDomain.FiniteAdeleRing.mul_nonZeroDivisor_mem_adicCompletionIntegers: a finite adele has a common denominator in R.
• IsDedekindDomain.FiniteAdeleRing.exists_forall_valued_sub_le_and_forall_valued_sub_le_one: strong approximation with explicit precision at finitely many places and integrality everywhere.
• IsDedekindDomain.FiniteAdeleRing.denseRange_algebraMap: K is dense in the finite adele ring.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §§14–15.
• J. Neukirch, Algebraic Number Theory, Chapter I, §3 (the Chinese remainder theorem).

instance IsDedekindDomain.FiniteAdeleRing.instT2Space_tauCeti (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : T2Space (FiniteAdeleRing R K)

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.one_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : 1 v = 1

The value of 1 : 𝔸ᶠ[R, K] at a finite place is 1.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.zero_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : 0 v = 0

The value of the zero finite adele at every finite place is zero.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.sub_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a b : FiniteAdeleRing R K) (v : HeightOneSpectrum R) : (a - b) v = a v - b v

Subtraction of finite adeles is computed place by place.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.mul_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a b : FiniteAdeleRing R K) (v : HeightOneSpectrum R) : (a * b) v = a v * b v

Multiplication of finite adeles is computed place by place.

noncomputable def IsDedekindDomain.FiniteAdeleRing.integralEmbedding {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : ((v : HeightOneSpectrum R) → ↥(HeightOneSpectrum.adicCompletionIntegers K v)) →A[ℤ] FiniteAdeleRing R K

The product of the local integer rings embedded continuously in the finite adele ring. Its range is the set of finite adeles integral at every finite place.

Equations

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

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.integralEmbedding_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : (v : HeightOneSpectrum R) → ↥(HeightOneSpectrum.adicCompletionIntegers K v)) (v : HeightOneSpectrum R) : (integralEmbedding x) v = ↑(x v)

The integral embedding is evaluated place by place.

theorem IsDedekindDomain.FiniteAdeleRing.isEmbedding_integralEmbedding {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Topology.IsEmbedding ⇑integralEmbedding

The product of the local integer rings embeds into the finite adele ring.

theorem IsDedekindDomain.FiniteAdeleRing.continuous_integralEmbedding {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Continuous ⇑integralEmbedding

The embedding of the product of the local integer rings into the finite adeles is continuous.

theorem IsDedekindDomain.FiniteAdeleRing.range_integralEmbedding {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] : Set.range ⇑integralEmbedding = {a : FiniteAdeleRing R K | ∀ (v : HeightOneSpectrum R), a v ∈ HeightOneSpectrum.adicCompletionIntegers K v}

The range of the integral embedding is the set of finite adeles integral at every place.

theorem IsDedekindDomain.FiniteAdeleRing.continuous_ofAdicCompletion {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Continuous ⇑(ofAdicCompletion K v)

The embedding of the completion at a finite place into the finite adele ring is continuous: it is the coordinate inclusion RestrictedProduct.mulSingle v.

theorem IsDedekindDomain.FiniteAdeleRing.isCompact_integralFiniteAdeles {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] [∀ (v : HeightOneSpectrum R), CompactSpace ↥(HeightOneSpectrum.adicCompletionIntegers K v)] : IsCompact {a : FiniteAdeleRing R K | ∀ (v : HeightOneSpectrum R), a v ∈ HeightOneSpectrum.adicCompletionIntegers K v}

The integral finite adeles are compact when every local integer ring is compact.

theorem IsDedekindDomain.FiniteAdeleRing.forall_algebraMap_mem_adicCompletionIntegers_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (x : K) : (∀ (v : HeightOneSpectrum R), ((algebraMap K (FiniteAdeleRing R K)) x) v ∈ HeightOneSpectrum.adicCompletionIntegers K v) ↔ x ∈ (algebraMap R K).range

The diagonal image of an element of K in the finite adele ring is integral at every finite place exactly when the element lies in R.

Strong approximation

theorem IsDedekindDomain.FiniteAdeleRing.mul_nonZeroDivisor_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a : FiniteAdeleRing R K) : ∃ b ∈ nonZeroDivisors R, ∀ (v : HeightOneSpectrum R), a v * (algebraMap R (HeightOneSpectrum.adicCompletion K v)) b ∈ HeightOneSpectrum.adicCompletionIntegers K v

A finite adele has a common denominator: some nonzero divisor b of R makes a * b integral at every place.

theorem IsDedekindDomain.FiniteAdeleRing.exists_forall_valued_sub_le_and_forall_valued_sub_le_one {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a : FiniteAdeleRing R K) (s : Finset (HeightOneSpectrum R)) (n : HeightOneSpectrum R → ℕ) : ∃ (x : K), (∀ v ∈ s, Valued.v ((algebraMap K (HeightOneSpectrum.adicCompletion K v)) x - a v) ≤ WithZero.exp (-↑(n v))) ∧ ∀ (v : HeightOneSpectrum R), Valued.v ((algebraMap K (HeightOneSpectrum.adicCompletion K v)) x - a v) ≤ 1

Strong approximation for the finite adeles, in explicit form. Every finite adele a is approximated by an element x of K to any prescribed precision at finitely many places, while x - a is integral at every place.

theorem IsDedekindDomain.FiniteAdeleRing.exists_forall_sub_algebraMap_mem_adicCompletionIntegers {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (a : FiniteAdeleRing R K) : ∃ (x : K), ∀ (v : HeightOneSpectrum R), a v - (algebraMap K (HeightOneSpectrum.adicCompletion K v)) x ∈ HeightOneSpectrum.adicCompletionIntegers K v

Every finite adele differs from a diagonal element by an integral finite adele.

theorem IsDedekindDomain.FiniteAdeleRing.exists_finset_forall_mem_of_mem_nhds_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {U : Set (FiniteAdeleRing R K)} (hU : U ∈ nhds 0) : ∃ (I : Finset (HeightOneSpectrum R)) (n : HeightOneSpectrum R → ℕ), ∀ (a : FiniteAdeleRing R K), (∀ (v : HeightOneSpectrum R), a v ∈ HeightOneSpectrum.adicCompletionIntegers K v) → (∀ v ∈ I, Valued.v (a v) ≤ WithZero.exp (-↑(n v))) → a ∈ U

Every neighbourhood of 0 in the finite adele ring contains a basic congruence neighbourhood. There are a finite set I of places and exponents n such that every finite adele integral at every place, with v-adic valuation at most exp (-n v) at each v ∈ I, lies in the neighbourhood.

theorem IsDedekindDomain.FiniteAdeleRing.denseRange_algebraMap (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] : DenseRange ⇑(algebraMap K (FiniteAdeleRing R K))

Strong approximation: K is dense in the finite adele ring of R.