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

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.

Equations

• NumberField.InfiniteAdeleRing K = ((v : NumberField.InfinitePlace K) → v.Completion)

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

Equations

• NumberField.InfiniteAdeleRing.instCommRing K = Pi.commRing

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

Equations

• NumberField.InfiniteAdeleRing.instInhabited K = { default := 0 }

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)

Equations

• NumberField.InfiniteAdeleRing.instTopologicalSpace K = Pi.topologicalSpace

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)

Equations

• NumberField.InfiniteAdeleRing.instAlgebra K = Pi.algebra (NumberField.InfinitePlace K) NumberField.InfinitePlace.Completion

@[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.

Equations

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

@[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$.