Local compactness of finite adele rings

The finite adele ring of a Dedekind domain with finite residue fields is locally compact. Each adic completion is a nonarchimedean local field, and its integer ring is compact and open. The result then follows from the local-compactness theorem for restricted products. If the Dedekind domain is moreover countable, the finite adele ring is σ-compact: every finite adele has a common denominator b, so it lies in one of the countably many compact sets b⁻¹ · ∏_v 𝒪_v.

The finite-residue-field hypothesis is stated directly, rather than specialized to rings of integers, so this applies to every Dedekind domain for which the same local compactness argument is valid.

Main results

• IsDedekindDomain.FiniteAdeleRing.instLocallyCompactSpace: the finite adele ring is locally compact when all residue fields are finite.
• IsDedekindDomain.FiniteAdeleRing.instSigmaCompactSpace: the finite adele ring is σ-compact when moreover the Dedekind domain is countable.

References

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

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

The finite adele ring of a Dedekind domain with finite residue fields is locally compact.

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

The finite adele ring of a countable Dedekind domain with finite residue fields is σ-compact.