Regrouping ideal arithmetic functions by absolute norm

This file defines TauCeti.normCoeff, the ordinary arithmetic function obtained by summing an IdealArithmeticFunction over each fibre of the absolute norm. These fibres are finite by Ideal.finite_setOfPred_absNorm_eq, so the coefficients are honest finite sums. The resulting function has value zero at 0, as required by Mathlib's ArithmeticFunction carrier; that value is available from ArithmeticFunction.map_zero.

The construction is bundled as a complex-linear map. The basic API exposes the finite norm fibre TauCeti.normFiber and its finiteness, records the value at one, proves compatibility with complex conjugation, and records in TauCeti.norm_normCoeff_eq_sum_norm_of_nonneg that no cancellation occurs inside a fibre when the values of f are nonnegative. Regrouping is compatible with transporting along an isomorphism of number fields: TauCeti.normCoeff_map says that an isomorphism e : K ≃+* L leaves every norm coefficient unchanged.

Regrouping loses information as soon as a norm fibre has more than one element: TauCeti.exists_forall_normCoeff_nonneg_not_forall_nonneg produces a nonzero ideal arithmetic function, with a negative value, whose norm coefficients all vanish. This is the rejection test that forbids weakening the nonnegativity hypothesis of the converse regrouping theorem to nonnegativity of the coefficients themselves.

Roadmap role

This is the finite-norm-fibre part of Layer 1.1 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md. The next layer step uses these coefficients to regroup an absolutely convergent series over nonzero ideals into a Mathlib LSeries.

References

• J. Neukirch, Algebraic Number Theory, Chapter VII.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapters II--III.

theorem TauCeti.finite_normFiber (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | Ideal.absNorm ↑I = n}.Finite

The fibre of nonzero integral ideals with a fixed absolute norm is finite.

noncomputable def TauCeti.normFiber (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : Finset ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))

The finite set of nonzero integral ideals with a fixed absolute norm.

Equations

• TauCeti.normFiber K n = ⋯.toFinset

@[simp]

theorem TauCeti.mem_normFiber (K : Type u_1) [Field K] [NumberField K] {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} {n : ℕ} : I ∈ normFiber K n ↔ Ideal.absNorm ↑I = n

Membership in an absolute-norm fibre.

theorem TauCeti.coe_normFiber (K : Type u_1) [Field K] [NumberField K] (n : ℕ) : ↑(normFiber K n) = (fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => Ideal.absNorm ↑I) ⁻¹' {n}

The absolute-norm fibre, viewed as a set, is the preimage of {n} under the absolute norm.

@[simp]

theorem TauCeti.normFiber_zero (K : Type u_1) [Field K] [NumberField K] : normFiber K 0 = ∅

No nonzero integral ideal has absolute norm zero.

@[simp]

theorem TauCeti.normFiber_one (K : Type u_1) [Field K] [NumberField K] : normFiber K 1 = {1}

The unit ideal is the unique nonzero integral ideal of absolute norm one.

noncomputable def TauCeti.normCoeff (K : Type u_1) [Field K] [NumberField K] : IdealArithmeticFunction K →ₗ[ℂ] ArithmeticFunction ℂ

Regroup ideal arithmetic functions by absolute norm as a complex-linear map.

The coefficient at n is the finite sum of f I over the nonzero integral ideals I whose absolute norm is n. Use normCoeff_apply for this formula.

Equations

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

theorem TauCeti.normCoeff_apply (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : ℕ) : ((normCoeff K) f) n = ∑ᶠ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (_ : I ∈ {I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | Ideal.absNorm ↑I = n}), f I

The value of normCoeff f is the finite sum of f over the corresponding absolute-norm fibre.

theorem TauCeti.normCoeff_eq_sum_normFiber (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : ℕ) : ((normCoeff K) f) n = ∑ I ∈ normFiber K n, f I

The value of normCoeff f as a sum over the finite absolute-norm fibre.

theorem TauCeti.hasFiniteSupport_normCoeff_summand (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : ℕ) : Function.HasFiniteSupport ({I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | Ideal.absNorm ↑I = n}.indicator f)

The summand defining a norm coefficient has finite support.

@[simp]

theorem TauCeti.normCoeff_apply_one (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) : ((normCoeff K) f) 1 = f 1

The norm coefficient at 1 is the value at the unit ideal.

@[simp]

theorem TauCeti.normCoeff_star_apply (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (n : ℕ) : ((normCoeff K) fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => (starRingEnd ℂ) (f I)) n = star (((normCoeff K) f) n)

Regrouping commutes with coefficientwise complex conjugation.

@[simp]

theorem TauCeti.normCoeff_fun_mul_comp_absNorm (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (g : ℕ → ℂ) (n : ℕ) : ((normCoeff K) fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => f I * g (Ideal.absNorm ↑I)) n = ((normCoeff K) f) n * g n

A factor depending on the ideal only through its norm pulls out of the regrouping. The fibre summed over is exactly the ideals of absolute norm n, so such a factor is constant on it.

@[simp]

theorem TauCeti.normCoeff_mul_absNorm_cpow (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (z : ℂ) (n : ℕ) : ((normCoeff K) fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => f I * ↑(Ideal.absNorm ↑I) ^ (-z)) n = ((normCoeff K) f) n * ↑n ^ (-z)

Regrouping absorbs a norm twist. Twisting an ideal arithmetic function by N(I) ^ (-z) twists its n-th norm coefficient by n ^ (-z). This is the compatibility of normCoeff with the norm twists of a weight, general and purely imaginary alike, since the unitary twist is the multiplicative one.

@[simp]

theorem TauCeti.normCoeff_map (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (e : K ≃+* L) (f : IdealArithmeticFunction K) (n : ℕ) : ((normCoeff L) (IdealArithmeticFunction.map e f)) n = ((normCoeff K) f) n

Regrouping is transported by an isomorphism of fields. An isomorphism e : K ≃+* L matches the nonzero ideals of 𝓞 L with those of 𝓞 K preserving absolute norms, so it matches the norm fibres and leaves every norm coefficient unchanged.

theorem TauCeti.norm_normCoeff_eq_sum_norm_of_nonneg (K : Type u_1) [Field K] [NumberField K] (f : IdealArithmeticFunction K) (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), 0 ≤ f I) (n : ℕ) : ‖((normCoeff K) f) n‖ = ∑ I ∈ normFiber K n, ‖f I‖

Absence of cancellation inside norm fibres, for a nonnegative ideal arithmetic function: the absolute value of a norm coefficient is the sum of the absolute values over the fibre.

The cancellation rejection test

theorem TauCeti.exists_forall_normCoeff_nonneg_not_forall_nonneg (K : Type u_1) [Field K] [NumberField K] {A B : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hAB : A ≠ B) (hN : Ideal.absNorm ↑A = Ideal.absNorm ↑B) : ∃ (f : IdealArithmeticFunction K), f ≠ 0 ∧ (normCoeff K) f = 0 ∧ ¬∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), 0 ≤ f I

Rejection test. A nonnegative sum over an absolute-norm fibre does not force the individual ideal summands to be nonnegative. As soon as two distinct nonzero integral ideals share an absolute norm — for instance the two primes above 5 in ℚ(i) — the two-summand witness -1 + 1 = 0 produces a nonzero ideal arithmetic function with a negative value whose regrouping is the zero arithmetic function, hence has nonnegative coefficients.

So the hypothesis of TauCeti.summable_idealTerm_of_nonneg cannot be weakened to nonnegativity of TauCeti.normCoeff f, and TauCeti.normCoeff is not injective.