Canonical local factors and formal Euler products for ideal arithmetic functions #
This file develops the Euler-product layer for arithmetic functions on nonzero ideals. It builds
the canonical formal power series at each height-one prime and sends that series into Mathlib's
ArithmeticFunction.ofPowerSeries API. The resulting local arithmetic factor has the prescribed
prime-power values and vanishes away from powers of the prime-ideal norm.
It then restricts an ideal arithmetic function to the nonzero ideals whose prime factors lie in a prescribed set of height-one primes, and proves that for a finite set of primes the norm coefficients of that restriction are exactly the product of the local factors, taken in Mathlib's Dirichlet convolution of arithmetic functions. Passing to Mathlib's formal Euler product gives the norm coefficients of the original function. Everything here is a formal identity of coefficients: no analytic convergence hypothesis enters.
Main definitions #
TauCeti.IdealArithmeticFunction.localPowerSerieshas coefficientf (P ^ n)atn.TauCeti.IdealArithmeticFunction.localArithmeticFactorrealizes that power series as an arithmetic function supported on powers ofN(P).TauCeti.IdealArithmeticFunction.supportedPart f Sisfrestricted to the nonzero ideals all of whose prime factors lie inS, and zero elsewhere.
Main results #
TauCeti.IdealArithmeticFunction.supportedPart_insert: for a multiplicativef, adjoining one prime to the support convolves the restriction with the restriction to the powers of that prime.TauCeti.IdealArithmeticFunction.normCoeff_supportedPart: the finite Euler productnormCoeff (supportedPart f S) = ∏ P ∈ S, localArithmeticFactor f Pfor a multiplicativefand a finite setSof height-one primes.TauCeti.IdealArithmeticFunction.normCoeff_eq_eulerProduct: the norm coefficients of a multiplicative ideal arithmetic function are Mathlib's formal Euler product of its canonical local factors.
Implementation notes #
"Supported on S" is spelled Ideal.IsPrimeTo · Sᶜ: no prime outside S divides the ideal.
That predicate, and the splitting Ideal.IsPrimeTo.exists_eq_pow_mul of an ideal into a prime
power times a cofactor together with its uniqueness Ideal.eq_and_eq_of_pow_mul_eq_pow_mul, live
in TauCeti/RingTheory/DedekindDomain/Ideal.lean, since nothing in them is specific to a number
field. Uniqueness is what makes the induction work: it is why exactly one summand of the ideal
convolution survives at each ideal. The multiplicativity of f over a prime-power factorization,
TauCeti.IdealArithmeticFunction.IsMultiplicative.map_prod_pow, likewise lives with the predicate
it elaborates, in TauCeti/NumberTheory/ArithmeticDirichletSeries/Basic.lean.
TauCeti.MultiplicativeIdealWeight.restrict is the opposite regime and is not a substitute:
it restricts away from a finite set of primes and stays inside the bundled weight carrier. A
finite Euler product needs support on a finite set of primes, so all but finitely many primes are
bad; such a function is never a MultiplicativeIdealWeight, whose zero support is finite by
definition. Hence supportedPart is a plain ideal arithmetic function.
Finiteness is what carries the finite products to the full Euler product. A nonzero ideal has
only finitely many prime divisors, and only finitely many primes have norm at most a given n, so
at a fixed norm coefficient the restriction supportedPart f S already agrees with f as soon as
S contains those primes. Each finite product is therefore eventually the exact norm coefficient,
and Mathlib's ArithmeticFunction.eulerProduct, being the limit of those finite products, computes
the norm coefficients of f itself. The local factors are derived from f rather than stored, so
this identity holds for any multiplicative f with no further data.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII.
- Mathlib's
ArithmeticFunction.ofPowerSeriesandArithmeticFunction.eulerProductAPIs. TauCetiRoadmap/ArithmeticDirichletSeries/Suggested.lean, whose local-factor target signatures and naming are adapted here.
The e-th power of a height-one prime of 𝓞 K, as a nonzero integral ideal.
Instances For
A prime power, as a nonzero integral ideal, has the expected underlying ideal.
The absolute norm is multiplicative on prime powers.
Distinct primes give distinct first powers, so a family indexed by the primes is a subfamily of one indexed by the nonzero ideals.
Distinct exponents give distinct prime powers.
Every nonzero ideal is eventually supported. A finite set of height-one primes that
contains all primes of norm at most Ideal.absNorm A already contains every prime divisor of A,
and those bounded-norm sets are cofinal by the Northcott property of the absolute norm.
The canonical local power series of f at a height-one prime P; its coefficient at n is
the value of f at the nonzero ideal P ^ n.
Equations
- f.localPowerSeries P = PowerSeries.mk fun (n : ℕ) => f ⟨P.asIdeal ^ n, ⋯⟩
Instances For
Coefficients of the canonical local power series are the prime-power values of f.
The constant coefficient of the canonical local power series is f 1.
The canonical local arithmetic factor at P, obtained by substituting N(P)⁻ˢ into the
formal prime-power series through Mathlib's ArithmeticFunction.ofPowerSeries.
Equations
Instances For
The canonical local arithmetic factor is Mathlib's arithmetic function associated to the
local power series at P.
At a power of N(P), the local arithmetic factor is the corresponding value at P ^ n.
A local arithmetic factor vanishes away from powers of its prime-ideal norm.
A nonzero value of a local arithmetic factor is supported on a power of the prime-ideal norm.
If f takes the unit ideal to 1, each canonical local arithmetic factor is a
multiplicative arithmetic function.
If f takes the unit ideal to 1, the formal Euler product of its canonical local factors is
multiplicative as an arithmetic function.
At each coefficient, finite products of the canonical local factors eventually equal their formal Euler product.
The canonical local power series of the convolution identity is the constant series 1.
Every canonical local arithmetic factor of the convolution identity is 1.
Finite Euler products #
The part of f supported on the nonzero ideals all of whose prime factors lie in S: it
agrees with f there and vanishes on every other nonzero ideal. Being supported on S is
Ideal.IsPrimeTo · Sᶜ, that no prime outside S divides the ideal. Use
supportedPart_apply_of_isPrimeTo_compl and supportedPart_apply_of_not_isPrimeTo_compl rather
than unfolding.
Equations
- f.supportedPart S = {A : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) | (↑A).IsPrimeTo Sᶜ}.indicator f
Instances For
On an ideal supported on S, the restriction of f to S is f.
On an ideal with a prime factor outside S, the restriction of f to S vanishes.
The restriction of f to S is supported on the ideals supported on S.
The unit ideal is supported on every set of primes. This is not marked @[simp]: simp
already reaches it through supportedPart_apply_of_isPrimeTo_compl.
Restricting a multiplicative ideal arithmetic function to the ideals supported on S keeps it
multiplicative: an ideal is supported on S exactly when both factors of a product are.
Every nonzero ideal is supported on the set of all height-one primes.
Only the unit ideal is supported on no prime at all, so the empty restriction of a function
taking the value 1 there is the convolution identity.
Splitting off one prime. For a multiplicative f, adjoining a prime P ∉ S to the support
convolves the restriction to S with the restriction to the powers of P; the factorization of an
ideal supported on insert P S into its P-part and its S-part is unique, so exactly one
summand of the convolution survives.
The norm coefficients of the restriction to the powers of a single prime P are exactly its
canonical local arithmetic factor.
The finite Euler product. For a multiplicative ideal arithmetic function, the norm
coefficients of its restriction to the ideals supported on a finite set S of height-one primes
are the product, in Mathlib's Dirichlet convolution of arithmetic functions, of the canonical
local factors at the primes of S.
At a fixed coefficient, restricting to a sufficiently large finite set of prime ideals does not change the norm coefficient: the norm fibre is finite, and each of its members is eventually supported.
The formal Euler product of norm coefficients. The norm coefficients of a multiplicative
ideal arithmetic function are Mathlib's ArithmeticFunction.eulerProduct of the canonical local
arithmetic factors. This is an equality of arithmetic functions; the analytic infinite product
obtained after evaluating their LSeries is a separate absolute-convergence question.