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.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.instCommRing (K : Type u_1) [Field K] [NumberField K] : CommRing (NumberField.AdeleRing K)

Equations

• NumberField.AdeleRing.instCommRing K = Prod.instCommRing

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

Equations

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

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

Equations

• NumberField.AdeleRing.instTopologicalSpace K = instTopologicalSpaceProd

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

Equations

• ⋯ = ⋯

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

Equations

• NumberField.AdeleRing.instAlgebra K = Prod.algebra K (NumberField.InfiniteAdeleRing K) (DedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K)

@[simp]

theorem NumberField.AdeleRing.algebraMap_fst_apply (K : Type u_1) [Field K] [NumberField K] {v : NumberField.InfinitePlace K} (x : K) : ((algebraMap K (NumberField.AdeleRing K)) x).1 v = ↑(WithAbs ↑v) x

@[simp]

theorem NumberField.AdeleRing.algebraMap_snd_apply (K : Type u_1) [Field K] [NumberField K] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (x : K) : (fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ↑((algebraMap K (NumberField.AdeleRing K)) x).2 v) v = ↑K x

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

instance 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.

Equations

• ⋯ = ⋯

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 = (algebraMap K (NumberField.AdeleRing K)).range.toAddSubgroup