Every open subgroup of the idele class group contains a ray subgroup

Let K be a number field. The ray subgroups raySubgroup 𝔪, indexed by the moduli 𝔪 of K, are open subgroups of the idele class group C_K. This file proves that they are cofinal among all open subgroups: every open subgroup of C_K contains raySubgroup 𝔪 for some modulus 𝔪. Consequently the finite quotients C_K / raySubgroup 𝔪 ≅ Cl_𝔪 see every open subgroup, which is what identifies the continuous finite-order characters of C_K with the ray class characters.

The proof works in the idele group. An open subgroup V of the ideles is a neighbourhood of 1, so it contains all ideles x with x and x⁻¹ in a neighbourhood W of 1 in the adele ring. The finite part of W contains a basic congruence neighbourhood: integrality at every finite place and a congruence x_v ≡ 1 to some level n v at finitely many places v. The modulus 𝔪 with exponent n v at those places and every real place in its infinite part therefore has ideleCongruenceSubgroup 𝔪 ≤ V, once the archimedean components are handled: an open subgroup is closed, so V contains every connected set of ideles through 1, hence all ideles concentrated at a complex place and all positive ideles concentrated at a real place. The finite and archimedean components of a congruence idele are then separately in V.

Since the ray subgroups and the idele congruence subgroups are themselves open, a subgroup of the idele class group or of the idele group is open exactly when it contains one of them.

As the ray subgroups of two moduli generate the ray subgroup of their greatest common divisor, the moduli whose ray subgroup lies in a given open subgroup U are exactly the multiples of a least one, the conductor of U (OpenSubgroup.ideleClassConductor). Applied to the norm group of an extension of number fields, it is the conductor of that extension. Its exponent at a finite place v is read off at v alone: it is the least n such that U contains the ideles concentrated at v with component in U(K_v, n) (OpenSubgroup.exponent_ideleClassConductor_le_iff).

Main definitions

• OpenSubgroup.ideleClassConductor: the least modulus whose ray subgroup lies in an open subgroup of the idele class group.

Main results

• TauCeti.GlobalNumberFields.ofCompletion_mem_connectedComponentOfOne: every idele concentrated at a complex place and every positive idele concentrated at a real place lies in the identity component of the idele group.
• TauCeti.GlobalNumberFields.ofCompletion_mem_of_isOpen: an open subgroup of the idele group contains every idele concentrated at a complex place and every positive idele concentrated at a real place.
• TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_ofFiniteIdele_mem_of_mem_nhds: every neighbourhood of 1 in the idele group contains the finite parts of the ideles of some idele congruence subgroup.
• TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_le_of_isOpen: every open subgroup of the idele group contains an idele congruence subgroup.
• TauCeti.GlobalNumberFields.isOpen_iff_exists_ideleCongruenceSubgroup_le: a subgroup of the idele group is open exactly when it contains an idele congruence subgroup.
• TauCeti.GlobalNumberFields.exists_raySubgroup_le_of_isOpen: every open subgroup of the idele class group contains a ray subgroup.
• TauCeti.GlobalNumberFields.isOpen_iff_exists_raySubgroup_le: a subgroup of the idele class group is open exactly when it contains a ray subgroup.
• OpenSubgroup.ideleClassConductor_dvd_iff: the conductor of U divides 𝔪 exactly when the ray subgroup of 𝔪 lies in U.
• OpenSubgroup.ideleClassConductor_inf: the conductor of U ⊓ V is the least common multiple of the conductors of U and V.
• OpenSubgroup.exponent_ideleClassConductor_le_iff: the exponent of a finite place v in the conductor of U is at most n exactly when U contains the ideles concentrated at v with component in U(K_v, n).

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §17.

theorem TauCeti.GlobalNumberFields.ofCompletion_mem_connectedComponentOfOne {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] (w : NumberField.InfinitePlace K) (u : w.Completionˣ) (hu : ∀ (hw : w.IsReal), 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hw) ↑u) : (NumberField.IdeleGroup.ofCompletion R K w) u ∈ Subgroup.connectedComponentOfOne (NumberField.IdeleGroup R K)

The archimedean identity component of the idele group: every idele concentrated at a complex place, and every positive idele concentrated at a real place, lies in the identity component of the idele group.

theorem TauCeti.GlobalNumberFields.ofCompletion_mem_of_isOpen {K : Type u_1} [Field K] {R : Type u_2} [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K] {V : Subgroup (NumberField.IdeleGroup R K)} (hV : IsOpen ↑V) (w : NumberField.InfinitePlace K) (u : w.Completionˣ) (hu : ∀ (hw : w.IsReal), 0 < (NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hw) ↑u) : (NumberField.IdeleGroup.ofCompletion R K w) u ∈ V

An open subgroup of the idele group contains the archimedean identity component: it contains every idele concentrated at a complex place and every positive idele concentrated at a real place. Membership of an idele in an open subgroup therefore depends on its archimedean components only through their signs at the real places.

