OAI/NumberTheory/DukePrimeDegree/Arithmetic/ClassFieldRealization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Unconditional even ray realization of cyclic ideal characters

The conductor of a totally real cyclic extension has no infinite part. Arithmetic Artin reciprocity and the common rational congruence modulus therefore supply the kernel law for every actual Frobenius ideal character. This gives their realization as even ray characters.

  1. theorem OAI.DukePrimeDegree.idealCharacter_kernelLaw_of_even_modulus line 24
  2. theorem OAI.DukePrimeDegree.exists_cyclic_ray_family_unconditional line 63

    Source documentation

    Actual cyclic Frobenius characters of a totally real extension have one common even ray modulus, with the discriminant primes removed.

    theorem exists_cyclic_ray_family_unconditional
    (K L : Type) [Field K] [NumberField K] [Field L] [NumberField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)] [NumberField.IsTotallyReal K] [NumberField.IsTotallyReal L] :
    ∃ N : ℕ, 0 < N ∧ (NumberField.discr L).natAbs ∣ N ∧
      ∃ ψ : ((L ≃ₐ[K] L) →* ℂˣ) → EvenRayCharacter K N,
        (∀ χ, (ψ χ).idealHom = idealHom K L χ) ∧
        ∀ χ, χ ≠ 1 → (ψ χ).IsNonprincipal := by
…