Adele Ring

We define the adele ring of a number field K as the direct product of the infinite adele ring of K and the finite adele ring of K. We show that the adele ring of K is a locally compact space.

Main definitions

• NumberField.adeleRing K is the adele ring of a number field K.
• NumberField.AdeleRing.globalEmbedding K is the map sending x ∈ K to (x)ᵥ.
• NumberField.AdeleRing.principalSubgroup K is the subgroup of principal adeles (x)ᵥ.

Main results

• AdeleRing.locallyCompactSpace : the adele ring of a number field is a locally compact space.

References

• [J.W.S. Cassels, A. Frölich, Algebraic Number Theory][cassels1967algebraic]
• [M.I. de Frutos-Fernàndez, Formalizing the Ring of Adèles of a Global Field][defrutosfernandez2022]

Tags

adele ring, dedekind domain

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

The adele ring of a number field.

Equations

• NumberField.adeleRing K = (NumberField.infiniteAdeleRing K × ↥(DedekindDomain.finiteAdeleRing (↥(NumberField.ringOfIntegers K)) K))

instance NumberField.AdeleRing.instCommRingAdeleRing (K : Type u_1) [Field K] [NumberField K] : CommRing (NumberField.adeleRing K)

Equations

• NumberField.AdeleRing.instCommRingAdeleRing K = Prod.instCommRing

instance NumberField.AdeleRing.instInhabitedAdeleRing (K : Type u_1) [Field K] [NumberField K] : Inhabited (NumberField.adeleRing K)

Equations

• NumberField.AdeleRing.instInhabitedAdeleRing K = { default := 0 }

instance NumberField.AdeleRing.topologicalSpace (K : Type u_1) [Field K] [NumberField K] : TopologicalSpace (NumberField.adeleRing K)

Equations

• NumberField.AdeleRing.topologicalSpace K = instTopologicalSpaceProd

instance NumberField.AdeleRing.topologicalRing (K : Type u_1) [Field K] [NumberField K] : TopologicalRing (NumberField.adeleRing K)

Equations

• ⋯ = ⋯

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

The global embedding sending x ∈ K to (x)ᵥ.

Equations

• NumberField.AdeleRing.globalEmbedding K = RingHom.prod (NumberField.InfiniteAdeleRing.globalEmbedding K) (DedekindDomain.FiniteAdeleRing.globalEmbedding (↥(NumberField.ringOfIntegers K)) K)

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

theorem NumberField.AdeleRing.locallyCompactSpace (K : Type u_1) [Field K] [NumberField K] : LocallyCompactSpace (NumberField.adeleRing K)

The adele ring of a number field is a locally compact space.

def NumberField.AdeleRing.principalSubgroup (K : Type u_1) [Field K] [NumberField K] : AddSubgroup (NumberField.adeleRing K)

The subgroup of principal adeles (x)ᵥ where x ∈ K.

Equations

• NumberField.AdeleRing.principalSubgroup K = Subring.toAddSubgroup (RingHom.range (NumberField.AdeleRing.globalEmbedding K))