The trivial ideal weight and Dedekind zeta coefficients

This file identifies the norm coefficients of the trivial ideal weight with the coefficients of the Dedekind zeta function. There is one necessary exception: Mathlib's coefficient counts all integral ideals and therefore has value 1 at index zero, contributed by the zero ideal, whereas an ArithmeticFunction has value zero there. Since LSeries ignores its zero coefficient, the two coefficient systems define the same series.

Since 1 * 1 = 1 pointwise, the same identification shows that regrouping has no pointwise-product formula as soon as some norm is attained by two ideals (TauCeti.not_forall_normCoeff_mul_eq_pmul): the coefficient of the product is the ideal count, not its square. ℚ(i), with its two ideals of norm 5, is such a field.

For the rational field the ring of integers is isomorphic to ℤ. Mapping an ideal through this isomorphism and using Int.ideal_span_absNorm_eq_self shows that there is exactly one ideal of each positive norm. Thus the trivial ideal weight over ℚ regroups to the constant coefficient 1 at every positive index, as for the Riemann zeta function.

Roadmap role

This is Layer 1.3, the trivial specialization, of TauCetiRoadmap/ArithmeticDirichletSeries/README.md. It completes Layer 1 without asserting the exact abscissa of convergence; that is Layer 5, proved in TauCeti.abscissaOfAbsConv_normCoeff_one.

noncomputable def TauCeti.dedekindZetaCoeff (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ℕ

The coefficient used in Mathlib's definition of the Dedekind zeta function: the number of integral ideals of absolute norm n.

Unlike an ArithmeticFunction, this function has value 1 at zero, contributed by the zero ideal.

Equations

• TauCeti.dedekindZetaCoeff K n = Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

@[simp]

theorem TauCeti.dedekindZetaCoeff_zero (K : Type u_1) [Field K] [NumberField K] : dedekindZetaCoeff K 0 = 1

The zero ideal is the unique integral ideal of absolute norm zero.

theorem TauCeti.dedekindZeta_eq_LSeries_dedekindZetaCoeff (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : NumberField.dedekindZeta K s = LSeries (fun (n : ℕ) => ↑(dedekindZetaCoeff K n)) s

The Dedekind zeta function is the LSeries of dedekindZetaCoeff.

theorem TauCeti.card_normFiber_eq_dedekindZetaCoeff (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : n ≠ 0) : (normFiber K n).card = dedekindZetaCoeff K n

Away from zero, the cardinality of the finite nonzero-ideal norm fibre is the corresponding Dedekind zeta coefficient.

@[simp]

theorem TauCeti.normCoeff_one_apply (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ((normCoeff K) 1) n = ↑(if n = 0 then 0 else dedekindZetaCoeff K n)

The trivial ideal arithmetic function regroups to the Dedekind zeta coefficients away from zero. At zero its norm coefficient is forced to vanish by the ArithmeticFunction carrier.

theorem TauCeti.normCoeff_toIdealArithmeticFunction_one_apply (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ((normCoeff K) (UnitaryIdealWeight.toIdealArithmeticFunction 1)) n = ↑(if n = 0 then 0 else dedekindZetaCoeff K n)

The trivial unitary ideal weight has the Dedekind zeta coefficients away from zero.

theorem TauCeti.dedekindZeta_eq_LSeries_normCoeff_one (K : Type u_1) [Field K] [NumberField K] (s : ℂ) : NumberField.dedekindZeta K s = LSeries (⇑((normCoeff K) 1)) s

Regrouping the trivial ideal weight gives Mathlib's Dedekind zeta function.

theorem TauCeti.not_forall_normCoeff_mul_eq_pmul (K : Type u_1) [Field K] [NumberField K] {n : ℕ} (hn : 1 < dedekindZetaCoeff K n) : ¬∀ (f g : IdealArithmeticFunction K), (normCoeff K) (f * g) = ((normCoeff K) f).pmul ((normCoeff K) g)

Regrouping does not turn pointwise products into pointwise products. If two or more integral ideals share the absolute norm n, then no formula normCoeff (f * g) = (normCoeff f).pmul (normCoeff g) holds: already for f = g = 1 the n-th coefficient of 1 * 1 = 1 is the ideal count dedekindZetaCoeff K n, not its square.

@[simp]

theorem TauCeti.dedekindZetaCoeff_rat (n : ℕ) : dedekindZetaCoeff ℚ n = 1

There is exactly one integral ideal of ℚ of each absolute norm.

@[simp]

theorem TauCeti.normFiber_rat_absNorm (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers ℚ)))) : normFiber ℚ (Ideal.absNorm ↑I) = {I}

Over ℚ, a nonzero integral ideal is the only one of its absolute norm.

theorem TauCeti.normCoeff_one_rat_apply {n : ℕ} (hn : 0 < n) : ((normCoeff ℚ) 1) n = 1

Over ℚ, the trivial ideal weight has coefficient 1 at every positive integer.

theorem TauCeti.normCoeff_toIdealArithmeticFunction_one_rat_apply {n : ℕ} (hn : 0 < n) : ((normCoeff ℚ) (UnitaryIdealWeight.toIdealArithmeticFunction 1)) n = 1

Over ℚ, the trivial unitary ideal weight has coefficient 1 at every positive integer.