Arithmetic functions on nonzero ideals

For the intended number-field applications, an ideal-indexed Dirichlet series should not assign an arithmetic coefficient to the zero ideal. Excluding it ensures that ideal convolution never considers factorizations through the zero ideal. This file introduces the carrier used throughout the arithmetic-Dirichlet-series roadmap, parameterized over an arbitrary field:

• TauCeti.IdealArithmeticFunction K is a complex-valued function on the nonzero ideals of 𝓞 K;
• TauCeti.IdealArithmeticFunction.zeroExtend is its canonical extension to all integral ideals, with value zero at the zero ideal;
• TauCeti.IdealArithmeticFunction.restrict restricts a function on all ideals to the nonzero ideals;
• TauCeti.IdealArithmeticFunction.map and TauCeti.IdealArithmeticFunction.mapEquiv: functoriality under an isomorphism K ≃+* L of the ambient fields.

It also carries the multiplicativity predicate TauCeti.IdealArithmeticFunction.IsMultiplicative — value 1 at the unit ideal, multiplicative on relatively prime nonzero ideals — together with its two factorization consequences: IsMultiplicative.map_prod for a pairwise relatively prime finite product, and, over a number field, IsMultiplicative.map_prod_pow for a prime-power factorization of a nonzero ideal, the factorizations themselves being supplied by Ideal.exists_eq_prod_pow.

The two operations are inverse precisely on functions vanishing at the zero ideal. The resulting existence-and-uniqueness API is recorded without exposing the implementation of zeroExtend: TauCeti.IdealArithmeticFunction.existsUnique_zeroExtend_eq characterizes its image, while TauCeti.IdealArithmeticFunction.zeroExtend_injective says that no information is lost.

The extension respects the pointwise additive, scalar, and multiplicative operations. It does not preserve the pointwise unit: the constant-one function on all ideals takes value one at the zero ideal, and therefore cannot be a zero extension. The theorem TauCeti.IdealArithmeticFunction.not_exists_zeroExtend_eq_one is the zero-ideal rejection test required by Layer 0 of the roadmap.

Roadmap role

This is Layer 0.1 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md, and is the common carrier on which its norm regrouping, ideal convolution, Euler products, and summatory functions are built. Later Layer 0 files add completely multiplicative and unitary subtypes; those are special coefficient systems on this general carrier, not replacements for it.

References

• TauCetiRoadmap/ArithmeticDirichletSeries/Suggested.lean, whose Layer 0.1 nonzero-ideal carrier and zero-extension design are adapted here.
• J. Neukirch, Algebraic Number Theory, Chapter VII.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapters II--III.

@[reducible, inline]

abbrev TauCeti.IdealArithmeticFunction (K : Type u_1) [Field K] : Type u_1

An ideal arithmetic function over a field K: a complex-valued function on the nonzero ideals of 𝓞 K.

The domain is (Ideal (𝓞 K))⁰, Mathlib's non-zero-divisor submonoid. Since the ring of integers is a domain, its elements are exactly the ideals different from ⊥. For number fields, keeping ⊥ out of the carrier ensures that later divisor sums use only the nonzero-ideal factorization theory.

Equations

• TauCeti.IdealArithmeticFunction K = (↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → ℂ)

structure TauCeti.IdealArithmeticFunction.IsMultiplicative {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : Prop

An ideal arithmetic function is multiplicative when it takes the unit ideal to 1 and respects products of relatively prime nonzero ideals. This is weaker than the complete multiplicativity carried by MultiplicativeIdealWeight.

• map_one : f 1 = 1

  A multiplicative ideal arithmetic function takes the unit ideal to 1.

• map_mul_of_isRelPrime {I J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))} (hIJ : IsRelPrime ↑I ↑J) : f (I * J) = f I * f J

  A multiplicative ideal arithmetic function respects products of relatively prime ideals.

theorem TauCeti.IdealArithmeticFunction.isMultiplicative_one {K : Type u_1} [Field K] : IsMultiplicative 1

The everywhere-one ideal arithmetic function is multiplicative.

