Topology of the adele ring of a number field

Mathlib's NumberField.InfiniteAdeleRing K is the finite product of the completions of K at its infinite places, and NumberField.AdeleRing R K is the product of the infinite adele ring with the finite adele ring of R. Both are defined as type synonyms, so the Hausdorff property of the underlying products is not found by instance search. This file records it, so that closedness of discrete subgroups and separation of quotients apply to the adele ring. For the same reason Prod.fst_mul does not apply to adeles, so the file also records that the infinite component of a product of adeles is the product of the infinite components (NumberField.AdeleRing.fst_mul), and that the embeddings of a completion at an infinite place into the infinite adele ring and into the adele ring are continuous (NumberField.InfiniteAdeleRing.continuous_ofCompletion, NumberField.AdeleRing.continuous_ofCompletion), as is the embedding of a completion at a finite place into the adele ring (NumberField.AdeleRing.continuous_ofAdicCompletion).

The field K is dense in both the infinite and the finite adele ring, but its diagonal image is discrete in the adele ring itself. What is dense is the subring generated by K and the idempotent (1, 0) cutting out the infinite component, and so a continuous ring homomorphism out of the adele ring is determined by its values on K and on that idempotent (NumberField.AdeleRing.ringHom_ext).

It also upgrades Mathlib's ring equivalence between the infinite adele ring and the Minkowski mixed space to a homeomorphism. Each local factor is isometric to ℝ or ℂ, so the product equivalence and its inverse are continuous, and the norm of the mixed space (NumberField.mixedEmbedding.norm) is carried to the norm of the infinite adele ring.

instance NumberField.InfiniteAdeleRing.instT2Space (K : Type u_2) [Field K] : T2Space (InfiniteAdeleRing K)

The infinite adele ring is Hausdorff, as a finite product of the completions at the infinite places.

noncomputable def NumberField.InfiniteAdeleRing.homeomorphMixedSpace (K : Type u_2) [Field K] : InfiniteAdeleRing K ≃ₜ mixedEmbedding.mixedSpace K

The infinite adele ring is homeomorphic to the Minkowski mixed space. This is the topological form of InfiniteAdeleRing.ringEquiv_mixedSpace: the underlying equivalence is the one of that ring isomorphism, and continuity in both directions comes from the isometry of each completion with ℝ or ℂ.

@[simp]

theorem NumberField.InfiniteAdeleRing.homeomorphMixedSpace_apply (K : Type u_2) [Field K] (x : InfiniteAdeleRing K) : (homeomorphMixedSpace K) x = (ringEquiv_mixedSpace K) x

@[simp]

theorem NumberField.InfiniteAdeleRing.coe_homeomorphMixedSpace (K : Type u_2) [Field K] : ⇑(homeomorphMixedSpace K) = ⇑(ringEquiv_mixedSpace K)

@[simp]

theorem NumberField.InfiniteAdeleRing.homeomorphMixedSpace_symm_apply (K : Type u_2) [Field K] (x : mixedEmbedding.mixedSpace K) : (homeomorphMixedSpace K).symm x = (ringEquiv_mixedSpace K).symm x

@[simp]

theorem NumberField.InfiniteAdeleRing.coe_homeomorphMixedSpace_symm (K : Type u_2) [Field K] : ⇑(homeomorphMixedSpace K).symm = ⇑(ringEquiv_mixedSpace K).symm

theorem NumberField.InfiniteAdeleRing.continuous_ringEquiv_mixedSpace (K : Type u_2) [Field K] : Continuous ⇑(ringEquiv_mixedSpace K)

The standard ring equivalence from the infinite adele ring to the Minkowski mixed space is continuous.

theorem NumberField.InfiniteAdeleRing.continuous_ringEquiv_mixedSpace_symm (K : Type u_2) [Field K] : Continuous ⇑(ringEquiv_mixedSpace K).symm

The inverse of the standard ring equivalence from the Minkowski mixed space to the infinite adele ring is continuous.

theorem NumberField.InfiniteAdeleRing.exists_sub_algebraMap_integer_mem_parallelepiped (K : Type u_2) [Field K] [NumberField K] (z : InfiniteAdeleRing K) : ∃ (y : RingOfIntegers K), (ringEquiv_mixedSpace K) (z - (algebraMap K (InfiniteAdeleRing K)) ((algebraMap (RingOfIntegers K) K) y)) ∈ parallelepiped ⇑(mixedEmbedding.latticeBasis K)

Every infinite adele can be translated by the image of an algebraic integer into the closed fundamental parallelepiped of the Minkowski lattice.

@[simp]

theorem NumberField.InfiniteAdeleRing.mixedEmbedding_norm_ringEquiv_mixedSpace (K : Type u_2) [Field K] [NumberField K] (x : InfiniteAdeleRing K) : mixedEmbedding.norm (fun (v : { w : InfinitePlace K // w.IsReal }) => (InfinitePlace.Completion.extensionEmbeddingOfIsReal ⋯) (x ↑v), fun (v : { w : InfinitePlace K // w.IsComplex }) => (InfinitePlace.Completion.extensionEmbedding ↑v) (x ↑v)) = ‖x‖

The norm of the Minkowski mixed-space image of an infinite adele is its norm: the product over the infinite places of the local absolute values, squared at the complex places.

The image InfiniteAdeleRing.ringEquiv_mixedSpace K x is written in the coordinates that InfiniteAdeleRing.ringEquiv_mixedSpace_apply produces, which is its simp-normal form.

instance NumberField.AdeleRing.instT2Space (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : T2Space (AdeleRing R K)

The adele ring is Hausdorff, as the product of the infinite and the finite adele rings.

@[simp]

theorem NumberField.AdeleRing.fst_mul {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (a b : AdeleRing R K) : (a * b).1 = a.1 * b.1

The infinite component of a product of adeles is the product of their infinite components.

theorem NumberField.InfiniteAdeleRing.continuous_ofCompletion (K : Type u_2) [Field K] (w : InfinitePlace K) : Continuous ⇑(ofCompletion w)

The embedding of the completion at an infinite place into the infinite adele ring is continuous: it is the coordinate inclusion Pi.mulSingle w.

theorem NumberField.AdeleRing.continuous_ofCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (w : InfinitePlace K) : Continuous ⇑(ofCompletion R K w)

The embedding of the completion at an infinite place into the adele ring is continuous.

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

The embedding of the completion at a finite place into the adele ring is continuous.

theorem NumberField.AdeleRing.ringHom_ext (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [NumberField K] {T : Type u_3} [NonAssocSemiring T] [TopologicalSpace T] [T2Space T] {f g : AdeleRing R K →+* T} (hf : Continuous ⇑f) (hg : Continuous ⇑g) (hK : ∀ (x : K), f ((algebraMap K (AdeleRing R K)) x) = g ((algebraMap K (AdeleRing R K)) x)) (h₁₀ : ∀ (a : AdeleRing R K), a.1 = 1 → a.2 = 0 → f a = g a) : f = g

A continuous ring homomorphism out of the adele ring is determined by its values on K and on the idempotent (1, 0), the second hypothesis being stated for every adele with components 1 and 0. The diagonal copy of K is not dense in the adele ring, but K × K is dense in the product of the infinite and the finite adele rings, and (x, y) = e x + (1 - e) y for the idempotent e = (1, 0). The target need only be a nonassociative semiring: the equivalent decomposition (x, y) = e (x - y) + y uses subtraction only in K.