Ray subgroups of the idele class group

Let K be a number field and 𝔪 a modulus. The ray subgroup raySubgroup 𝔪 is the image in the idele class group of the ideles satisfying the finite and infinite congruence conditions imposed by 𝔪. Thus an idele class belongs to the ray subgroup precisely when it has a representative in ideleCongruenceSubgroup 𝔪.

The quotient map from ideles to idele classes is open. Since the idele congruence subgroup is open, its image is open as well. The ray subgroups are antitone in the modulus: increasing the finite exponents or adding real places imposes stronger conditions and gives a smaller subgroup. The ray subgroup of the greatest common divisor of two moduli is generated by their two ray subgroups, which is what gives every open subgroup a least modulus whose ray subgroup it contains.

The pullback of raySubgroup 𝔪 to the idele group is the join of the idele congruence subgroup and the principal ideles. This is the form used to identify the kernel of the homomorphism from idele classes to ray classes.

Main definitions

• TauCeti.GlobalNumberFields.raySubgroup: the image of an idele congruence subgroup in the idele class group.

Main results

• TauCeti.GlobalNumberFields.mem_raySubgroup_iff: membership through a congruence-idele representative.
• TauCeti.GlobalNumberFields.mk_mem_raySubgroup_iff: a class represented by an idele belongs precisely when that idele is in the join of the congruence subgroup and the principal ideles.
• TauCeti.GlobalNumberFields.raySubgroup_antitone: ray subgroups decrease when the modulus grows.
• TauCeti.GlobalNumberFields.raySubgroup_gcd: the ray subgroup of a greatest common divisor is the join of the two ray subgroups.
• TauCeti.GlobalNumberFields.isOpen_raySubgroup: every ray subgroup is open.
• TauCeti.GlobalNumberFields.ofCompletion_mem_raySubgroup: an idele class concentrated at an infinite place where the modulus imposes no sign condition is a ray class.

References

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

noncomputable def TauCeti.GlobalNumberFields.raySubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K)

The ray subgroup of the idele class group: the image of the ideles satisfying the congruence conditions of 𝔪 under the quotient by the principal ideles.

instance TauCeti.GlobalNumberFields.normal_raySubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (raySubgroup 𝔪).Normal

Every ray subgroup is normal: it is the image of a subgroup of the commutative idele group under the quotient map.

theorem TauCeti.GlobalNumberFields.mem_raySubgroup_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K} : c ∈ raySubgroup 𝔪 ↔ ∃ x ∈ ideleCongruenceSubgroup 𝔪, (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K)) x = c

Membership in a ray subgroup is represented by a congruence idele.

@[simp]

theorem TauCeti.GlobalNumberFields.comap_raySubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup.comap (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K)) (raySubgroup 𝔪) = ideleCongruenceSubgroup 𝔪 ⊔ NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K

The pullback of a ray subgroup to the ideles. An idele represents a class in raySubgroup 𝔪 exactly when it belongs to the join of the congruence subgroup and the principal ideles.

@[simp]

theorem TauCeti.GlobalNumberFields.mk_mem_raySubgroup_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} : ↑x ∈ raySubgroup 𝔪 ↔ x ∈ ideleCongruenceSubgroup 𝔪 ⊔ NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K

Membership of an idele representative in a ray subgroup. The class of an idele lies in raySubgroup 𝔪 exactly when the idele differs from a congruence idele by a principal idele.

theorem TauCeti.GlobalNumberFields.raySubgroup_antitone {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : raySubgroup 𝔫 ≤ raySubgroup 𝔪

Ray subgroups decrease when the modulus grows.

theorem TauCeti.GlobalNumberFields.raySubgroup_gcd {K : Type u_1} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) : raySubgroup (𝔪.gcd 𝔫) = raySubgroup 𝔪 ⊔ raySubgroup 𝔫

The ray subgroup of a greatest common divisor is generated by the two ray subgroups. A subgroup containing the ray subgroups of two moduli therefore contains the ray subgroup of their greatest common divisor.

theorem TauCeti.GlobalNumberFields.ofCompletion_mem_raySubgroup {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {w : NumberField.InfinitePlace K} (hw : ∀ w' ∈ 𝔪.infinitePart, ↑w' ≠ w) (u : w.Completionˣ) : (NumberField.IdeleClassGroup.ofCompletion (NumberField.RingOfIntegers K) K w) u ∈ raySubgroup 𝔪

An idele class concentrated at an infinite place outside the modulus is a ray class. If the infinite place w is not one of the real places of 𝔪, the class of the idele that is u at w and 1 at every other place lies in raySubgroup 𝔪, for every u ∈ K_wˣ.

theorem TauCeti.GlobalNumberFields.isOpen_raySubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : IsOpen ↑(raySubgroup 𝔪)

Every ray subgroup is open in the idele class group.