The infinite adele ring of a number field

This file contains the formalisation of the infinite adele ring of a number field as the finite product of completions over its infinite places.

Main definitions

• NumberField.InfiniteAdeleRing of a number field K is defined as the product of the completions of K over its infinite places.
• NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace is the ring isomorphism between the infinite adele ring of K and ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of K.

Main results

• NumberField.InfiniteAdeleRing.locallyCompactSpace : the infinite adele ring is a locally compact space.

References

• [J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory][cassels1967algebraic]

Tags

infinite adele ring, number field

The infinite adele ring

The infinite adele ring is the finite product of completions of a number field over its infinite places. See NumberField.InfinitePlace for the definition of an infinite place and NumberField.InfinitePlace.Completion for the associated completion.

def NumberField.InfiniteAdeleRing (K : Type u_1) [Field K] : Type u_1

The infinite adele ring of a number field.

instance NumberField.InfiniteAdeleRing.instCommRing (K : Type u_1) [Field K] : CommRing (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instInhabited (K : Type u_1) [Field K] : Inhabited (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instNontrivial (K : Type u_1) [Field K] [NumberField K] : Nontrivial (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instTopologicalSpace (K : Type u_1) [Field K] : TopologicalSpace (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instIsTopologicalRing (K : Type u_1) [Field K] : IsTopologicalRing (InfiniteAdeleRing K)

instance NumberField.InfiniteAdeleRing.instAlgebra (K : Type u_1) [Field K] : Algebra K (InfiniteAdeleRing K)

@[simp]

theorem NumberField.InfiniteAdeleRing.algebraMap_apply (K : Type u_1) [Field K] (x : K) (v : InfinitePlace K) : (algebraMap K (InfiniteAdeleRing K)) x v = ↑x

instance NumberField.InfiniteAdeleRing.locallyCompactSpace (K : Type u_1) [Field K] [NumberField K] : LocallyCompactSpace (InfiniteAdeleRing K)

The infinite adele ring is locally compact.

@[reducible, inline]

abbrev NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace (K : Type u_1) [Field K] : InfiniteAdeleRing K ≃+* mixedEmbedding.mixedSpace K

The ring isomorphism between the infinite adele ring of a number field and the space ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of the number field.

@[simp]

theorem NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply (K : Type u_1) [Field K] (x : InfiniteAdeleRing K) : (ringEquiv_mixedSpace K) x = (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))

theorem NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp (K : Type u_1) [Field K] {x : K} : (mixedEmbedding K) x = (ringEquiv_mixedSpace K) ((algebraMap K (InfiniteAdeleRing K)) x)

Transfers the embedding of x ↦ (x)ᵥ of the number field K into its infinite adele ring to the mixed embedding x ↦ (φᵢ(x))ᵢ of K into the space ℝ ^ r₁ × ℂ ^ r₂, where (r₁, r₂) is the signature of K and φᵢ are the complex embeddings of K.

theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap (K : Type u_1) [Field K] [NumberField K] : DenseRange ⇑(algebraMap K (InfiniteAdeleRing K))

Weak approximation for the infinite adele ring

The number field $K$ is dense in the infinite adele ring $\prod_v K_v$.