The finite adele ring at a single place

Let R be a Dedekind domain with fraction field K. The finite adele ring 𝔸ᶠ = 𝔸ᶠ[R, K] is the restricted product of the completions K_v = v.adicCompletion K over the height one primes v of R. This file relates 𝔸ᶠ to one completion K_v at a time, in both directions:

• the projection proj K v : 𝔸ᶠ →A[K] K_v, reading off the v-component, is a continuous K-algebra homomorphism. It is surjective and open, hence a quotient map, and it carries the integral finite adeles onto the local integers 𝒪_v. That it is a K-algebra homomorphism is the statement that the diagonal embedding K → 𝔸ᶠ followed by the projection is the completion map K → K_v;
• the map single K v : K_v →L[K] 𝔸ᶠ sends x to the finite adele with v-component x and all other components 0. It is a closed embedding onto the finite adeles supported at v, it is linear over 𝔸ᶠ acting on K_v through the projection, and single K v x is integral exactly when x is.

The multiplicative counterpart of single K v is Mathlib's IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion, which puts 1 rather than 0 at the other places; it is a closed embedding as well.

Main definitions

• IsDedekindDomain.FiniteAdeleRing.proj: the projection onto the completion at a finite place.
• IsDedekindDomain.FiniteAdeleRing.single: the finite adeles supported at a single place.

Main results

• IsDedekindDomain.FiniteAdeleRing.isOpenQuotientMap_proj: the projection is an open quotient map.
• IsDedekindDomain.FiniteAdeleRing.image_proj_integralAdeles: the integral finite adeles project onto the local integers.
• IsDedekindDomain.FiniteAdeleRing.isClosedEmbedding_single and IsDedekindDomain.FiniteAdeleRing.range_single: single K v is a closed embedding whose range is the set of finite adeles vanishing away from v; IsDedekindDomain.FiniteAdeleRing.isClosedEmbedding_ofAdicCompletion is the multiplicative counterpart.
• IsDedekindDomain.FiniteAdeleRing.single_mem_integralAdeles_iff: a finite adele supported at v is integral exactly when its v-component is.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §14.
• A. Weil, Basic Number Theory, Chapter IV, §1.

The projection onto one completion

def IsDedekindDomain.FiniteAdeleRing.proj {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : FiniteAdeleRing R K →A[K] HeightOneSpectrum.adicCompletion K v

The projection of the finite adele ring onto the completion v.adicCompletion K at a finite place v, as a continuous K-algebra homomorphism.

@[simp]

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

The projection onto the completion at v reads off the v-component.

Finite adeles supported at one place

noncomputable def IsDedekindDomain.FiniteAdeleRing.single {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : HeightOneSpectrum.adicCompletion K v →L[K] FiniteAdeleRing R K

The finite adele supported at the single place v: its v-component is x and all its other components are 0. It is a continuous K-linear map v.adicCompletion K → 𝔸ᶠ[R, K].

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.single_apply_self {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (x : HeightOneSpectrum.adicCompletion K v) : ((single K v) x) v = x

The finite adele supported at v has v-component x.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.single_apply_of_ne {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {v w : HeightOneSpectrum R} (h : w ≠ v) (x : HeightOneSpectrum.adicCompletion K v) : ((single K v) x) w = 0

The finite adele supported at v vanishes at every other place.

theorem IsDedekindDomain.FiniteAdeleRing.eq_single_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) (a : FiniteAdeleRing R K) : a = (single K v) (a v) ↔ ∀ (w : HeightOneSpectrum R), w ≠ v → a w = 0

A finite adele is supported at v exactly when it is single K v of its v-component.

theorem IsDedekindDomain.FiniteAdeleRing.range_single {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Set.range ⇑(single K v) = {a : FiniteAdeleRing R K | ∀ (w : HeightOneSpectrum R), w ≠ v → a w = 0}

The range of single K v is the set of finite adeles vanishing at every place other than v.

theorem IsDedekindDomain.FiniteAdeleRing.leftInverse_proj_single {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Function.LeftInverse ⇑(proj K v) ⇑(single K v)

The projection onto the completion at v is a left inverse of single K v.

@[simp]

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

Multiplying a finite adele supported at v by any finite adele a multiplies its v-component by a v: single K v is linear over 𝔸ᶠ[R, K] acting on the completion through the projection.

@[simp]

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

The right-handed form of mul_single.

theorem IsDedekindDomain.FiniteAdeleRing.isClosedEmbedding_single {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Topology.IsClosedEmbedding ⇑(single K v)

single K v is a closed embedding of the completion at v into the finite adele ring.

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

The finite adele ofAdicCompletion K v x, which is x at v and 1 at every other place, gives a closed embedding of the completion at v into the finite adele ring.

@[simp]

theorem IsDedekindDomain.FiniteAdeleRing.single_mem_integralAdeles_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 : HeightOneSpectrum.adicCompletion K v} : (∀ (w : HeightOneSpectrum R), ((single K v) x) w ∈ HeightOneSpectrum.adicCompletionIntegers K w) ↔ x ∈ HeightOneSpectrum.adicCompletionIntegers K v

A finite adele supported at v is integral exactly when its v-component lies in the local integers.

Topological properties of the projection

theorem IsDedekindDomain.FiniteAdeleRing.proj_surjective {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : Function.Surjective ⇑(proj K v)

The projection onto the completion at v is surjective.

theorem IsDedekindDomain.FiniteAdeleRing.isOpenMap_proj {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsOpenMap ⇑(proj K v)

The projection onto the completion at v is an open map.

theorem IsDedekindDomain.FiniteAdeleRing.isOpenQuotientMap_proj {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : IsOpenQuotientMap ⇑(proj K v)

The projection onto the completion at v is an open quotient map.

theorem IsDedekindDomain.FiniteAdeleRing.image_proj_integralAdeles {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : HeightOneSpectrum R) : ⇑(proj K v) '' ↑(integralAdeles R K) = ↑(HeightOneSpectrum.adicCompletionIntegers K v)

The integral finite adeles project onto the local integers at v.