The ray class count, reindexed by a representative ideal

Counting the integral ideals of a fixed ray class is awkward directly, because the class condition is not a divisibility condition. Multiplying by an ideal 𝔞 whose class is the inverse one turns it into two conditions that are: divisibility by 𝔞, and triviality of the class. The norm bound is carried along, scaled by the norm of 𝔞.

Main results

• TauCeti.GlobalNumberFields.rayClassIdealCountingFunction_eq_card_dvd_and_idealClass_eq_one: the counting function as the number of multiples of 𝔞 of trivial class and bounded norm.

Provenance

The reindexing follows Mathlib's class-group analogue NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₁ (Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean) move for move: subtypeEquiv, then subtypeSubtypeEquivSubtypeInter, then Nat.card_congr. That lemma is private, is a Nat.card equality rather than an Equiv, and is stated over (Ideal (𝓞 K))⁰, so it cannot be called from here.

theorem TauCeti.GlobalNumberFields.rayClassIdealCountingFunction_eq_card_dvd_and_idealClass_eq_one {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) {c : RayClassGroup 𝔪} (𝔞 : ↥(integralIdealsPrimeTo 𝔪)) (h𝔞 : (idealClass 𝔪) 𝔞 = c⁻¹) (x : ℝ) : rayClassIdealCountingFunction 𝔪 c x = Nat.card { I : ↥(integralIdealsPrimeTo 𝔪) // 𝔞 ∣ I ∧ (idealClass 𝔪) I = 1 ∧ ↑(Ideal.absNorm ↑I) ≤ x * ↑(Ideal.absNorm ↑𝔞) }

The counting function as a count of multiples of 𝔞. For 𝔞 in the inverse class of c, the count runs over the multiples of 𝔞 of trivial class, against a norm bound scaled by N 𝔞; any 𝔞 of that class serves, as the left-hand side does not mention it. This is the rewrite that trades the class condition for a divisibility condition, where rayClassIdealCountingFunction_def is the one that keeps the class condition.