HeckeFactors.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The principal cyclic Hecke factor

The principal factor in a cyclic Artin factorization is the actual Dedekind zeta function with the finitely many Euler factors at the chosen modulus removed. A nonprincipal factor is the proved entire continuation of its realized even ray character.

lemma OAI.DukePrimeDegree.principal_artin_coefficient line 28
theorem OAI.DukePrimeDegree.principal_artinDirichlet_eq line 35
Source documentation
The principal Artin Dirichlet series agrees with the incomplete Dedekind zeta function in the half-plane of absolute convergence.
```
theorem principal_artinDirichlet_eq (N : ℕ) (hN : 0 < N)
    {s : ℂ} (hs : 1 < s.re) :
    artinDirichlet F E 1 N s =
      NumberField.dedekindZeta F s * removedEulerPolynomial F N s := by
…
```
theorem OAI.DukePrimeDegree.principal_continuation_eq_artinDirichlet line 80

theorem OAI.DukePrimeDegree.nonprincipal_continuation_eq_artinDirichlet line 90

Source documentation

The entire continuation attached to a realized nonprincipal ray character agrees with the actual Frobenius Artin Dirichlet series.

theorem nonprincipal_continuation_eq_artinDirichlet
    [NumberField.IsTotallyReal F] {d N : ℕ} [NeZero N]
    (σ : OrderedEmbeddings (d + 1) F) (hn : finrank ℚ F = d + 1)
    (χ : (E ≃ₐ[F] E) →* ℂˣ) (ψ : EvenRayCharacter F N)
    (hid : ψ.idealHom = idealHom F E χ) (hψ : ψ.IsNonprincipal)
    {s : ℂ} (hs : 1 < s.re) :
    ψ.nonprincipalContinued σ hn s = artinDirichlet F E χ N s := by
…

theorem OAI.DukePrimeDegree.exists_cyclic_ray_family line 106

Source documentation

The conductor kernel gives one common family of even ray realizations for all cyclic characters.

theorem exists_cyclic_ray_family
    [NumberField.IsTotallyReal F] [NumberField.IsTotallyReal E]
    [IsCyclic (E ≃ₐ[F] E)] (N : ℕ) (hN : 0 < N)
    (hk : ∀ χ : (E ≃ₐ[F] E) →* ℂˣ,
      PrincipalRay.KernelLaw (idealHom F E χ) N) :
    ∃ ψ : ((E ≃ₐ[F] E) →* ℂˣ) → EvenRayCharacter F N,
      (∀ χ, (ψ χ).idealHom = idealHom F E χ) ∧
      ∀ χ, χ ≠ 1 → (ψ χ).IsNonprincipal := by
…