Counting the integral ideals of a ray class

Let 𝔪 be a modulus of a number field K and c a ray class of 𝔪. This file introduces rayClassIdealCountingFunction 𝔪 c x, the number of nonzero integral ideals prime to the finite part of 𝔪 that lie in the class c and have norm at most x, and proves the two facts that make it a counting function at all: the sets being counted are finite, and summing over the ray class group recovers the unrestricted count.

The carrier is integralIdealsPrimeTo 𝔪, the monoid on which idealClass is defined, so coprimality and nonvanishing are forced by the type rather than imposed as side conditions; the zero ideal and ideals sharing a prime with the finite part cannot enter the count.

Finiteness is not proved here. TauCeti.Order.Northcott.Basic already fixes the project's convention for counting by an inclusive real cutoff, and supplies finite_setOf_natCast_le for any natural-valued Northcott function. All this file adds is the Northcott instance for the absolute norm on integralIdealsPrimeTo 𝔪; the finiteness, and with it normLE, summatory and Nat.card_coe_normLE, then come from that shared layer. The bound is taken in ℝ rather than ℕ because the asymptotics that consume this count are.

The partition is stated first as an equivalence, idealClassSigmaEquiv, and only then in counting form. The equivalence needs no finiteness at all, and it is what a consumer weighting the classes by a character reaches for; the counting statement is its Nat.card shadow.

Main definitions

• TauCeti.GlobalNumberFields.rayClassIdealCountingFunction: the number of nonzero integral ideals prime to 𝔪 in a fixed ray class with norm at most x.
• TauCeti.GlobalNumberFields.idealClassSigmaEquiv: the ideals prime to 𝔪 of norm at most x, partitioned into their ray classes.

Main results

• TauCeti.GlobalNumberFields.sum_rayClassIdealCountingFunction: the class counts sum to the unrestricted count of nonzero integral ideals prime to 𝔪 of norm at most x.
• TauCeti.GlobalNumberFields.rayClassIdealCountingFunction_def, TauCeti.GlobalNumberFields.idealClassSigmaEquiv_apply_coe and TauCeti.GlobalNumberFields.idealClassSigmaEquiv_symm_apply_fst: the characteristic lemmas of the two definitions, so that a consumer never has to unfold either.

References

• J. Neukirch, Algebraic Number Theory, Chapter VI, §1.
• CBirkbeck/AINTLIB @ 2622c61d2502159c62865a1b59fc1de473519113 (Apache-2.0, Chris Birkbeck), projects/Chebotarev/CebotarevDensity/ForMathlib/IdealCongruenceCount.lean: card_norm_le_residue_eq_sum_class is the corresponding partition step, stated there for the ordinary class group together with a norm-residue condition.

Finiteness of the sets being counted

instance TauCeti.GlobalNumberFields.instNorthcottSubtypeIdealRingOfIntegersMemSubmonoidIntegralIdealsPrimeToNatCoeMonoidWithZeroHomAbsNormVal {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Northcott fun (I : ↥(integralIdealsPrimeTo 𝔪)) => Ideal.absNorm ↑I

The absolute norm is Northcott on the ideals prime to a modulus: only finitely many have norm below any bound. This mirrors TauCeti.instNorthcottAbsNormNonZeroDivisors, which does the same for (Ideal R)⁰.

instance TauCeti.GlobalNumberFields.instFiniteSubtypeIdealRingOfIntegersMemSubmonoidIntegralIdealsPrimeToLeRealCastCoeMonoidWithZeroHomNatAbsNormVal {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : ℝ) : Finite { I : ↥(integralIdealsPrimeTo 𝔪) // ↑(Ideal.absNorm ↑I) ≤ x }

The nonzero integral ideals prime to 𝔪 of norm at most a real bound form a finite type. The cutoff is real, and inclusive, per the convention TauCeti.Order.Northcott.Basic fixes.

instance TauCeti.GlobalNumberFields.instFiniteSubtypeIdealRingOfIntegersMemSubmonoidIntegralIdealsPrimeToAndEqRayClassGroupCoeMonoidHomIdealClassLeRealCastMonoidWithZeroHomNatAbsNormVal {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (c : RayClassGroup 𝔪) (x : ℝ) : Finite { I : ↥(integralIdealsPrimeTo 𝔪) // (idealClass 𝔪) I = c ∧ ↑(Ideal.absNorm ↑I) ≤ x }

Restricting to a single ray class keeps the set finite.

The counting function and the class partition

noncomputable def TauCeti.GlobalNumberFields.rayClassIdealCountingFunction {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (c : RayClassGroup 𝔪) (x : ℝ) : ℕ

The ray class ideal counting function. The number of nonzero integral ideals in the ray class c of 𝔪, prime to the finite part of 𝔪, whose norm is at most x. The carrier already forces coprimality and nonvanishing, so the zero ideal and other classes cannot enter.

Equations

• One or more equations did not get rendered due to their size.

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

The counting function as the cardinality defining it. The rewrite rule turning rayClassIdealCountingFunction into the set of ideals of class c whose norm is at most x.

noncomputable def TauCeti.GlobalNumberFields.idealClassSigmaEquiv {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : ℝ) : (c : RayClassGroup 𝔪) × { I : ↥(integralIdealsPrimeTo 𝔪) // (idealClass 𝔪) I = c ∧ ↑(Ideal.absNorm ↑I) ≤ x } ≃ { I : ↥(integralIdealsPrimeTo 𝔪) // ↑(Ideal.absNorm ↑I) ≤ x }

The ray classes partition the ideals of bounded norm. An ideal prime to 𝔪 of norm at most x is the same thing as a ray class together with an ideal of that class and that norm bound, because idealClass 𝔪 is a function on the carrier and the summands are exactly its fibres.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GlobalNumberFields.idealClassSigmaEquiv_apply_coe {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : ℝ) (p : (c : RayClassGroup 𝔪) × { I : ↥(integralIdealsPrimeTo 𝔪) // (idealClass 𝔪) I = c ∧ ↑(Ideal.absNorm ↑I) ≤ x }) : ↑((idealClassSigmaEquiv 𝔪 x) p) = ↑p.snd

The partition keeps the ideal: it only forgets which class the ideal was filed under.

@[simp]

theorem TauCeti.GlobalNumberFields.idealClassSigmaEquiv_symm_apply_fst {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (x : ℝ) (I : { I : ↥(integralIdealsPrimeTo 𝔪) // ↑(Ideal.absNorm ↑I) ≤ x }) : ((idealClassSigmaEquiv 𝔪 x).symm I).fst = (idealClass 𝔪) ↑I

Filing an ideal under its own ray class is the inverse of forgetting it: the class component is idealClass 𝔪 I and the ideal component is I again.

theorem TauCeti.GlobalNumberFields.sum_rayClassIdealCountingFunction {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) [Fintype (RayClassGroup 𝔪)] (x : ℝ) : ∑ c : RayClassGroup 𝔪, rayClassIdealCountingFunction 𝔪 c x = Nat.card { I : ↥(integralIdealsPrimeTo 𝔪) // ↑(Ideal.absNorm ↑I) ≤ x }

The class counts sum to the total. Summing rayClassIdealCountingFunction over the ray class group recovers the number of nonzero integral ideals prime to 𝔪 of norm at most x.

The ray class group is always finite (finite_rayClassGroup), but it carries no canonical Fintype, so the enumeration is taken as a hypothesis rather than fixed to Fintype.ofFinite here; that keeps the statement usable against whichever enumeration the caller holds.