The Chebotarev density theorem

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremThe Chebotarev density theorem#

For a finite Galois extension L / K of number fields and a conjugacy class C of Gal(L/K), the primes of 𝓞 K whose Frobenius in L lies in C have Dirichlet density #C / #Gal(L/K).

NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet.{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]
  (C : ConjClasses Gal(L/K)) :
  NumberField.Set.HasDirichletDensity (NumberField.Chebotarev.frobeniusPrimeSet K L C)
    (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet.

Other forms

The Chebotarev density theorem, for Chebyshev's ψ. Formalized in Tau Ceti as NumberField.Chebotarev.frobeniusPsi_asymptotic.

NumberField.Chebotarev.frobeniusPsi_asymptotic.{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]
  (C : ConjClasses Gal(L/K)) :
  (fun x =>
      NumberField.Chebotarev.frobeniusPsi K L C x -
        ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)) * x) =o[Filter.atTop]
    fun x => x

The Chebotarev density theorem, for Chebyshev's ψ, as a limit. Formalized in Tau Ceti as NumberField.Chebotarev.tendsto_frobeniusPsi.

NumberField.Chebotarev.tendsto_frobeniusPsi.{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]
  (C : ConjClasses Gal(L/K)) :
  Filter.Tendsto (fun x => NumberField.Chebotarev.frobeniusPsi K L C x / x) Filter.atTop
    (nhds (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K))))

Sources

• Tau Ceti documentation: NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet
• Source of NumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet in TauCeti/NumberTheory/Chebotarev/Density/Chebotarev.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.hasDirichletDensity_frobeniusPrimeSet · NumberField.Chebotarev.frobeniusPsi_asymptotic · NumberField.Chebotarev.tendsto_frobeniusPsi

Uses 9 · Used by 2

Statement usesThe primes of K with Artin class C in L

Proof usesThe analytic Euler product · Artin's theorem · The continued L-function of a unitary weight, defined by partial summation · The crossing constant · The crossing constant approaches 1 / #Aut_K(L) · The fixed-field Frobenius fiber count · The ideal-theoretic Artin map · Weighted Chebotarev for abelian extensions

Used byNon-Galois Chebotarev for splitting types · NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet

TheoremNumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet#

Natural-density Chebotarev: among the primes of K, the primes with arithmetic Frobenius class C have density #C / #Gal(L/K).

NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet.{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]
  (C : ConjClasses Gal(L/K)) :
  NumberField.Set.HasNaturalDensity (NumberField.Chebotarev.frobeniusPrimeSet K L C)
    (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet
• Source of NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet in TauCeti/NumberTheory/Chebotarev/PrimeCounting/FrobeniusPrimeCount.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet

Uses 2

Statement usesThe primes of K with Artin class C in L

Proof usesThe Chebotarev density theorem

TheoremWeighted Chebotarev for abelian extensions#

If Gal(L/K) is abelian, then for every σ ∈ Gal(L/K) the Frobenius ψ function of σ satisfies ψ_σ(x) = x / #Gal(L/K) + o(x).

NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm.{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]
  (hab : ∀ (σ τ : Gal(L/K)), σ * τ = τ * σ) (σ : Gal(L/K)) :
  (fun x =>
      NumberField.Chebotarev.frobeniusPsi K L (ConjClasses.mk σ) x -
        1 / ↑(Nat.card Gal(L/K)) * x) =o[Filter.atTop]
    fun x => x

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm
• Source of NumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm in TauCeti/NumberTheory/Chebotarev/PrimeCounting/Chebotarev.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.frobeniusPsi_asymptotic_of_mul_comm

Uses 10 · Used by 1

Proof usesThe analytic Euler product · Artin's theorem · The continued L-function of a unitary weight, defined by partial summation · The crossing constant · The crossing constant approaches 1 / #Aut_K(L) · The Dedekind zeta function has no zeros on the line Re s = 1 away from its pole · The fixed-field Frobenius fiber count · The ideal-theoretic Artin map · The primes of K with Artin class C in L · The Wiener--Ikehara theorem

Used byThe Chebotarev density theorem

TheoremNon-Galois Chebotarev for splitting types#

The primes with residue-degree multiset μ in E have density the total proportion of elements whose action on Gal(L/K) ⧸ Gal(L/E) has full cycle type μ, expressed as a sum of conjugacy-class proportions. No normality of E/K or realizability hypothesis on μ is needed.

NumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq.{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]
  (E : IntermediateField K L) (μ : Multiset ℕ) :
  NumberField.Set.HasDirichletDensity
    {𝔭 | Multiset.map (fun P => (↑P).inertiaDeg (NumberField.RingOfIntegers K)) Finset.univ.val = μ}
    (∑ C with (MulAction.toPerm (Quotient.out C)).fullCycleType = μ,
      ↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq
• Source of NumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq in TauCeti/NumberTheory/Chebotarev/Density/SplittingType.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.hasDirichletDensity_setOf_map_inertiaDeg_eq

Uses 3

Proof usesThe analytic Euler product · The Chebotarev density theorem · The primes of K with Artin class C in L

TheoremDirichlet's theorem on primes in arithmetic progressions, with Dirichlet density#

For m ≠ 0 and a a unit modulo m, the primes of 𝓞 ℚ whose absolute norm is congruent to a modulo m have Dirichlet density 1 / φ(m).

NumberField.Chebotarev.hasDirichletDensity_primesCongruent (m a : ℕ) [NeZero m] (ha : IsUnit ↑a) :
  NumberField.Set.HasDirichletDensity {𝔭 | Ideal.absNorm 𝔭.asIdeal % m = a % m} (1 / ↑m.totient)

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.hasDirichletDensity_primesCongruent.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.hasDirichletDensity_primesCongruent
• Source of NumberField.Chebotarev.hasDirichletDensity_primesCongruent in TauCeti/NumberTheory/Chebotarev/Density/PrimesCongruent.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.hasDirichletDensity_primesCongruent

Uses 5

Proof usesA one-sided Abel bound · The analytic Euler product · Boundary data for the prime Dirichlet series of S · The prime ideal theorem · Prime-number-theorem transfer from exact boundary data

DefinitionThe primes of K with Artin class C in L#

A height-one prime 𝔭 of 𝓞 K belongs to frobeniusPrimeSet K L C when 𝔭 is unramified in L — so that artinSymbol is applicable — and its Artin class is C.

The unramifiedness proof is packaged existentially rather than assumed, because artinSymbol takes it as an argument and no value is assigned at a ramified prime. See mem_frobeniusPrimeSet_iff_artinSymbol_eq for the form used once such a proof is available.

The carrier and this membership condition are taken from TauCetiRoadmap/Chebotarev/Suggested.lean, lines 64–76, described in the section Frobenius prime sets and finite exceptional sets of TauCetiRoadmap/Chebotarev/README.md.

NumberField.Chebotarev.frobeniusPrimeSet.{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]
  (C : ConjClasses Gal(L/K)) :
  Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.frobeniusPrimeSet.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.frobeniusPrimeSet
• Source of NumberField.Chebotarev.frobeniusPrimeSet in TauCeti/NumberTheory/Chebotarev/FrobeniusPrimeSet.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.frobeniusPrimeSet

Used by 5

Used byNon-Galois Chebotarev for splitting types · NumberField.Chebotarev.hasNaturalDensity_frobeniusPrimeSet · The Chebotarev density theorem · The fixed-field Frobenius fiber count · Weighted Chebotarev for abelian extensions

TheoremThe fixed-field Frobenius fiber count#

Let sigma represent the conjugacy class C, and let p be an unramified prime with Artin class C. The number of primes of L ^ <sigma> above p whose relative Artin class in L / L ^ <sigma> is represented by sigma.toFixedFieldAlgEquiv is

#Gal(L/K) / (#C * orderOf sigma).

The division is exact by ConjClasses.card_carrier_mul_orderOf_dvd.

NumberField.Chebotarev.fixedField_frobenius_fiber_card.{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]
  (C : ConjClasses Gal(L/K)) (sigma : Gal(L/K)) (hsigma : sigma ∈ C.carrier)
  (p : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
  (hp : p ∈ NumberField.Chebotarev.frobeniusPrimeSet K L C) :
  Nat.card
      { P //
        IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) P = p ∧
          P ∈
            NumberField.Chebotarev.frobeniusPrimeSet
              (↥(IntermediateField.fixedField (Subgroup.zpowers sigma))) L
              (ConjClasses.mk sigma.toFixedFieldAlgEquiv) } =
    Nat.card Gal(L/K) / (Nat.card ↑C.carrier * orderOf sigma)

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.fixedField_frobenius_fiber_card.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.fixedField_frobenius_fiber_card
• Source of NumberField.Chebotarev.fixedField_frobenius_fiber_card in TauCeti/NumberTheory/Chebotarev/FixedField/FiberCount.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanNumberField.Chebotarev.fixedField_frobenius_fiber_card

Uses 2 · Used by 2

Statement usesArtin's theorem · The primes of K with Artin class C in L

Used byThe Chebotarev density theorem · Weighted Chebotarev for abelian extensions

DefinitionThe crossing constant#

The number of tagged elements of the auxiliary cyclic group H — those whose order is divisible by f — divided by #Aut_K(L) * #H.

That is the tag proportion within H, divided in addition by the order of Aut_K(L), which enters only through its order: the denominator that turns a count of tags into the density contributed by one auxiliary prime.

TauCeti.NumberField.Chebotarev.crossingConstant.{u_1, u_2, u_3} (K : Type u_1) (L : Type u_2)
  [CommSemiring K] [Semiring L] [Algebra K L] {H : Type u_3} [Group H] [Fintype H] (f : ℕ) : ℝ

Lean

Formalized in Tau Ceti as TauCeti.NumberField.Chebotarev.crossingConstant.

Sources

• Tau Ceti documentation: TauCeti.NumberField.Chebotarev.crossingConstant
• Source of TauCeti.NumberField.Chebotarev.crossingConstant in TauCeti/NumberTheory/Chebotarev/Crossing/CrossingConstant.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanTauCeti.NumberField.Chebotarev.crossingConstant

Used by 3

Used byThe Chebotarev density theorem · The crossing constant approaches 1 / #Aut_K(L) · Weighted Chebotarev for abelian extensions

TheoremThe crossing constant approaches 1 / #Aut_K(L)#

For every δ < 1 / #Aut_K(L) there is a level r such that the crossing constant of every cyclic group whose order is divisible by f ^ r exceeds δ.

The level depends only on δ, f and the order of Aut_K(L), not on the cyclic group, so a consumer that can choose an auxiliary group of any level pushes the crossing bound arbitrarily close to 1 / #Aut_K(L).

TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant.{u_1, u_2, u_4} (K : Type u_1)
  (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] (f : ℕ) {δ : ℝ}
  (hδ : δ < 1 / ↑(Nat.card (L ≃ₐ[K] L))) :
  ∃ r,
    ∀ (H : Type u_4) [inst : Group H] [inst_1 : Fintype H] [IsCyclic H],
      f ^ r ∣ Nat.card H → δ < TauCeti.NumberField.Chebotarev.crossingConstant K L f

Lean

Formalized in Tau Ceti as TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant.

Sources

• Tau Ceti documentation: TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant
• Source of TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant in TauCeti/NumberTheory/Chebotarev/Crossing/CrossingConstant.lean
• Tau Ceti roadmap status: The Chebotarev density theorem

LeanTauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant

Uses 2 · Used by 2

Statement usesThe crossing constant

Proof usesEuler's product formula for the elements of order divisible by f

Used byThe Chebotarev density theorem · Weighted Chebotarev for abelian extensions

TheoremThe prime number theorem for arithmetic progressions#

At every nonzero level m, the number of primes of 𝒪 ℚ whose norms are congruent to an invertible residue a modulo m is asymptotic to Li(x) / φ(m). This is the logarithmic-integral form of equidistribution among the invertible residue classes.

NumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral (m a : ℕ) [NeZero m]
  (ha : IsUnit ↑a) :
  Asymptotics.IsEquivalent Filter.atTop
    (fun x => TauCeti.primeCount ℚ {p | Ideal.absNorm p.asIdeal % m = a % m} x) fun x =>
    1 / ↑m.totient * TauCeti.Real.logIntegral x

Lean

Formalized in Tau Ceti as NumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral.

Sources

• Tau Ceti documentation: NumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral
• Source of NumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral in TauCeti/NumberTheory/Chebotarev/PrimeCounting/PrimesCongruent.lean

LeanNumberField.Chebotarev.primeCount_primesCongruent_isEquivalent_logIntegral

Uses 2

Proof usesBoundary data for the prime Dirichlet series of S · Prime-number-theorem transfer from exact boundary data

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.