3. Zeta factorisation for abelian extensions
For an abelian Galois extension L/K of number fields with G = \Gal{L/K}, the
Dedekind zeta function \zeta_L factors as a product of Hecke L-functions
indexed by characters of G. This is the analytic engine of the cyclotomic case
of Chebotarev.
A character of G is a group homomorphism \chi : G \to \mathbb{C}^\times.
Lean code for Definition3.1●1 definition
Associated Lean declarations
-
Chebotarev.galoisCharacter[complete]
-
Chebotarev.galoisCharacter[complete]
-
abbrevdefined in CebotarevDensity/ZetaProduct.leancomplete
abbrev Chebotarev.galoisCharacter.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Type u_2
abbrev Chebotarev.galoisCharacter.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] : Type u_2
A character of `Gal(L/K)` valued in `ℂ^×`.
For an abelian character \chi : G \to \mathbb{C}^\times, there is a function
L(\chi, \cdot) : \mathbb{C} \to \mathbb{C} such that on \operatorname{Re}(s) > 1,
L(\chi, s) \;=\; \prod_\mathfrak{p} \bigl(1 - \chi(\Frob_\mathfrak{p})\, \Norm\mathfrak{p}^{-s}\bigr)^{-1},
where the product runs over primes \mathfrak{p} of \mathcal{O}_K unramified in
L, with the convention \chi(\mathfrak{p}) = 0 on ramified primes.
Lean code for Lemma3.2●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.exists_artinLSeries_eulerProduct_abelian.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [_hAb : IsMulCommutative Gal(L/K)] (χ : Chebotarev.galoisCharacter K L) (s : ℂ) : 1 < s.re → ∏' (𝔭 : { 𝔭 // 𝔭.IsPrime ∧ Chebotarev.UnramifiedIn K L 𝔭 }), (1 - ↑(χ (Quotient.out (Chebotarev.frobeniusClass K L ↑𝔭))) * ↑(Ideal.absNorm ↑𝔭) ^ (-s))⁻¹ = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)
theorem Chebotarev.exists_artinLSeries_eulerProduct_abelian.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [_hAb : IsMulCommutative Gal(L/K)] (χ : Chebotarev.galoisCharacter K L) (s : ℂ) : 1 < s.re → ∏' (𝔭 : { 𝔭 // 𝔭.IsPrime ∧ Chebotarev.UnramifiedIn K L 𝔭 }), (1 - ↑(χ (Quotient.out (Chebotarev.frobeniusClass K L ↑𝔭))) * ↑(Ideal.absNorm ↑𝔭) ^ (-s))⁻¹ = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)
Sharifi 7.1.18 (p. 141): Euler product for an abelian Galois character `χ : Gal(L/K) → ℂ^×`. For `Re s > 1` the Euler product over unramified primes equals the Dirichlet series `Σ_𝔞 χ(𝔞) N𝔞^{-s}`, where `χ(𝔞) = galoisCharacterOnIdeal K L χ 𝔞` is the completely-multiplicative ideal character. The proof instantiates the generic weighted prime-ideal Euler product `weighted_eulerProduct_eq_tsum` with the weight `w = galoisCharacterOnIdeal K L χ` (completely multiplicative with `‖w‖ ≤ 1`). The product on the left ranges over *unramified* primes, whereas the weighted Euler product ranges over *all* nonzero primes; the two agree because `w(𝔭) = 0` at a ramified prime, so its local factor `(1 - 0)⁻¹ = 1` drops out of the product. At an unramified prime `w(𝔭) = χ(Frob 𝔭)` by `galoisCharacterOnIdeal_apply_prime`.
Sharifi Prop. 7.1.18 (p. 141). The Euler product converges absolutely on
\operatorname{Re}(s) > 1 by comparison with \zeta_K.
For each unramified prime \mathfrak{p} of \mathcal{O}_K, the local Euler factor
of \zeta_L at \mathfrak{p} factors as
\prod_{\mathfrak{P} \mid \mathfrak{p}} \bigl(1 - \Norm\mathfrak{P}^{-s}\bigr)^{-1} \;=\; \prod_\chi \bigl(1 - \chi(\Frob_\mathfrak{p})\, \Norm\mathfrak{p}^{-s}\bigr)^{-1}.
Lean code for Lemma3.3●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.dedekindZeta_local_factor_eq_product_artin_local.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (_hunr : Chebotarev.UnramifiedIn K L 𝔭) (s : ℂ) (_hs : 1 < s.re) : ∏' (𝔓 : { 𝔓 // 𝔓.IsPrime ∧ 𝔓.LiesOver 𝔭 ∧ 𝔓 ≠ ⊥ }), (1 - ↑(Ideal.absNorm ↑𝔓) ^ (-s))⁻¹ = ∏' (χ : Chebotarev.galoisCharacter K L), (1 - ↑(χ (Quotient.out (Chebotarev.frobeniusClass K L 𝔭))) * ↑(Ideal.absNorm 𝔭) ^ (-s))⁻¹
theorem Chebotarev.dedekindZeta_local_factor_eq_product_artin_local.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (_hunr : Chebotarev.UnramifiedIn K L 𝔭) (s : ℂ) (_hs : 1 < s.re) : ∏' (𝔓 : { 𝔓 // 𝔓.IsPrime ∧ 𝔓.LiesOver 𝔭 ∧ 𝔓 ≠ ⊥ }), (1 - ↑(Ideal.absNorm ↑𝔓) ^ (-s))⁻¹ = ∏' (χ : Chebotarev.galoisCharacter K L), (1 - ↑(χ (Quotient.out (Chebotarev.frobeniusClass K L 𝔭))) * ↑(Ideal.absNorm 𝔭) ^ (-s))⁻¹
Sharifi 7.1.16 (p. 141) local step: the local Euler factor at an unramified prime `𝔭` of `K` factors as a product over characters. Source quote (paraphrased identity): the local factor `∏_{𝔓|𝔭}(1-N𝔓^{-s})^{-1}` equals `∏_χ(1-χ(σ_𝔭) N𝔭^{-s})^{-1}`.
Standard cyclic-group character theory applied to the residue Galois group: the
characters of \Gal{(\mathcal{O}_L/\mathfrak{P})/(\mathcal{O}_K/\mathfrak{p})}
separate elements, and the indicated product over \chi recovers the local factor
(Sharifi 7.1.16 step at \mathfrak{p}).
For a nontrivial character \chi : G \to \mathbb{C}^\times, there is a constant
C such that
\biggl\lVert \sum_{\Norm\mathfrak{a} \le N} \chi(\mathfrak{a}) \biggr\rVert \;\le\; C \cdot N^{1 - 1/[K:\mathbb{Q}]} \qquad \text{for all } N \ge 1.
Lean code for Lemma3.4●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.character_sum_geometry_of_numbers_bound.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) : ∃ C, ∀ (N : ℕ), ‖∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ ∧ Ideal.absNorm 𝔞 ≤ N }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞‖ ≤ C * ↑N ^ (1 - (↑(Module.finrank ℚ K))⁻¹)
theorem Chebotarev.character_sum_geometry_of_numbers_bound.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) : ∃ C, ∀ (N : ℕ), ‖∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ ∧ Ideal.absNorm 𝔞 ≤ N }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞‖ ≤ C * ↑N ^ (1 - (↑(Module.finrank ℚ K))⁻¹)
Sharifi 7.1.19 step 1 (p. 142): geometry-of-numbers bound. The partial-sum character sum `Σ_{N𝔞≤N} χ(𝔞)` (with `χ(𝔞) = galoisCharacterOnIdeal K L χ 𝔞` the completely-multiplicative ideal character) is `O(N^{1-1/[K:ℚ]})` for a nontrivial character `χ`. This is the convergence input that extends `L(χ,·)` to `Z(1 - [K:ℚ]^{-1})`.
Geometry-of-numbers count of ideals in a norm-bounded region (Sharifi 7.1.19,
p. 142, step 1). The per-residue-class count is C N + O(N^{1 - 1/[K:\mathbb{Q}]});
summing over \chi(\mathfrak{a}) = \zeta for \zeta a root of unity, the C N
contributions cancel by \sum_\zeta \zeta = 0.
For every nontrivial character \chi : G \to \mathbb{C}^\times, the Dirichlet
series L(\chi, s) = \sum_{\mathfrak{a}} \chi(\mathfrak{a})\, \Norm\mathfrak{a}^{-s}
extends to a function analytic on \operatorname{Re}(s) > 1 - 1/[K:\mathbb{Q}],
agreeing with the Euler product on \operatorname{Re}(s) > 1. In particular,
L(\chi, 1) is well-defined.
Lean code for Lemma3.5●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.artinLSeries_analytic_extension.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) : ∃ Lf, AnalyticOn ℂ Lf {s | 1 - (↑(Module.finrank ℚ K))⁻¹ < s.re} ∧ ∀ (s : ℂ), 1 < s.re → Lf s = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)
theorem Chebotarev.artinLSeries_analytic_extension.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) : ∃ Lf, AnalyticOn ℂ Lf {s | 1 - (↑(Module.finrank ℚ K))⁻¹ < s.re} ∧ ∀ (s : ℂ), 1 < s.re → Lf s = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)
Sharifi 7.1.19 step 1b (p. 142) — analytic extension of `L(χ,·)`. Combining the geometry-of-numbers bound `character_sum_geometry_of_numbers_bound` with Sharifi Lemma 7.1.5 (p. 138, a generic Dirichlet-series convergence criterion given a polynomial bound on partial sums), the Dirichlet series `L(χ,s) = Σ_𝔞 χ(𝔞) N𝔞^{-s}` converges absolutely and uniformly on every compact subset of `Z(1 - 1/[K:ℚ])`, defining an analytic extension of `L(χ,·)` from `Re s > 1` to that half-plane. Source quote (verbatim, p. 142): > "By Lemma 7.1.5, we therefore have that `Σ_𝔞⊂𝓞_K χ(𝔞) N𝔞^{-s}` > converges absolutely and uniformly on every compact subset of > `Z(1 - d^{-1})`." Mathlib analogue of Sharifi Lemma 7.1.5: `LSeries.summable_of_partial_sums_le_const_mul_rpow` (or the `LSeries.tendsto_neg_logDerivLSeries_eq_*` machinery in `Mathlib.NumberTheory.LSeries.*`). **Stated at cyclotomic generality** (`L = K(μ_m)`), like the geometry-of-numbers input it rests on (`character_sum_geometry_of_numbers_bound`, leaf G — see the restatement note there, expert review 2026-06-05): the general-abelian partial-sum bound needs class field theory, while for `L = K(μ_m)` it is CFT-free. Every consumer (the non-vanishing chain, the cyclotomic Chebotarev case) instantiates at a cyclotomic extension.
Combine Lemma 3.4 (Sharifi 7.1.19 step 1a) with
Sharifi Lemma 7.1.5 (p. 138, a generic Dirichlet-series convergence criterion from a
polynomial bound on partial sums): given
\bigl|\sum_{n \le N} a_n\bigr| \le C N^{u}, the Dirichlet series
\sum_n a_n n^{-s} converges absolutely and uniformly on every compact subset of
\operatorname{Re}(s) > u. Applied to a_{\mathfrak{a}} = \chi(\mathfrak{a}) with
u = 1 - 1/[K:\mathbb{Q}], the series defines an analytic function on
\operatorname{Re}(s) > 1 - 1/[K:\mathbb{Q}].
Lean code for Lemma3.6●1 theorem
Associated Lean declarations
-
Chebotarev.artinLSeries_one_ne_zero[complete]
-
Chebotarev.artinLSeries_one_ne_zero[complete]
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.artinLSeries_one_ne_zero.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) (Lf : ℂ → ℂ) : AnalyticOn ℂ Lf {s | 1 - (↑(Module.finrank ℚ K))⁻¹ < s.re} → (∀ (s : ℂ), 1 < s.re → Lf s = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)) → Lf 1 ≠ 0
theorem Chebotarev.artinLSeries_one_ne_zero.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} K L] (hm : m % 4 ≠ 2) (χ : Chebotarev.galoisCharacter K L) (_hχ : χ ≠ 1) (Lf : ℂ → ℂ) : AnalyticOn ℂ Lf {s | 1 - (↑(Module.finrank ℚ K))⁻¹ < s.re} → (∀ (s : ℂ), 1 < s.re → Lf s = ∑' (𝔞 : { 𝔞 // 𝔞 ≠ ⊥ }), Chebotarev.galoisCharacterOnIdeal K L χ ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)) → Lf 1 ≠ 0
Sharifi 7.1.19 step 2 (p. 142): non-vanishing of `L(χ,1)` for nontrivial `χ`. Source argument: if any `L(χ,1) = 0`, the `log ζ_L = Σ_χ log L(χ,·)` decomposition leads to a sub-asymptotic strictly weaker than the simple pole `log ζ_L ~ log(1/(s-1))`, a contradiction. Uses `artinLSeries_analytic_extension` so that "`L(χ, 1)` is defined" makes sense — the extension brings `s = 1` into the analyticity domain. **Stated at cyclotomic generality** (`L = K(μ_m)`): the proof bounds every other nontrivial factor `L_{χ'}` near `s = 1` via its analytic extension (`artinDirichletSeries_norm_le_of_ne_one` ⟸ `artinLSeries_analytic_extension`), which — like the geometry-of-numbers leaf it rests on — is CFT-free only cyclotomically (see the restatement note on `exists_card_galoisCharacterOnIdeal_eq_const_mul_add_pow`, expert review 2026-06-05).
Sharifi 7.1.19 step 2 (p. 142). Write \log\zeta_L(t) = \sum_\chi \log L(\chi, t)
for t > 1. Up to a bounded function as t \to 1^+, the right side has absolute
value at least \bigl(1 - \sum_\chi m_\chi\bigr)\log(t-1)^{-1}, where m_\chi is
the order of vanishing of L(\chi, s) at s = 1. If any m_\chi \ge 1, this is
at most 0 \cdot \log(t-1)^{-1}, contradicting
\log\zeta_L(s) \sim \log(s-1)^{-1}.
Let L/K be a finite abelian Galois extension of number fields. There is a family
of functions \{L(\chi, \cdot) : \chi \in \widehat{G}\}, each holomorphic on
\operatorname{Re}(s) > 1, satisfying for \operatorname{Re}(s) > 1
\zeta_L(s) \;=\; \Bigl(\prod_{\chi \in \widehat{G}} L(\chi, s)\Bigr) \cdot R(s),
together with L(\mathbf{1}, s) = \zeta_K(s) and L(\chi, 1) \ne 0 for every
\chi \ne \mathbf{1}. Here each L(\chi, \cdot) is the Euler product over the
unramified primes only, and the correction factor R(s) is the finite product of
the local factors (1 - \Norm\mathfrak{P}^{-s})^{-1} over the primes \mathfrak{P}
of \mathcal{O}_L lying above a ramified prime of \mathcal{O}_K. The naive
identity \zeta_L = \prod_\chi L(\chi, \cdot) is false in this formulation,
because L(\chi, \cdot) drops the ramified primes whereas \zeta_L keeps them;
R collects exactly the dropped factors and is nonzero for real s > 1.
Lean code for Theorem3.7●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/ZetaProduct.leancomplete
theorem Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] {s : ℂ} (hs : 1 < s.re) : NumberField.dedekindZeta L s = (∏' (χ : Chebotarev.galoisCharacter K L), Chebotarev.artinDirichletSeries K L χ s) * ∏' (𝔓 : { 𝔓 // 𝔓.IsPrime ∧ 𝔓 ≠ ⊥ ∧ ¬Chebotarev.UnramifiedIn K L (Ideal.under (NumberField.RingOfIntegers K) 𝔓) }), (1 - ↑(Ideal.absNorm ↑𝔓) ^ (-s))⁻¹
theorem Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] [FiniteDimensional K L] [hAb : IsMulCommutative Gal(L/K)] {s : ℂ} (hs : 1 < s.re) : NumberField.dedekindZeta L s = (∏' (χ : Chebotarev.galoisCharacter K L), Chebotarev.artinDirichletSeries K L χ s) * ∏' (𝔓 : { 𝔓 // 𝔓.IsPrime ∧ 𝔓 ≠ ⊥ ∧ ¬Chebotarev.UnramifiedIn K L (Ideal.under (NumberField.RingOfIntegers K) 𝔓) }), (1 - ↑(Ideal.absNorm ↑𝔓) ^ (-s))⁻¹
**The zeta factorisation** (Sharifi 7.1.16, p. 141, with the ramified factor made explicit). For `1 < Re s`, `ζ_L(s) = (∏_χ L_χ(s)) · R(s)`, where `L_χ = artinDirichletSeries K L χ` is the Euler product over **unramified** primes only, and the correction `R(s)` is the (finite) product of the Euler factors `(1 - N𝔓^{-s})^{-1}` over the primes `𝔓` of `𝓞 L` lying over a **ramified** prime of `𝓞 K`. The naive identity `ζ_L = ∏_χ L_χ` is false: `L_χ` drops the ramified primes (its ideal coefficient `χ(𝔭)` is `0` at ramified `𝔭`), whereas `ζ_L = ∏'_{all 𝔓}(1 - N𝔓^{-s})^{-1}` keeps them; `R` collects exactly the dropped factors. Only finitely many primes ramify, each with finitely many `𝔓` above, so `R` is a finite product, nonzero for real `s > 1`.