The ray class group as a quotient of the idele class group

Let K be a number field and 𝔪 a modulus. This file constructs the surjective homomorphism

rayClassQuotient 𝔪 : IdeleClassGroup (𝓞 K) K →* RayClassGroup 𝔪

and identifies its kernel with the ray subgroup raySubgroup 𝔪, so that the ray class group is the quotient of the idele class group by the image of the idele congruence subgroup.

The map is described on the ideles congruent to one modulo 𝔪 (ideleCongrOneSubgroup 𝔪): such an idele is a unit at every finite divisor of 𝔪, so the fractional ideal of its finite component is prime to 𝔪, and the idele is sent to the ray class of that ideal (rayClassQuotient_mk_of_mem). By weak approximation at the places of 𝔪, every idele becomes congruent to one after multiplication by a principal idele (exists_unitEmbedding_mul_mem_ideleCongrOneSubgroup), and a principal idele that is congruent to one comes from an element of Kˣ congruent to one, whose principal ideal lies in the ray. So the description determines a well-defined homomorphism on idele classes.

Main definitions

• TauCeti.GlobalNumberFields.rayClassQuotient: the homomorphism from the idele class group onto the ray class group of 𝔪.

Main results

• TauCeti.GlobalNumberFields.exists_unitEmbedding_mul_mem_ideleCongrOneSubgroup: every idele is congruent to one modulo 𝔪 after multiplication by a principal idele.
• TauCeti.GlobalNumberFields.rayClassQuotient_mk_of_mem: the image of the class of an idele congruent to one is the ray class of the fractional ideal of its finite component.
• TauCeti.GlobalNumberFields.rayClassQuotient_surjective: the map is surjective.
• TauCeti.GlobalNumberFields.ker_rayClassQuotient: its kernel is raySubgroup 𝔪.
• TauCeti.GlobalNumberFields.finiteIndex_raySubgroup: hence the ray subgroup has finite index.
• TauCeti.GlobalNumberFields.classMap_comp_rayClassQuotient: the maps are compatible with the transition maps between ray class groups.
• TauCeti.GlobalNumberFields.raySubgroup_le_raySubgroup_iff: for 𝔪 ∣ 𝔫, the ray subgroup of 𝔪 lies in that of 𝔫 exactly when the transition map from 𝔫 to 𝔪 is injective.
• TauCeti.GlobalNumberFields.rayClassQuotient_ofAdicCompletion_of_isUniformizer: the idele that is a uniformizer at a finite place v outside 𝔪 and 1 elsewhere is sent to the ray class of the prime v.
• TauCeti.GlobalNumberFields.ideleClassGroup_hom_ext_of_raySubgroup_le: two homomorphisms out of the idele class group that kill raySubgroup 𝔪 are equal once they agree on the uniformizers at the finite places outside 𝔪.
• TauCeti.GlobalNumberFields.rayClassQuotient_ofCompletion_neg_one: the idele that is -1 at one real place of 𝔪 and 1 elsewhere is sent to the ray class of the trivial residue and the sign pattern that is -1 exactly at that place.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1, Proposition 1.9.

Representatives congruent to one

theorem TauCeti.GlobalNumberFields.exists_unitEmbedding_mul_mem_ideleCongrOneSubgroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : ∃ (α : Kˣ), (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) α * x ∈ ideleCongrOneSubgroup 𝔪

Every idele is congruent to one after multiplication by a principal idele. This is weak approximation at the finite divisors and the real places of 𝔪: an element of K close enough to the inverse of the idele at those places makes the product a principal unit of the prescribed level at each finite divisor and positive at each selected real place.

The ray class of an idele congruent to one

theorem TauCeti.GlobalNumberFields.toFractionalIdeal_toFiniteIdele_mem_idealsPrimeTo {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongrOneSubgroup 𝔪) : IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) x) ∈ idealsPrimeTo 𝔪

The fractional ideal of an idele congruent to one is prime to the modulus: such an idele is a unit at every finite divisor of 𝔪.

The ray class of an idele class

noncomputable def TauCeti.GlobalNumberFields.rayClassQuotient {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K →* RayClassGroup 𝔪

The ray class of an idele class. The class of an idele x is sent to the ray class of the fractional ideal of the finite component of α x, for any α ∈ Kˣ making α x congruent to one modulo 𝔪; the result does not depend on the choice of α.

theorem TauCeti.GlobalNumberFields.rayClassQuotient_mk_of_mem {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x ∈ ideleCongrOneSubgroup 𝔪) : (rayClassQuotient 𝔪) ↑x = (rayClassMk 𝔪) ⟨IsDedekindDomain.FiniteAdeleRing.toFractionalIdeal ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) x), ⋯⟩

The ray class of the class of an idele congruent to one is the ray class of the fractional ideal of its finite component.

@[simp]

theorem TauCeti.GlobalNumberFields.oneEquivClassGroup_rayClassQuotient_mk {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) : oneEquivClassGroup ((rayClassQuotient (Modulus.one K)) ↑x) = (IsDedekindDomain.FiniteAdeleRing.toClassGroup (NumberField.RingOfIntegers K) K) ((NumberField.IdeleGroup.toFiniteIdele (NumberField.RingOfIntegers K) K) x)

