Euler-product coefficient data over a number field #
This file bundles the algebraic input for an Euler product over the height-one primes of the ring
of integers of a number field. An EulerProductData K consists of an ideal arithmetic function
that is multiplicative on relatively prime nonzero ideals. The prime-power series and local
arithmetic factors are canonically derived from the function as defined in
EulerProduct/Basic.lean, so nothing about the local behaviour is stored: the bundle carries
exactly the one algebraic hypothesis that an Euler product consumes.
The formal Euler-product identity follows from
IdealArithmeticFunction.normCoeff_eq_eulerProduct: coprime multiplicativity and unique
factorization prove that normCoeff is Mathlib's ArithmeticFunction.eulerProduct of the
canonical local factors.
Two hypotheses of the classical theory are deliberately absent, because the identity proved here does not need either. There is no distinguished finite set of exceptional primes: multiplicativity is required on every coprime pair of nonzero ideals, and the local factor at a prime is read off from the coefficients at its powers, good or bad. There is also no analytic input: the identity is an equality of arithmetic functions, and the convergence of the evaluated factors to an infinite product is a separate question.
Main definitions #
TauCeti.EulerProductDatabundles a multiplicative ideal coefficient system.TauCeti.EulerProductData.ofMultiplicativeIdealWeightregards a degree-one ideal weight as Euler-product data.- Pointwise multiplication, complex conjugation, and restriction away from sets of primes preserve the bundle.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII.
- Mathlib's
ArithmeticFunction.ofPowerSeriesandArithmeticFunction.eulerProductAPIs.
The algebraic coefficient data of an ideal Euler product. The local prime-power series is
canonically derived from toIdealArithmeticFunction.
- toIdealArithmeticFunction : IdealArithmeticFunction K
The coefficients indexed by nonzero integral ideals.
- isMultiplicative : self.toIdealArithmeticFunction.IsMultiplicative
Coprime multiplicativity, the exact algebraic hypothesis used by an Euler product.
Instances For
The canonical local power series of bundled Euler-product data at a height-one prime.
Equations
Instances For
Coefficients of the bundled local power series are the prime-power values of the data.
The degree-zero prime-power coefficient is one.
The local power series has constant coefficient one.
The canonical local arithmetic factor of bundled Euler-product data at a height-one prime.
Equations
Instances For
The bundled local arithmetic factor is the canonical factor of its coefficient function.
The bundled local arithmetic factor is Mathlib's arithmetic function associated to the
bundled local power series at P.
At a power of N(P), the bundled local arithmetic factor is the corresponding prime-power
coefficient.
Away from the powers of N(P), the bundled local arithmetic factor vanishes. Together with
localArithmeticFactor_apply_pow this determines it at every natural number.
The norm coefficients of bundled Euler-product data are the formal Euler product of its canonical local arithmetic factors.
A completely multiplicative ideal weight supplies Euler-product data.
Equations
- TauCeti.EulerProductData.ofMultiplicativeIdealWeight χ = { toIdealArithmeticFunction := χ.toIdealArithmeticFunction, isMultiplicative := ⋯ }
Instances For
The coefficient function underlying the Euler-product data of a multiplicative ideal weight.
The pointwise product of two Euler-product coefficient systems.
Equations
- One or more equations did not get rendered due to their size.
The trivial ideal coefficient system as Euler-product data.
Equations
Pointwise multiplication makes Euler-product data a commutative monoid. This product remains distinct from ideal Dirichlet convolution.
Equations
- One or more equations did not get rendered due to their size.
Complex conjugation makes Euler-product data a star monoid.
Equations
- One or more equations did not get rendered due to their size.
Restrict Euler-product data away from a set of height-one primes, leaving its coefficients unchanged on ideals prime to that set and setting the others to zero.
Equations
- D.restrictAway S = { toIdealArithmeticFunction := D.toIdealArithmeticFunction.supportedPart Sᶜ, isMultiplicative := ⋯ }