theorem TauCeti.IdealArithmeticFunction.IsMultiplicative.mul {K : Type u_1} [Field K] {f g : IdealArithmeticFunction K} (hf : f.IsMultiplicative) (hg : g.IsMultiplicative) : (f * g).IsMultiplicative

Pointwise products of multiplicative ideal arithmetic functions are multiplicative.

theorem TauCeti.IdealArithmeticFunction.IsMultiplicative.star {K : Type u_1} [Field K] {f : IdealArithmeticFunction K} (hf : f.IsMultiplicative) : (Star.star f).IsMultiplicative

Complex conjugation preserves multiplicativity of ideal arithmetic functions.

theorem TauCeti.IdealArithmeticFunction.IsMultiplicative.map_prod {K : Type u_1} [Field K] {f : IdealArithmeticFunction K} [DecompositionMonoid (Ideal (NumberField.RingOfIntegers K))] (hf : f.IsMultiplicative) {ι : Type u_2} (g : ι → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (s : Finset ι) (hs : (↑s).Pairwise fun (i j : ι) => IsRelPrime ↑(g i) ↑(g j)) : f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)

A multiplicative ideal arithmetic function factors over pairwise relatively prime products. This is the ideal analogue of Mathlib's ArithmeticFunction.IsMultiplicative.map_prod.

Passing from a pairwise hypothesis to relative primality against the whole product is exactly Mathlib's IsRelPrime.prod_right, which needs DecompositionMonoid (Ideal (𝓞 K)); that is all the ambient arithmetic this statement uses, and [NumberField K] supplies it.

theorem TauCeti.IdealArithmeticFunction.IsMultiplicative.map_prod_pow {K : Type u_1} [Field K] {f : IdealArithmeticFunction K} [NumberField K] (hf : f.IsMultiplicative) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (e : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) → ℕ) (A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hA : ↑A = ∏ P ∈ S, P.asIdeal ^ e P) : f A = ∏ P ∈ S, f ⟨P.asIdeal ^ e P, ⋯⟩

A multiplicative ideal arithmetic function factors over a prime-power factorization. Unique factorization writes every nonzero ideal as a product ∏ P ∈ S, P ^ e P over a finite set of height-one primes (Ideal.exists_eq_prod_pow), and a multiplicative f takes such a product to the product of its values on the prime powers.

