6. Chebotarev density theorem🔗

The general Galois case is reduced to the abelian case via the cyclic subextension generated by a class representative. Source: Sharifi 7.2.2 Step 1 (p. 143).

Lemma6.1

Statement uses 2

Statement dependency previews

Preview

Definition 2.4

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let L/K be a finite Galois extension with G = \Gal{L/K}, C \subseteq G a conjugacy class, \sigma \in C, and \mathfrak{p} a nonzero prime of \mathcal{O}_K unramified in L with \sigma_\mathfrak{p} = C. The number of primes \mathfrak{P} of \mathcal{O}_L above \mathfrak{p} with \Frob_\mathfrak{P} = \sigma is exactly |G|/(f \cdot |C|), where f = \operatorname{ord}(\sigma).

Definition 2.4 Definition 2.5

Lean code for Lemma6.1●1 theorem

theoremdefined in CebotarevDensity/FixedFieldDensity.lean

complete

theorem Chebotarev.count_primes_above_with_frobenius_eq_sigma.{u_3, u_4}
  (K : Type u_3) (L : Type u_4) [Field K] [NumberField K] [Field L]
  [NumberField L] [Algebra K L] [IsGalois K L] (σ : Gal(L/K))
  (C : ConjClasses Gal(L/K)) (_hσ : ConjClasses.mk σ = C)
  (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime]
  (hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_hCfrob : Chebotarev.frobeniusClass K L 𝔭 = C) :
  Nat.card
          { 𝔓 //
            ∃ (_ : 𝔓.IsPrime) (_ : 𝔓.LiesOver 𝔭) (_ : 𝔓 ≠ ⊥),
              IsArithFrobAt (NumberField.RingOfIntegers K) σ 𝔓 } *
        orderOf σ *
      Nat.card ↑C.carrier =
    Nat.card Gal(L/K)

theorem Chebotarev.count_primes_above_with_frobenius_eq_sigma.{u_3,
    u_4}
  (K : Type u_3) (L : Type u_4) [Field K]
  [NumberField K] [Field L]
  [NumberField L] [Algebra K L]
  [IsGalois K L] (σ : Gal(L/K))
  (C : ConjClasses Gal(L/K))
  (_hσ : ConjClasses.mk σ = C)
  (𝔭 :
    Ideal (NumberField.RingOfIntegers K))
  [𝔭.IsPrime]
  (hunr : Chebotarev.UnramifiedIn K L 𝔭)
  (_hCfrob :
    Chebotarev.frobeniusClass K L 𝔭 = C) :
  Nat.card
          { 𝔓 //
            ∃ (_ : 𝔓.IsPrime) (_ :
              𝔓.LiesOver 𝔭) (_ : 𝔓 ≠ ⊥),
              IsArithFrobAt
                (NumberField.RingOfIntegers
                  K)
                σ 𝔓 } *
        orderOf σ *
      Nat.card ↑C.carrier =
    Nat.card Gal(L/K)

Sharifi 7.2.2 Step 1, above-counting (p. 143). Verbatim source quote:
"exactly `|G|/f|C|` of these have Frobenius σ". For a prime `𝔭` of
`𝓞 K` with Frobenius class `C` and a representative `σ ∈ C`, the count
of primes `𝔓` of `𝓞 L` above `𝔭` with `Frob_𝔓 = σ` is `|G|/(f·|C|)`.

This is the substantive new sub-lemma for the conjugacy-class →
cyclic reduction; the fixed-field cyclic-subextension setup
(`E = L^⟨σ⟩`, `[L:E] = ord σ`) is mathlib's `IntermediateField.fixedField`
and `IsGalois.card_aut_eq_finrank` applied at `⟨σ⟩`, and the density-lift
formula `δ_K(S) = (f|C|/|G|) δ_E(T_σ)` follows from this counting
together with `Σ N𝔭^{-s} ~ Σ NP^{-s}` (Sharifi 7.1.12 applied to both
`K` and `E`).

Proof for Lemma 6.1

uses 0

The Galois group G acts transitively on primes above \mathfrak{p}, with stabiliser D_\mathfrak{P}. Hence the orbit has size |G|/|D_\mathfrak{P}|. For unramified \mathfrak{p}, D_\mathfrak{P} = \langle \Frob_\mathfrak{P} \rangle has order f, so there are |G|/f primes above \mathfrak{p}. Their Frobenius elements form a G-orbit in C (under conjugation), which is all of C by transitivity; this orbit has size |C|, and within each orbit the count of representatives \sigma is |G|/(f \cdot |C|) (Sharifi p. 143).

