The geometric coefficient of the ray ideal count

Counting the points of a coset of congruenceLattice 𝔪 (mk0 𝔞) in the norm-≤ t section of rayFundamentalDomain 𝔪 gives a main term V / covol · t, where V is the volume of the norm-one section of the domain and covol the covolume of the lattice. This file evaluates the coefficient V / covol · N 𝔞 that this produces for the ideals of a ray class, where t = x · N 𝔞, in terms of rayClassIdealMainTerm 𝔪.

Writing w_𝔪 for the number of roots of unity congruent to one modulo 𝔪, the coefficient is V / covol · N 𝔞 = w_𝔪 · rayClassIdealMainTerm 𝔪.

Main results

• TauCeti.GlobalNumberFields.measureReal_div_covolume_congruenceLattice_mul_absNorm: the coefficient is w_𝔪 times rayClassIdealMainTerm 𝔪.

theorem TauCeti.GlobalNumberFields.measureReal_div_covolume_congruenceLattice_mul_absNorm {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (𝔞 : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : MeasureTheory.volume.real (rayFundamentalDomain 𝔪 ∩ {x : NumberField.mixedEmbedding.mixedSpace K | NumberField.mixedEmbedding.norm x ≤ 1}) / ZLattice.covolume (congruenceLattice 𝔪 ((FractionalIdeal.mk0 K) 𝔞)) MeasureTheory.volume * ↑(Ideal.absNorm ↑𝔞) = ↑(Nat.card ↥(unitsCongruenceTorsion 𝔪)) * rayClassIdealMainTerm 𝔪

The geometric coefficient of the ray ideal count. The volume of the norm-one section of rayFundamentalDomain 𝔪, over the covolume of the congruence lattice of a nonzero integral ideal 𝔞, times the norm of 𝔞, is w_𝔪 · rayClassIdealMainTerm 𝔪, where w_𝔪 is the number of roots of unity congruent to one modulo 𝔪. In particular the left-hand side does not depend on 𝔞.