Local compactness of adeles

The adele ring of a number field is locally compact: its archimedean part is a finite product of local fields, while its finite part is a restricted product with compact open integer rings. It is also σ-compact, which is what the open mapping theorem for topological groups needs.

Main results

• NumberField.AdeleRing.instLocallyCompactSpace: the full adele ring is locally compact.
• NumberField.InfiniteAdeleRing.instSigmaCompactSpace, NumberField.AdeleRing.instSigmaCompactSpace: the infinite and full adele rings are σ-compact.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §14.

instance NumberField.AdeleRing.instLocallyCompactSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [NumberField K] [Algebra R K] [IsFractionRing R K] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] : LocallyCompactSpace (AdeleRing R K)

The adele ring of a number field is locally compact.

instance NumberField.InfiniteAdeleRing.instSigmaCompactSpace (K : Type u_2) [Field K] [NumberField K] : SigmaCompactSpace (InfiniteAdeleRing K)

The infinite adele ring of a number field is σ-compact, since it is homeomorphic to the finite-dimensional mixed space.

instance NumberField.AdeleRing.instSigmaCompactSpace (R : Type u_1) [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [NumberField K] [Algebra R K] [IsFractionRing R K] [∀ (v : IsDedekindDomain.HeightOneSpectrum R), Finite (R ⧸ v.asIdeal)] [Countable R] : SigmaCompactSpace (AdeleRing R K)

The adele ring of a number field is σ-compact when its Dedekind domain is countable.