Compactness of the norm-one idele class group

For a number field K, the norm-one idele class group C_K¹ = 𝕀_K¹ / Kˣ is compact. This is the adelic form of the two finiteness theorems of algebraic number theory: the finiteness of the ideal class group and Dirichlet's unit theorem. The full idele class group is not compact, since the idele class norm maps it onto ℝ>0; C_K¹ is the kernel of that map.

Main results

• TauCeti.GlobalNumberFields.IdeleClassGroup.isCompact_normOne: the norm-one idele class group is a compact subset of the idele class group.
• TauCeti.GlobalNumberFields.IdeleClassGroup.compactSpace_normOne: the norm-one idele class group is a compact space.

References

• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §16.
• J. Neukirch, Algebraic Number Theory, Chapter VI, §1, Theorem 1.6.
• A. Weil, Basic Number Theory, Chapter IV, §4.

theorem TauCeti.GlobalNumberFields.IdeleClassGroup.isCompact_normOne (K : Type u_1) [Field K] [NumberField K] : IsCompact ↑(normOne K)

The norm-one idele class group is compact. This is the adelic form of the finiteness of the class group together with Dirichlet's unit theorem.

instance TauCeti.GlobalNumberFields.IdeleClassGroup.compactSpace_normOne (K : Type u_1) [Field K] [NumberField K] : CompactSpace ↥(normOne K)

The norm-one idele class group is a compact space.