noncomputable def TauCeti.IdealArithmeticFunction.zeroExtend {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : Ideal (NumberField.RingOfIntegers K) → ℂ

Extend an ideal arithmetic function to all integral ideals by assigning zero to ⊥.

Use zeroExtend_bot and zeroExtend_coe to simplify its two characteristic cases, rather than unfolding this definition.

Equations

• f.zeroExtend I = Function.extend Subtype.val f 0 I

def TauCeti.IdealArithmeticFunction.restrict {K : Type u_1} [Field K] (g : Ideal (NumberField.RingOfIntegers K) → ℂ) : IdealArithmeticFunction K

Restrict a function on all integral ideals to the nonzero ideals.

Equations

• TauCeti.IdealArithmeticFunction.restrict g I = g ↑I

@[simp]

theorem TauCeti.IdealArithmeticFunction.restrict_apply {K : Type u_1} [Field K] (g : Ideal (NumberField.RingOfIntegers K) → ℂ) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : restrict g I = g ↑I

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_bot {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : f.zeroExtend ⊥ = 0

The zero extension is zero at the zero ideal.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_of_ne {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) {I : Ideal (NumberField.RingOfIntegers K)} (hI : I ≠ ⊥) : f.zeroExtend I = f ⟨I, ⋯⟩

Away from ⊥, the zero extension is the original ideal arithmetic function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_coe {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) : f.zeroExtend ↑I = f I

The zero extension agrees with the original function on every nonzero ideal.

@[simp]

theorem TauCeti.IdealArithmeticFunction.restrict_zeroExtend {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : restrict f.zeroExtend = f

Restricting a zero extension recovers the original ideal arithmetic function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_restrict {K : Type u_1} [Field K] {g : Ideal (NumberField.RingOfIntegers K) → ℂ} (hg : g ⊥ = 0) : (restrict g).zeroExtend = g

Extending a restriction recovers a function on all ideals exactly when it vanishes at ⊥.

theorem TauCeti.IdealArithmeticFunction.exists_zeroExtend_eq_iff {K : Type u_1} [Field K] {g : Ideal (NumberField.RingOfIntegers K) → ℂ} : (∃ (f : IdealArithmeticFunction K), f.zeroExtend = g) ↔ g ⊥ = 0

A function on all ideals is a zero extension if and only if it vanishes at ⊥.

theorem TauCeti.IdealArithmeticFunction.zeroExtend_injective {K : Type u_1} [Field K] : Function.Injective zeroExtend

Zero extension is injective: its values on nonzero ideals retain the entire function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_eq_iff {K : Type u_1} [Field K] {f g : IdealArithmeticFunction K} : f.zeroExtend = g.zeroExtend ↔ f = g

Two zero extensions agree exactly when the underlying ideal arithmetic functions agree.

theorem TauCeti.IdealArithmeticFunction.existsUnique_zeroExtend_eq {K : Type u_1} [Field K] {g : Ideal (NumberField.RingOfIntegers K) → ℂ} (hg : g ⊥ = 0) : ∃! f : IdealArithmeticFunction K, f.zeroExtend = g

A function on all ideals that vanishes at ⊥ is the zero extension of a unique ideal arithmetic function.

theorem TauCeti.IdealArithmeticFunction.zeroExtend_eq_zero_iff {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), f I ≠ 0) {I : Ideal (NumberField.RingOfIntegers K)} : f.zeroExtend I = 0 ↔ I = ⊥

The zero extension is zero exactly at ⊥ when the original function has no zero values.

theorem TauCeti.IdealArithmeticFunction.zeroExtend_ne_zero {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) (hf : ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), f I ≠ 0) {I : Ideal (NumberField.RingOfIntegers K)} (hI : I ≠ ⊥) : f.zeroExtend I ≠ 0

If the original function does not vanish, its zero extension is nonzero at every nonzero ideal.

Compatibility with pointwise operations

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_zero {K : Type u_1} [Field K] : zeroExtend 0 = 0

Zero extension preserves the pointwise zero function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_add {K : Type u_1} [Field K] (f g : IdealArithmeticFunction K) : (f + g).zeroExtend = f.zeroExtend + g.zeroExtend

Zero extension preserves pointwise addition.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_neg {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : (-f).zeroExtend = -f.zeroExtend

Zero extension preserves pointwise negation.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_sub {K : Type u_1} [Field K] (f g : IdealArithmeticFunction K) : (f - g).zeroExtend = f.zeroExtend - g.zeroExtend

Zero extension preserves pointwise subtraction.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_smul {K : Type u_1} [Field K] (c : ℂ) (f : IdealArithmeticFunction K) : (c • f).zeroExtend = c • f.zeroExtend

Zero extension preserves pointwise complex scalar multiplication.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_mul {K : Type u_1} [Field K] (f g : IdealArithmeticFunction K) : (f * g).zeroExtend = f.zeroExtend * g.zeroExtend

Zero extension preserves pointwise multiplication.

theorem TauCeti.IdealArithmeticFunction.not_exists_zeroExtend_eq_one {K : Type u_1} [Field K] : ¬∃ (f : IdealArithmeticFunction K), f.zeroExtend = 1

Rejection test. The everywhere-one function on all integral ideals is not the zero extension of any ideal arithmetic function, since its value at ⊥ is one rather than zero. This is the roadmap's zero-ideal rejection test. Compare TauCeti.IdealArithmeticFunction.zeroExtend_one_apply, which computes the zero extension of the constant function 1 on the nonzero ideals.

theorem TauCeti.IdealArithmeticFunction.zeroExtend_one_apply {K : Type u_1} [Field K] (I : Ideal (NumberField.RingOfIntegers K)) : zeroExtend 1 I = if I = ⊥ then 0 else 1

The constant-one function on nonzero ideals extends to the indicator of ideals unequal to ⊥.

Functoriality under an isomorphism of fields

noncomputable def TauCeti.IdealArithmeticFunction.map {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction K) : IdealArithmeticFunction L

Transport along an isomorphism of fields. An isomorphism e : K ≃+* L carries an ideal arithmetic function for K to one for L: the value at a nonzero ideal of 𝓞 L is the value of f at its preimage in 𝓞 K under NumberField.RingOfIntegers.mapRingEquiv e.

Equations

• TauCeti.IdealArithmeticFunction.map e f J = f.zeroExtend (Ideal.comap (NumberField.RingOfIntegers.mapRingEquiv e) ↑J)

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction K) (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers L)))) : map e f J = f.zeroExtend (Ideal.comap (NumberField.RingOfIntegers.mapRingEquiv e) ↑J)