The ordinary ideal class of an idele is its ray class at the trivial modulus.

theorem TauCeti.GlobalNumberFields.rayClassQuotient_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(rayClassQuotient 𝔪)

The ray class map is surjective. An invertible fractional ideal prime to 𝔪 is the ideal of a finite idele that is a unit at every finite divisor of 𝔪; replacing its components there by 1, and taking 1 at every infinite place, gives an idele congruent to one with the same ideal.

theorem TauCeti.GlobalNumberFields.ker_rayClassQuotient {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (rayClassQuotient 𝔪).ker = raySubgroup 𝔪

The kernel of the ray class map is the ray subgroup. The ray class of an idele congruent to one is trivial exactly when its ideal is generated by an element congruent to one; dividing by that element leaves an idele congruent to one that is a unit at every finite place, that is, an element of the idele congruence subgroup.

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

The ray subgroup has finite index: it is the kernel of the surjection rayClassQuotient 𝔪 onto the finite ray class group.

theorem TauCeti.GlobalNumberFields.classMap_comp_rayClassQuotient {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : (classMap h).comp (rayClassQuotient 𝔫) = rayClassQuotient 𝔪

The ray class maps are compatible with the transition maps: for 𝔪 ∣ 𝔫, the ray class of an idele class modulo 𝔫, carried to the ray class group of 𝔪, is its ray class modulo 𝔪.

@[simp]

theorem TauCeti.GlobalNumberFields.classMap_rayClassQuotient {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) (c : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K) : (classMap h) ((rayClassQuotient 𝔫) c) = (rayClassQuotient 𝔪) c

The ray class maps are compatible with the transition maps.

theorem TauCeti.GlobalNumberFields.raySubgroup_le_raySubgroup_iff {K : Type u_1} [Field K] [NumberField K] {𝔪 𝔫 : Modulus K} (h : 𝔪 ∣ 𝔫) : raySubgroup 𝔪 ≤ raySubgroup 𝔫 ↔ (classMap h).ker ≤ ⊥

Comparison of ray subgroups along a transition map: for 𝔪 ∣ 𝔫, the ray subgroup of 𝔪 lies in that of 𝔫 exactly when the transition map from 𝔫 to 𝔪 is injective. Under the surjective ray class map modulo 𝔫, the ray subgroup of 𝔪 is the preimage of the kernel of the transition map, and that of 𝔫 is the preimage of the trivial subgroup.

Uniformizers at finite places

theorem TauCeti.GlobalNumberFields.rayClassQuotient_ofAdicCompletion_of_isUniformizer {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} {π : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ} (hπ : IsUniformizer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) π) (I : ↥(idealsPrimeTo 𝔪)) (hI : ↑↑I = ↑v.asIdeal) : (rayClassQuotient 𝔪) ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) π) = (rayClassMk 𝔪) I

The ray class of a uniformizer at a finite place is the ray class of the prime. For a finite place v of K outside the support of a modulus 𝔪 and a uniformizer π of K_v, the class of the idele with component π at v and 1 elsewhere has the ray class of the prime v: this idele is congruent to one modulo 𝔪, and its fractional ideal is v.

theorem TauCeti.GlobalNumberFields.ideleClassGroup_hom_ext_of_raySubgroup_le {K : Type u_1} [Field K] [NumberField K] {𝔪 : Modulus K} {M : Type u_2} [Group M] {f g : NumberField.IdeleClassGroup (NumberField.RingOfIntegers K) K →* M} (hf : raySubgroup 𝔪 ≤ f.ker) (hg : raySubgroup 𝔪 ≤ g.ker) (h : ∀ v ∉ 𝔪.support, ∀ (π : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ), IsUniformizer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) π → f ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) π) = g ((NumberField.IdeleClassGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) π)) : f = g

Homomorphisms out of the idele class group are determined on uniformizers. Two homomorphisms out of C_K whose kernels contain the ray subgroup of 𝔪 are equal as soon as they agree on the class of every idele that is a uniformizer at a finite place outside the support of 𝔪 and 1 elsewhere. Both factor through the ray class group of 𝔪, which is generated by the ray classes of the primes outside the support, and those are the images of these ideles (rayClassQuotient_ofAdicCompletion_of_isUniformizer).

By exists_raySubgroup_le_of_isOpen, every homomorphism with open kernel kills some ray subgroup.

Signs at the real places

theorem TauCeti.GlobalNumberFields.rayClassQuotient_ofCompletion_neg_one {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) [DecidableEq ↥𝔪.infinitePart] (w : ↥𝔪.infinitePart) : (rayClassQuotient 𝔪) ((NumberField.IdeleClassGroup.ofCompletion (NumberField.RingOfIntegers K) K ↑↑w) (-1)) = (residueSignRayClass 𝔪) (1, Pi.mulSingle w (-1))

The ray class of the sign -1 at a real place of the modulus. The class of the idele that is -1 at a real place w of 𝔪 and 1 at every other place is the class residueSignRayClass 𝔪 (1, Pi.mulSingle w (-1)) of the trivial residue and of the sign pattern that is -1 at w and 1 at the other real places of 𝔪.

At a real place outside 𝔪 the corresponding class is trivial (ofCompletion_mem_raySubgroup).