Lemma6.2

Statement uses 4

Statement dependency previews

Preview

Definition 1.1

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 1✓L∃∀N

Let \sigma \in \Gal{L/K}, E = L^{\langle \sigma \rangle}, and \sigma_E \in \Gal{L/E} the corresponding element. Given the abelian-case density over E for the Frobenius-fibre of \sigma_E (value 1/|\Gal{L/E}|), the K-density of the Frobenius class [\sigma] is |[\sigma]|/|G|.

Definition 1.1 Definition 2.5 Lemma 6.1 Lemma 1.8

Lean code for Lemma6.2●1 theorem

theoremdefined in CebotarevDensity/FixedFieldDensity.lean

complete

theorem Chebotarev.density_lift_through_fixedField.{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] (σ : Gal(L/K))
  (E : IntermediateField K L) (σE : Gal(L/↥E))
  (hσE : AlgEquiv.restrictScalars K σE = σ)
  (_hEfix : E = IntermediateField.fixedField (Subgroup.zpowers σ))
  (_hab :
    Chebotarev.HasDirichletDensity
      {P |
        P.IsPrime ∧
          Chebotarev.UnramifiedIn (↥E) L P ∧
            Chebotarev.frobeniusClass (↥E) L P = ConjClasses.mk σE}
      (↑(Nat.card Gal(L/↥E)))⁻¹) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
    (↑(Nat.card ↑(ConjClasses.mk σ).carrier) / ↑(Nat.card Gal(L/K)))

theorem Chebotarev.density_lift_through_fixedField.{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] (σ : Gal(L/K))
  (E : IntermediateField K L)
  (σE : Gal(L/↥E))
  (hσE :
    AlgEquiv.restrictScalars K σE = σ)
  (_hEfix :
    E =
      IntermediateField.fixedField
        (Subgroup.zpowers σ))
  (_hab :
    Chebotarev.HasDirichletDensity
      {P |
        P.IsPrime ∧
          Chebotarev.UnramifiedIn (↥E) L
              P ∧
            Chebotarev.frobeniusClass (↥E)
                L P =
              ConjClasses.mk σE}
      (↑(Nat.card Gal(L/↥E)))⁻¹) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            ConjClasses.mk σ}
    (↑(Nat.card
          ↑(ConjClasses.mk σ).carrier) /
      ↑(Nat.card Gal(L/K)))

**Density-lift through the fixed-field subextension** (Sharifi 7.2.2
Step 1, p. 143). Let `σ ∈ Gal(L/K)`, `E = L^⟨σ⟩` the fixed field of the
cyclic subgroup `⟨σ⟩`, and `σ_E ∈ Gal(L/E)` the corresponding element.
Given the abelian-case density over `E` for the Frobenius-fibre of `σ_E`
(value `1/|Gal(L/E)|`), the density over `K` of the Frobenius **class** of
`σ` is `|C|/|G|`.

Source quote (verbatim, p. 143): "δ(S) = … = (f|C|/|G|) δ(T_σ),
recalling once again that `Σ_𝔭 N𝔭^{-s} ~ Σ_P NP^{-s}`. Supposing the
theorem for K/E, we have δ(T_σ) = 1/f, and we therefore obtain δ(S) =
|C|/|G|." Here `f = ord σ = |Gal(L/E)|`, and the counting factor is
`count_primes_above_with_frobenius_eq_sigma`.

The hypothesis `hEfix` records that `E` is the fixed field of `⟨σ⟩`; the
hypothesis `hσE` records that `σ_E` restricts to `σ` over `K` (so `σ_E`
generates `Gal(L/E)` and a prime with `Frob^E_𝔓 = σ_E` has `Frob^K_𝔓 = σ`);
the hypothesis `hab` is the abelian-case output for `L/E` from
`chebotarev_abelian`.

Proof for Lemma 6.2

Proof uses 2

Proof dependency previews

Preview

Lemma 1.8

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

