Definitions/Def_NumberField_CompletedRayL.lean

Throughout, K is a number field. For a modulus \mathfrak f \subseteq \mathcal O_K, a class C in the narrow ray class group \mathtt{NarrowRayClassGroup}\,K\,\mathfrak f — the quotient of the subgroup coprimeToModulus K 𝔣 of invertible fractional ideals whose valuation \mathrm{count}_v vanishes at every height-one prime v dividing \mathfrak f, by the subgroup generated by the principal ideals (\alpha) with \alpha \neq 0, \alpha - 1 \in \mathfrak f and \tau(\alpha) > 0 for every ring homomorphism \tau \colon K \to \mathbb R — and a natural number n, rayZetaCoeff K 𝔣 C n is the cardinality (as a Nat.card, hence 0 on an infinite type) of the type of nonzero integral ideals I of \mathcal O_K with \mathrm{N}(I) = n such that the associated invertible fractional ideal FractionalIdeal.mk0 K I lies in coprimeToModulus K 𝔣 and its narrow ray class is C.

Then rayZeta K 𝔣 C s is Mathlib's LSeries of the coefficient function n \mapsto rayZetaCoeff K 𝔣 C n, that is \sum_{n \ge 1} \mathrm{rayZetaCoeff}(n)\, n^{-s} as a tsum, so it takes the value 0 where the series fails to be summable. For a monoid homomorphism \chi from the narrow ray class group to \mathbb C, rayClassLSeries K 𝔣 χ s is the unrestricted sum \sum_C' \chi(C)\, \zeta(s, C) over all classes. Finally, for a finite set S of real infinite places of K, completedRayL K 𝔣 χ S s is (|d_K| \cdot \mathrm{N}\mathfrak f)^{s/2} \, \Gamma_{\mathbb R}(s)^{r_1 - \#S} \, \Gamma_{\mathbb R}(s+1)^{\#S} \, \Gamma_{\mathbb C}(s)^{r_2} \, L(s, \chi), with r_1, r_2 the numbers of real and complex places, \Gamma_{\mathbb R} and \Gamma_{\mathbb C} Mathlib's Deligne \Gamma-factors, and the exponent r_1 - \#S formed by truncated subtraction of natural numbers. The set S records the signature of \chi at the real places only through these \Gamma-factors; no compatibility between \chi and S, and no primitivity or finiteness condition on \mathfrak f or \chi, is imposed in the definitions, which are therefore total.