Defining equation of TauCeti.IdealArithmeticFunction.map: the value at a nonzero ideal of 𝓞 L is the zero extension of f at its preimage in 𝓞 K.

@[simp]

theorem TauCeti.IdealArithmeticFunction.zeroExtend_map {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction K) (I : Ideal (NumberField.RingOfIntegers L)) : (map e f).zeroExtend I = f.zeroExtend (Ideal.comap (NumberField.RingOfIntegers.mapRingEquiv e) I)

Transport is compatible with extension by zero: both extensions send an ideal of 𝓞 L to the value of f at its preimage in 𝓞 K, the zero ideal included.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_id {K : Type u_1} [Field K] (f : IdealArithmeticFunction K) : map (RingEquiv.refl K) f = f

Transporting along the identity field isomorphism is the identity.

theorem TauCeti.IdealArithmeticFunction.map_map {K : Type u_1} [Field K] {L : Type u_2} {M : Type u_3} [Field L] [Field M] (e : K ≃+* L) (e' : L ≃+* M) (f : IdealArithmeticFunction K) : map e' (map e f) = map (e.trans e') f

Transport is functorial: transporting along e and then along e' is the same as transporting along e.trans e'.

noncomputable def TauCeti.IdealArithmeticFunction.mapEquiv {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) : IdealArithmeticFunction K ≃ IdealArithmeticFunction L

Transport along an isomorphism of fields, as an equivalence of the two carriers, with inverse the transport along e.symm.

Equations

• TauCeti.IdealArithmeticFunction.mapEquiv e = { toFun := TauCeti.IdealArithmeticFunction.map e, invFun := TauCeti.IdealArithmeticFunction.map e.symm, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.IdealArithmeticFunction.mapEquiv_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction K) : (mapEquiv e) f = map e f

Evaluation of mapEquiv.

@[simp]

theorem TauCeti.IdealArithmeticFunction.mapEquiv_symm_apply {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction L) : (mapEquiv e).symm f = map e.symm f

Evaluation of the inverse of mapEquiv.

Transport preserves the pointwise structure inherited from Pi.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_zero {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) : map e 0 = 0

Transport preserves the pointwise zero function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_one {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) : map e 1 = 1

Transport preserves the pointwise one function.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_add {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f g : IdealArithmeticFunction K) : map e (f + g) = map e f + map e g

Transport preserves pointwise addition.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_mul {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f g : IdealArithmeticFunction K) : map e (f * g) = map e f * map e g

Transport preserves pointwise multiplication.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_neg {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f : IdealArithmeticFunction K) : map e (-f) = -map e f

Transport preserves pointwise negation.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_sub {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (f g : IdealArithmeticFunction K) : map e (f - g) = map e f - map e g

Transport preserves pointwise subtraction.

@[simp]

theorem TauCeti.IdealArithmeticFunction.map_smul {K : Type u_1} [Field K] {L : Type u_2} [Field L] (e : K ≃+* L) (c : ℂ) (f : IdealArithmeticFunction K) : map e (c • f) = c • map e f

Transport preserves pointwise complex scalar multiplication.