Infinite adele ring

This file formalises the definition of the infinite adele ring of a number field K as the product of completions of K over its infinite places and we show that it is locally compact. The definition of the completions are formalised in AdeleRingLocallyCompact.NumberTheory.NumberField.Embeddings.

Main definitions

• DedekindDomain.infiniteAdeleRing of a number field K is defined as the product of the completions of K over its Archimedean places.

Main results

• DedekindDomain.InfiniteAdeleRing.locallyCompactSpace : the infinite adele ring is a locally compact space since it is a finite product of locally compact spaces.

References

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

Tags

infinite adele ring, number field

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) → NumberField.InfinitePlace.completion K v)

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

Equations

• NumberField.InfiniteAdeleRing.instCommRingInfiniteAdeleRing K = Pi.commRing

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• NumberField.InfiniteAdeleRing.topologicalSpace K = Pi.topologicalSpace

instance NumberField.InfiniteAdeleRing.topologicalRing (K : Type u_1) [Field K] : TopologicalRing (NumberField.infiniteAdeleRing K)

Equations

• ⋯ = ⋯

def NumberField.InfiniteAdeleRing.globalEmbedding (K : Type u_1) [Field K] : K →+* NumberField.infiniteAdeleRing K

Equations

• NumberField.InfiniteAdeleRing.globalEmbedding K = Pi.ringHom fun (v : NumberField.InfinitePlace K) => NumberField.InfinitePlace.Completion.coeRingHom K v

theorem NumberField.InfiniteAdeleRing.globalEmbedding_injective (K : Type u_1) [Field K] [NumberField K] : Function.Injective ⇑(NumberField.InfiniteAdeleRing.globalEmbedding K)

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

The infinite adele ring is locally compact.