Counting ideals of trivial ray class by points of the ray fundamental domain

Let 𝔪 be a modulus of a number field K and 𝔞 a nonzero integral ideal prime to 𝔪. This file matches the integral ideals prime to 𝔪 that are multiples of 𝔞, have trivial ray class and have norm at most s, against the points of rayIdealSet 𝔪 𝔞 of mixed norm at most s: each such ideal accounts for exactly Nat.card (unitsCongruenceTorsion 𝔪) points.

The correspondence sends a point to the ideal generated by the algebraic integer it is the image of; the generator criterion idealClass_eq_one_iff_exists_generator identifies the ideals of trivial ray class as exactly those arising this way.

Main results

• TauCeti.GlobalNumberFields.card_idealClass_eq_one_dvd_norm_le: the number of multiples of 𝔞 prime to 𝔪 of trivial ray class and norm at most s, times the number of roots of unity congruent to one modulo 𝔪, is the number of points of rayIdealSet 𝔪 𝔞 of mixed norm at most s.

theorem TauCeti.GlobalNumberFields.card_idealClass_eq_one_dvd_norm_le {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (𝔞 : ↥(integralIdealsPrimeTo 𝔪)) (s : ℝ) : Nat.card { I : ↥(integralIdealsPrimeTo 𝔪) // 𝔞 ∣ I ∧ (idealClass 𝔪) I = 1 ∧ ↑(Ideal.absNorm ↑I) ≤ s } * Nat.card ↥(unitsCongruenceTorsion 𝔪) = Nat.card { a : ↑(rayIdealSet 𝔪 ⟨↑𝔞, ⋯⟩) // NumberField.mixedEmbedding.norm ↑a ≤ s }

Ideals of trivial ray class, counted by points of the ray fundamental domain. For a nonzero integral ideal 𝔞 prime to 𝔪, the number of integral ideals prime to 𝔪 that are multiples of 𝔞, have trivial ray class and have norm at most s, multiplied by the number of roots of unity congruent to one modulo 𝔪, is the number of points of rayIdealSet 𝔪 𝔞 of mixed norm at most s.

This is the ray analogue of NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le. The left-hand count is the one rayClassIdealCountingFunction_eq_card_dvd_and_idealClass_eq_one reduces the ray class counting function to, with s the scaled bound there.