For primes P of E above \mathfrak{p} \in S = \{\mathfrak{p} : \sigma_\mathfrak{p} = [\sigma]\}, exactly |G|/(f|C|) of the primes of L above have Frobenius \sigma (Lemma 6.1); with \sum_\mathfrak{p} \Norm\mathfrak{p}^{-s} \sim \sum_P \Norm{P}^{-s} (Lemma 1.8 over both K and E), \delta_K(S) = (f|C|/|G|)\,\delta_E(T_\sigma) = (f|C|/|G|)(1/f) = |C|/|G|.

Lemma 6.1 Lemma 1.8

Theorem6.3

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

Used by 3

Reverse dependency previews

Preview

Corollary 6.1.5

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Chebotarev density theorem. For a finite Galois extension L/K of number fields with G = \Gal{L/K} and any conjugacy class C \subseteq G, \delta\bigl(\{\mathfrak{p} \subset \mathcal{O}_K : \sigma_\mathfrak{p} = C\}\bigr) \;=\; \frac{|C|}{|G|}.

Theorem 5.8 Lemma 6.2

Lean code for Theorem6.3●1 theorem

theoremdefined in CebotarevDensity/Main.lean

complete

theorem Chebotarev.chebotarev_density.{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] [FiniteDimensional K L] (C : ConjClasses Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = C}
    (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

theorem Chebotarev.chebotarev_density.{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] [FiniteDimensional K L]
  (C : ConjClasses Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            C}
    (↑(Nat.card ↑C.carrier) /
      ↑(Nat.card Gal(L/K)))

**Chebotarev's density theorem** (Sharifi 7.2.2; SL Appendix).

For a finite Galois extension `L/K` of number fields with Galois group `G`
and a conjugacy class `C ⊆ G`, the Dirichlet density of the set of primes
`𝔭` of `𝓞 K` (unramified in `L`) such that the Frobenius conjugacy class of
`𝔭` is `C` equals `|C| / |G|`.

Proof for Theorem 6.3

Proof uses 2

Proof dependency previews

Preview

Theorem 5.8

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Pick a representative \sigma \in C (ConjClasses.mk_surjective) and let E = L^{\langle \sigma \rangle} be the fixed field of \langle \sigma \rangle. The isomorphism \langle \sigma \rangle \xrightarrow{\sim} \Gal{L/E} (IntermediateField.subgroupEquivAlgEquiv) shows \Gal{L/E} is commutative (as \langle \sigma \rangle is cyclic), so L/E is abelian and Theorem 5.8 applies to its Frobenius \sigma_E, giving \delta_E(T_\sigma) = 1/|\Gal{L/E}|. Feeding this into the density lift Lemma 6.2 yields |C|/|G|.

Theorem 5.8 Lemma 6.2

Theorem6.4

Statement uses 2

Statement dependency previews

Preview

Theorem 5.8

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 0✓L∃∀N

Chebotarev, abelian case. When G = \Gal{L/K} is abelian, the Chebotarev density theorem holds: for every conjugacy class C, \delta(\{\mathfrak{p} : \sigma_\mathfrak{p} = C\}) = |C|/|G|.

Theorem 5.8 Lemma 6.1.2

Lean code for Theorem6.4●1 theorem

theoremdefined in CebotarevDensity/Main.lean

complete

theorem Chebotarev.chebotarev_density_of_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] [FiniteDimensional K L]
  [IsMulCommutative Gal(L/K)] (C : ConjClasses Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = C}
    (↑(Nat.card ↑C.carrier) / ↑(Nat.card Gal(L/K)))

theorem Chebotarev.chebotarev_density_of_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] [FiniteDimensional K L]
  [IsMulCommutative Gal(L/K)]
  (C : ConjClasses Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            C}
    (↑(Nat.card ↑C.carrier) /
      ↑(Nat.card Gal(L/K)))

**Chebotarev's density theorem, abelian case.** For an abelian Galois
extension `L/K`, the Dirichlet density of primes `𝔭` of `𝓞 K` unramified in
`L` whose Frobenius conjugacy class is `C` is `|C| / |Gal(L/K)|`.

Proof for Theorem 6.4

Proof uses 2

Proof dependency previews

Preview

Theorem 5.8

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

In an abelian group each class C = [\sigma] is a singleton (Lemma 6.1.2), so |C| = 1 and the target density is 1/|G|; this is exactly Theorem 5.8 for the representative \sigma.

Theorem 5.8 Lemma 6.1.2

6.1. Corollaries