OAI/NumberTheory/DukePrimeDegree/Arithmetic/CyclicContinuation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continued cyclic Artin factorizations

After realizing the nonprincipal cyclic characters as even ray characters, the actual Artin factorization continues away from zero and one. Its zero-order relation has nonnegative finite summands.

  1. def OAI.DukePrimeDegree.cyclicHeckeFactor line 31

    Source documentation

    The principal factor is the incomplete Dedekind zeta function; the other factors are the entire continuations of the realized characters.

    def cyclicHeckeFactor (σ : OrderedEmbeddings (d + 1) F)
    (hn : finrank ℚ F = d + 1)
    (ψ : ((E ≃ₐ[F] E) →* ℂˣ) → EvenRayCharacter F N)
    (χ : (E ≃ₐ[F] E) →* ℂˣ) : ℂ → ℂ :=
…
  2. theorem OAI.DukePrimeDegree.cyclicHeckeFactor_eq_artinDirichlet line 38
  3. theorem OAI.DukePrimeDegree.cyclicHeckeFactor_analytic line 53
  4. theorem OAI.DukePrimeDegree.cyclicHeckeFactor_finite_nonnegative_order line 69
  5. theorem OAI.DukePrimeDegree.cyclicHeckeFactor_product_eq line 99
  6. theorem OAI.DukePrimeDegree.cyclicHeckeFactor_sum_orders line 125