The main term of the ray class ideal count

This file defines the main term of the ray class ideal count and proves it positive: the number of integral ideals of a fixed ray class with absolute norm at most x is this coefficient times x, up to a power-saving error; this is TauCeti.GlobalNumberFields.isBigO_rayClassIdealCountingFunction_sub.

The coefficient is the Dedekind-zeta residue divided by the order of the ray class group, times one correction factor 1 - (N 𝔭)⁻¹ for each prime 𝔭 in the support of the modulus. The Euler factor of ζ_K at 𝔭 is (1 - N 𝔭 ^ (-s))⁻¹, so deleting 𝔭 from the Euler product multiplies ζ_K s by its reciprocal 1 - N 𝔭 ^ (-s); the factor above is that reciprocal at s = 1. The intended count runs over the ideals prime to the finite part of the modulus, which is what makes those corrections the right ones.

Main definitions

• TauCeti.GlobalNumberFields.rayClassIdealMainTerm: the coefficient.

Main results

• TauCeti.GlobalNumberFields.rayClassIdealMainTerm_eq: the coefficient written out.
• TauCeti.GlobalNumberFields.rayClassIdealMainTerm_one: at the trivial modulus it is the Dedekind-zeta residue over the class number.
• TauCeti.GlobalNumberFields.rayClassIdealMainTerm_pos: it is positive.

References

• S. Lang, Algebraic Number Theory, Chapter VIII, §2.
• J. Neukirch, Algebraic Number Theory, Chapter VII, §5.

noncomputable def TauCeti.GlobalNumberFields.rayClassIdealMainTerm {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : ℝ

The coefficient intended as the main term of the ray class ideal count: the Dedekind-zeta residue of K, divided by the order of the ray class group of 𝔪, times one correction factor 1 - (N 𝔭)⁻¹ — the reciprocal Euler factor at s = 1 — for each prime 𝔭 in the support of 𝔪.

Equations

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

theorem TauCeti.GlobalNumberFields.rayClassIdealMainTerm_eq {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : rayClassIdealMainTerm 𝔪 = NumberField.dedekindZeta_residue K / ↑(Nat.card (RayClassGroup 𝔪)) * ∏ v ∈ 𝔪.support, (1 - (↑(Ideal.absNorm v.asIdeal))⁻¹)

The coefficient, written out. The Dedekind-zeta residue divided by the order of the ray class group, times the correction factors at the primes dividing the finite part of the modulus.

@[simp]

theorem TauCeti.GlobalNumberFields.rayClassIdealMainTerm_one {K : Type u_1} [Field K] [NumberField K] : rayClassIdealMainTerm (Modulus.one K) = NumberField.dedekindZeta_residue K / ↑(Nat.card (ClassGroup (NumberField.RingOfIntegers K)))

The trivial modulus gives the classical coefficient. Its support is empty, so the correction product is 1, and its ray class group is the class group; what is left is the Dedekind-zeta residue over the class number.

theorem TauCeti.GlobalNumberFields.rayClassIdealMainTerm_pos {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : 0 < rayClassIdealMainTerm 𝔪

The main term is positive.