OAI/NumberTheory/DukePrimeDegree/Arithmetic/ClassFieldBridge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic Artin map realizes the actual ideal character

Prime-to-modulus ideals are generated by primes outside the modulus. At unramified primes the arithmetic Artin element agrees with the Frobenius used by the ideal-character Dirichlet series. Thus principal ray ideals lie in the kernel of the actual ideal character.

  1. theorem OAI.DukePrimeDegree.idealCharacter_eq_artin_comp line 31

    Source documentation

    Agreement at unramified primes identifies the genuine ideal character with composition through the arithmetic Artin map.

    theorem idealCharacter_eq_artin_comp
    (m : RayClass.Modulus K)
    (hm : m.congruenceSubgroup ≤ (ideleClassNorm K L).range)
    (hunram : ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      v ∉ m.finitePart.support →
      Algebra.IsUnramifiedAt (𝓞 K) (primeAbove K L v).val)
    (χ : (L ≃ₐ[K] L) →* ℂˣ) :
    (idealHom K L χ).comp (RayClass.primeToModulusIdeals m).subtype =
      χ.comp (arithmeticIdealArtinGaloisMap (K := K) (L := L) m hm) := by
…
  2. theorem OAI.DukePrimeDegree.idealCharacter_principalRay_eq_one line 57

    Source documentation

    No extra normalization hypothesis remains for a principal ray ideal.

    theorem idealCharacter_principalRay_eq_one
    (m : RayClass.Modulus K)
    (hm : m.congruenceSubgroup ≤ (ideleClassNorm K L).range)
    (hunram : ∀ v : IsDedekindDomain.HeightOneSpectrum (𝓞 K),
      v ∉ m.finitePart.support →
      Algebra.IsUnramifiedAt (𝓞 K) (primeAbove K L v).val)
    (χ : (L ≃ₐ[K] L) →* ℂˣ)
    (I : RayClass.primeToModulusIdeals m)
    (hI : I ∈ RayClass.principalRayIdealSubgroup m) :
    idealHom K L χ I = 1 := by
…