Indexing the prime-power ideals by a prime and an exponent

Every prime-power ideal of 𝓞 K is 𝔭 ^ (k + 1) for a unique height-one prime 𝔭 and a unique k : ℕ. This file records that bijection and what it does to an infinite sum: a summable family on the prime-power ideals has the same sum as the iterated sum over primes and exponents, and a summable family on all nonzero ideals collapses to that same iterated sum whenever it is supported on prime powers. Both statements assume summability; neither asserts it.

This is the ideal analogue of Mathlib's Nat.Primes.prodNatEquiv and the two summation lemmas built on it, tsum_primes_pow_eq and tsum_eq_tsum_primes_of_support_subset_prime_powers. Those are what turns an Euler-product logarithm, which is naturally indexed by (𝔭, k), into a Dirichlet series indexed by ideals — the shape a von Mangoldt coefficient identity needs.

Main definitions

• IsDedekindDomain.HeightOneSpectrum.idealPrimePowerOf: the prime-power ideal 𝔭 ^ (k + 1).
• TauCeti.idealPrimePowerEquiv: the bijection (𝔭, k) ↦ 𝔭 ^ (k + 1) onto the prime-power ideals.

Main results

• TauCeti.summable_comp_idealPrimePowerOf: a summable family on all nonzero ideals remains summable after restriction to the positive prime powers.
• TauCeti.summable_tsum_norm_idealPrimePowerOf: the prime-power tails of an absolutely summable ideal-indexed family are summable over the primes.
• TauCeti.tsum_idealPrimePower_eq: a summable family on the prime-power ideals has the same sum as the iterated sum over primes and exponents.
• TauCeti.tsum_eq_tsum_idealPrimePower_of_support_subset: a summable family on the nonzero ideals supported on prime powers has the same sum as that iterated sum.

Implementation notes

The inverse sends A to (primePowerBase A, primePowerExponent A - 1). The truncated subtraction is harmless because primePowerExponent A is positive, and the + 1 in the forward map is what keeps the exponent positive without carrying a hypothesis.

def IsDedekindDomain.HeightOneSpectrum.idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ) : TauCeti.IdealPrimePower K

The prime-power ideal 𝔭 ^ (k + 1).

Equations

• P.idealPrimePowerOf k = ⟨⟨P.asIdeal ^ (k + 1), ⋯⟩, ⋯⟩

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.coe_idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ) : ↑↑(P.idealPrimePowerOf k) = P.asIdeal ^ (k + 1)

theorem IsDedekindDomain.HeightOneSpectrum.coe_idealPrimePowerOf_eq_primeIdealPow {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (e : ℕ) : ↑(P.idealPrimePowerOf e) = P.primeIdealPow (e + 1)

The two representations of the positive power P ^ (e + 1) as a nonzero ideal agree.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.primePowerBase_idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ) : TauCeti.primePowerBase (P.idealPrimePowerOf k) = P

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.primePowerExponent_idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ) : TauCeti.primePowerExponent (P.idealPrimePowerOf k) = k + 1

noncomputable def TauCeti.idealPrimePowerEquiv {K : Type u_1} [Field K] [NumberField K] : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ ≃ IdealPrimePower K

A prime-power ideal is a prime and an exponent. The bijection (𝔭, k) ↦ 𝔭 ^ (k + 1) from height-one primes and natural numbers onto the prime-power ideals of 𝓞 K.

This is the ideal analogue of Nat.Primes.prodNatEquiv.

Equations

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.idealPrimePowerEquiv_apply {K : Type u_1} [Field K] [NumberField K] (P : HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ) : TauCeti.idealPrimePowerEquiv (P, k) = P.idealPrimePowerOf k

@[simp]

theorem TauCeti.idealPrimePowerEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] (A : IdealPrimePower K) : idealPrimePowerEquiv.symm A = (primePowerBase A, primePowerExponent A - 1)

The inverse of the prime-power indexing bijection is the prime base of a prime-power ideal together with its exponent, lowered by one.

theorem TauCeti.summable_comp_idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] {α : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → α} (hf : Summable f) : Summable fun (Pk : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) × ℕ) => f ↑(Pk.1.idealPrimePowerOf Pk.2)

Restricting a summable family on the nonzero ideals to the positive prime powers preserves summability.

theorem TauCeti.summable_tsum_norm_idealPrimePowerOf {K : Type u_1} [Field K] [NumberField K] {β : Type u_3} [NormedAddCommGroup β] {g : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → β} (hg : Summable fun (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) => ‖g I‖) : Summable fun (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => ∑' (e : ℕ), ‖g ↑(P.idealPrimePowerOf e)‖

The prime-power tails of an absolutely summable ideal-indexed family are summable over the primes. Restricting the norms to the pairs (P, e) and then summing out the exponent leaves a summable family on the height-one primes.

theorem TauCeti.tsum_idealPrimePower_eq {K : Type u_1} [Field K] [NumberField K] {α : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] [T0Space α] {g : IdealPrimePower K → α} (hg : Summable g) : ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ), g (P.idealPrimePowerOf k) = ∑' (A : IdealPrimePower K), g A

Summing over prime-power ideals is summing over primes and exponents. Stated for an arbitrary family on the prime-power ideals, not only for one restricted from the nonzero ideals.

theorem TauCeti.tsum_eq_tsum_idealPrimePower_of_support_subset {K : Type u_1} [Field K] [NumberField K] {α : Type u_2} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → α} [T0Space α] (hfm : Summable f) (hf : Function.support f ⊆ {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | IsPrimePow ↑A}) : ∑' (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), f A = ∑' (P : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (k : ℕ), f ↑(P.idealPrimePowerOf k)

A sum supported on prime powers is a sum over primes and exponents.