theorem TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_ofFiniteIdele_mem_of_mem_nhds {K : Type u_1} [Field K] [NumberField K] {N : Set (NumberField.IdeleGroup (NumberField.RingOfIntegers K) K)} (hN : N ∈ nhds 1) : ∃ (𝔪 : Modulus K), ∀ x ∈ ideleCongruenceSubgroup 𝔪, (NumberField.IdeleGroup.ofFiniteIdele (NumberField.RingOfIntegers K) K) ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) x) ∈ N

The finite parts of an idele congruence subgroup are small. For every neighbourhood N of 1 in the idele group there is a modulus 𝔪 such that the finite part of every idele of ideleCongruenceSubgroup 𝔪, that is, the idele with the same finite components and trivial infinite components, lies in N. The infinite components need separate treatment, because the congruence subgroup imposes no bound on them.

theorem TauCeti.GlobalNumberFields.exists_ideleCongruenceSubgroup_le_of_isOpen {K : Type u_1} [Field K] [NumberField K] (V : Subgroup (NumberField.IdeleGroup (NumberField.RingOfIntegers K) K)) (hV : IsOpen ↑V) : ∃ (𝔪 : Modulus K), ideleCongruenceSubgroup 𝔪 ≤ V

Every open subgroup of the idele group contains an idele congruence subgroup. The idele congruence subgroups are therefore cofinal among the open subgroups of the idele group; see isOpen_iff_exists_ideleCongruenceSubgroup_le for the resulting characterisation of openness.

theorem TauCeti.GlobalNumberFields.isOpen_iff_exists_ideleCongruenceSubgroup_le {K : Type u_1} [Field K] [NumberField K] (V : Subgroup (NumberField.IdeleGroup (NumberField.RingOfIntegers K) K)) : IsOpen ↑V ↔ ∃ (𝔪 : Modulus K), ideleCongruenceSubgroup 𝔪 ≤ V

A subgroup of the idele group is open exactly when it contains an idele congruence subgroup.

theorem TauCeti.GlobalNumberFields.exists_raySubgroup_le_of_isOpen {K : Type u_1} [Field K] [NumberField K] (U : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) (hU : IsOpen ↑U) : ∃ (𝔪 : Modulus K), raySubgroup 𝔪 ≤ U

Every open subgroup of the idele class group contains a ray subgroup. The ray subgroups are therefore cofinal among the open subgroups of the idele class group, so that the finite quotients C_K / raySubgroup 𝔪 see every open subgroup; see isOpen_iff_exists_raySubgroup_le for the resulting characterisation of openness.

theorem TauCeti.GlobalNumberFields.isOpen_iff_exists_raySubgroup_le {K : Type u_1} [Field K] [NumberField K] (U : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) : IsOpen ↑U ↔ ∃ (𝔪 : Modulus K), raySubgroup 𝔪 ≤ U

A subgroup of the idele class group is open exactly when it contains a ray subgroup.

The conductor of an open subgroup

noncomputable def OpenSubgroup.ideleClassConductor {K : Type u_1} [Field K] [NumberField K] (U : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) : TauCeti.GlobalNumberFields.Modulus K

The conductor of an open subgroup of the idele class group: the least modulus whose ray subgroup lies in U. Every modulus whose ray subgroup lies in U is a multiple of it (ideleClassConductor_dvd_iff).

theorem OpenSubgroup.raySubgroup_ideleClassConductor_le {K : Type u_1} [Field K] [NumberField K] (U : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) : TauCeti.GlobalNumberFields.raySubgroup U.ideleClassConductor ≤ ↑U

The ray subgroup of the conductor of U lies in U.

theorem OpenSubgroup.ideleClassConductor_dvd_iff {K : Type u_1} [Field K] [NumberField K] {U : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} {𝔪 : TauCeti.GlobalNumberFields.Modulus K} : U.ideleClassConductor ∣ 𝔪 ↔ TauCeti.GlobalNumberFields.raySubgroup 𝔪 ≤ ↑U

The universal property of the conductor: the conductor of U divides 𝔪 exactly when the ray subgroup of 𝔪 lies in U.

theorem OpenSubgroup.ideleClassConductor_dvd_of_le {K : Type u_1} [Field K] [NumberField K] {U V : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} (h : U ≤ V) : V.ideleClassConductor ∣ U.ideleClassConductor

A larger open subgroup has a smaller conductor.

@[simp]

theorem OpenSubgroup.ideleClassConductor_top {K : Type u_1} [Field K] [NumberField K] : ⊤.ideleClassConductor = TauCeti.GlobalNumberFields.Modulus.one K

The whole idele class group has the trivial conductor.

@[simp]

theorem OpenSubgroup.ideleClassConductor_inf {K : Type u_1} [Field K] [NumberField K] (U V : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)) : (U ⊓ V).ideleClassConductor = U.ideleClassConductor.lcm V.ideleClassConductor

The conductor of an intersection is the least common multiple of the conductors.

theorem OpenSubgroup.exponent_ideleClassConductor_le_iff {K : Type u_1} [Field K] [NumberField K] {U : OpenSubgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {n : ℕ} : U.ideleClassConductor.exponent v ≤ n ↔ ∀ u ∈ TauCeti.unitFiltration (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) n, ↑((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u) ∈ U

The exponents of the conductor are local. The exponent of a finite place v in the conductor of U is at most n exactly when U contains the class of every idele concentrated at v whose component lies in U(K_v, n).