5. Chebotarev: abelian case🔗

The abelian case is reduced to the cyclotomic case by Chebotarev's original crossing trick. Source: Sharifi 7.2.2 Step 2 (pp. 143--144).

Lemma5.1

uses 0used by 1✓L∃∀N

Let G, H be finite groups, \sigma \in G, \tau \in H. If |G| \mid \operatorname{ord}(\tau), then \langle (\sigma, \tau) \rangle \cap (G \times \{1\}) = \{1\}.

Lean code for Lemma5.1●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.cyclic_subgroup_meets_G_times_one_trivially.{u_3, u_4}
  (G : Type u_3) (H : Type u_4) [Group G] [Group H] [Finite G]
  [Finite H] (σ : G) (τ : H) (_hn : Nat.card G ∣ orderOf τ) :
  Subgroup.zpowers (σ, τ) ⊓ ⊤.prod ⊥ = ⊥

theorem Chebotarev.cyclic_subgroup_meets_G_times_one_trivially.{u_3,
    u_4}
  (G : Type u_3) (H : Type u_4) [Group G]
  [Group H] [Finite G] [Finite H] (σ : G)
  (τ : H) (_hn : Nat.card G ∣ orderOf τ) :
  Subgroup.zpowers (σ, τ) ⊓ ⊤.prod ⊥ = ⊥

Sharifi 7.2.2 Step 2 sub-lemma (i) — cyclic subgroup trivial meet
(p. 144). Source quote: "if `|G|` divides the order of `τ`, then
`⟨(σ,τ)⟩ ∩ (G × {1}) = 1`". This is the only place where the
`|G| | ord(τ)` hypothesis is used in Step 2.

Proof for Lemma 5.1

uses 0

Pure group theory. If (\sigma^k, \tau^k) \in G \times \{1\} then \tau^k = 1, so \operatorname{ord}(\tau) \mid k, hence |G| \mid k, hence \sigma^k = 1.

Lemma5.2

Statement uses 2

Statement dependency previews

Preview

Theorem 4.8

Loading preview

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

used by 1✓L∃∀N

Let L/K be a finite abelian Galois extension with G = \Gal{L/K}, \sigma \in G, and m \ge 1 coprime to the discriminant of L, so that \Gal{L(\zeta_m)/K} \cong G \times H with H = \Gal{K(\zeta_m)/K} \subseteq (\mathbb{Z}/m\mathbb{Z})^\times. Set H_n = \{\tau \in H : |G| \mid \operatorname{ord}(\tau)\}. Then \delta_{\inf}\bigl(\{\mathfrak{p} \subset \mathcal{O}_K : \sigma_\mathfrak{p} = \sigma\}\bigr) \;\ge\; \frac{|H_n|}{|G| \cdot |H|}.

Corrected. An earlier draft of this lemma claimed \delta\bigl(\{\mathfrak{p} : \sigma_\mathfrak{p} = \sigma\}\bigr) = 1/(|G| \cdot |H|) — that is mathematically wrong (the set \{\sigma_\mathfrak{p} = \sigma\} has density 1/|G|, not 1/(|G| \cdot |H|)). The actual per-m step that feeds into the proof of \delta(\sigma_\mathfrak{p} = \sigma) = 1/|G| is the \liminf lower bound above (Sharifi p. 144).

Lemma 5.1 Theorem 4.8

Lean code for Lemma5.2●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH.{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]
  [hAb : IsMulCommutative Gal(L/K)] (σ : Gal(L/K)) (m : ℕ) (_hm : 1 ≤ m)
  (hm4 : m % 4 ≠ 2) (hcop : (NumberField.discr L).natAbs.Coprime m) :
  ↑(Nat.card { τ // Nat.card Gal(L/K) ∣ orderOf τ }) /
      (↑(Nat.card Gal(L/K)) * ↑(Nat.card (ZMod m)ˣ)) ≤
    Filter.liminf
      (fun s ↦
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K L 𝔭 ∧
                  Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum Set.univ s)
      (nhdsWithin 1 (Set.Ioi 1))

theorem Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH.{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]
  [hAb : IsMulCommutative Gal(L/K)]
  (σ : Gal(L/K)) (m : ℕ) (_hm : 1 ≤ m)
  (hm4 : m % 4 ≠ 2)
  (hcop :
    (NumberField.discr L).natAbs.Coprime
      m) :
  ↑(Nat.card
          { τ //
            Nat.card Gal(L/K) ∣
              orderOf τ }) /
      (↑(Nat.card Gal(L/K)) *
        ↑(Nat.card (ZMod m)ˣ)) ≤
    Filter.liminf
      (fun s ↦
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K
                    L 𝔭 ∧
                  Chebotarev.frobeniusClass
                      K L 𝔭 =
                    ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum
            Set.univ s)
      (nhdsWithin 1 (Set.Ioi 1))

Sharifi 7.2.2 Step 2 — partial **lower bound** on `δ_inf(S_σ)` coming from one
cyclotomic crossing modulus `m`: `|H_n(m)|/(|G|·|H(m)|)` bounds the `liminf` of the
density ratio for `S_σ` in `K`. Source quote (p. 144): "δ_inf(S_σ) ≥ |H_n|/(|G|·|H|)".

The crossing is only valid at *admissible* `m`, so this per-`m` bound carries the same
two hypotheses as `exists_cyclotomicCrossing_fibres`: `hm4 : m % 4 ≠ 2` (feeding the
cyclotomic case) and `hcop : ((NumberField.discr L).natAbs).Coprime m` (the
linear-disjointness via the everywhere-unramified intersection / `discr_dvd_discr`). The
consumer `liminf_ratio_ge_inv_card_G` drives `m` along admissible primes.

Proof for Lemma 5.2

uses 0

By Lemma 5.1, the fixed field F = L(\zeta_m)^{\langle (\sigma, \tau) \rangle} satisfies F(\zeta_m) = L(\zeta_m), so the extension L(\zeta_m)/F is cyclotomic. Apply the cyclotomic case Theorem 4.8 to L(\zeta_m)/F to obtain \delta_F = 1/|\langle (\sigma, \tau) \rangle|. The conjugacy-class reduction (Theorem 6.3 below, Step 1's counting) lifts this to a K-density of 1/(|G| \cdot |H|).

Lemma5.3

uses 0used by 1XL∃∀N

Let n = p_1^{k_1} \cdots p_r^{k_r} with p_i distinct primes, k_i \ge 1. For an integer m \ge 1 with m \equiv 1 \pmod{n^j}, setting j_i = v_{p_i}(m-1) \ge j and H_n = \{\tau \in (\mathbb{Z}/m\mathbb{Z})^\times : n \mid \operatorname{ord}(\tau)\}, \frac{|H_n|}{|(\mathbb{Z}/m\mathbb{Z})^\times|} \;=\; \prod_{i=1}^r \biggl(1 - \frac{p_i^{k_i - 1}}{p_i^{j_i k_i}}\biggr) \;\ge\; \prod_{i=1}^r \biggl(1 - \frac{1}{p_i^{(j-1)k_i + 1}}\biggr).

Proof for Lemma 5.3

uses 0

Direct combinatorial computation on (\mathbb{Z}/m\mathbb{Z})^\times using CRT and the prime-power factorisation of n (Sharifi p. 144).

Lemma5.4

uses 1used by 1✓L∃∀N

As k \to \infty, |H_n|/|(\mathbb{Z}/n^k\mathbb{Z})^\times| \to 1.

Lemma 5.3

Lean code for Lemma5.4●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.H_n_over_H_tends_to_one (n : ℕ) (_hn : 1 ≤ n) :
  Filter.Tendsto
    (fun k ↦
      ↑(Nat.card { τ // n ∣ orderOf τ }) / ↑(Nat.card (ZMod (n ^ k))ˣ))
    Filter.atTop (nhds 1)

theorem Chebotarev.H_n_over_H_tends_to_one (n : ℕ)
  (_hn : 1 ≤ n) :
  Filter.Tendsto
    (fun k ↦
      ↑(Nat.card { τ // n ∣ orderOf τ }) /
        ↑(Nat.card (ZMod (n ^ k))ˣ))
    Filter.atTop (nhds 1)

Sharifi 7.2.2 Step 2 sub-lemma (v) — `|H_n|/|H| → 1` as `m ≡ 1 mod
n^k` for `k → ∞`. Verbatim source quote: "so `|H_n|/|H|` tends to 1 as
`j` increases".

Proof for Lemma 5.4

uses 0

The limit of the product formula Lemma 5.3 as j \to \infty: each factor tends to 1.

Lemma5.5

Statement uses 2

Statement dependency previews

Preview

Lemma 5.2

Loading preview

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

used by 1✓L∃∀N

For every \sigma \in G, \delta_{\inf}\bigl(\{\mathfrak{p} : \sigma_\mathfrak{p} = \sigma\}\bigr) \ge 1/|G|.

Lemma 5.2 Lemma 5.4

Lean code for Lemma5.5●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.liminf_ratio_ge_inv_card_G.{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] [hAb : IsMulCommutative Gal(L/K)]
  (σ : Gal(L/K)) :
  (↑(Nat.card Gal(L/K)))⁻¹ ≤
    Filter.liminf
      (fun s ↦
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K L 𝔭 ∧
                  Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum Set.univ s)
      (nhdsWithin 1 (Set.Ioi 1))

theorem Chebotarev.liminf_ratio_ge_inv_card_G.{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]
  [hAb : IsMulCommutative Gal(L/K)]
  (σ : Gal(L/K)) :
  (↑(Nat.card Gal(L/K)))⁻¹ ≤
    Filter.liminf
      (fun s ↦
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K
                    L 𝔭 ∧
                  Chebotarev.frobeniusClass
                      K L 𝔭 =
                    ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum
            Set.univ s)
      (nhdsWithin 1 (Set.Ioi 1))

Per-`σ` lower bound `δ_inf(S_σ) ≥ 1/|G|`, the limit of the per-`m` bound
`liminf_density_S_sigma_ge_card_H_n_div_GH` as `m → ∞` along a sequence of
*admissible primes* `m_k ≡ 1 (mod 4·n^k)` with `m_k > |disc L|` (Dirichlet's theorem on
primes in arithmetic progression). The lower half of Sharifi 7.2.2 Step 2 (p. 144).

Proof for Lemma 5.5

Proof uses 2

Proof dependency previews

Preview

Lemma 5.2

Loading preview

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

Take the limit of the per-m bound Lemma 5.2 as m \to \infty along m \equiv 1 \pmod{|G|^k}, where |H_n|/|H| \to 1 by Lemma 5.4.

Lemma 5.2 Lemma 5.4

Lemma5.6

Statement uses 2

Statement dependency previews

Preview

Definition 2.5

Loading preview

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

used by 1✓L∃∀N

As s \downarrow 1, the sum over \sigma \in G of the density ratios of the fibres \{\mathfrak{p} : \sigma_\mathfrak{p} = \sigma\} tends to 1.

Definition 2.5 Lemma 2.8

Lean code for Lemma5.6●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.ratioSum_frobeniusFibres_tendsto_one.{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]
  [hAb : IsMulCommutative Gal(L/K)] :
  Filter.Tendsto
    (fun s ↦
      ∑ σ,
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K L 𝔭 ∧
                  Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum Set.univ s)
    (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)

theorem Chebotarev.ratioSum_frobeniusFibres_tendsto_one.{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]
  [hAb : IsMulCommutative Gal(L/K)] :
  Filter.Tendsto
    (fun s ↦
      ∑ σ,
        Chebotarev.primeIdealZetaSum
            {𝔭 |
              𝔭.IsPrime ∧
                Chebotarev.UnramifiedIn K
                    L 𝔭 ∧
                  Chebotarev.frobeniusClass
                      K L 𝔭 =
                    ConjClasses.mk σ}
            s /
          Chebotarev.primeIdealZetaSum
            Set.univ s)
    (nhdsWithin 1 (Set.Ioi 1)) (nhds 1)

The density ratios of the `|G|` Frobenius-fibres `S_σ` (over
`σ ∈ Gal(L/K)`) sum to the ratio for the unramified primes, which tends
to `1` as `s ↓ 1` since the ramified primes are finite
(`finite_ramifiedIn`, density `0`). Sharifi 7.2.2 Step 2: the `S_σ`
partition the unramified primes.

Proof for Lemma 5.6

uses 1

The fibres partition the unramified primes; the ramified primes are finite (Lemma 2.8) hence contribute density 0, so the partial sums of the fibre ratios equal the ratio for the unramified primes, which tends to 1.

Lemma 2.8

Lemma5.7

uses 0used by 1✓L∃∀N

Let g_i (i in a finite index set of size N) be real functions with \liminf_{s \downarrow 1} g_i \ge 1/N for each i, and \sum_i g_i(s) \to 1 as s \downarrow 1. Then g_i(s) \to 1/N for every i.

Lean code for Lemma5.7●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one.{u_3}
  {ι : Type u_3} [Fintype ι] (g : ι → ℝ → ℝ)
  (hlo :
    ∀ (i : ι),
      (↑(Fintype.card ι))⁻¹ ≤
        Filter.liminf (g i) (nhdsWithin 1 (Set.Ioi 1)))
  (hbelow :
    ∀ (i : ι),
      Filter.IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2)
        (nhdsWithin 1 (Set.Ioi 1)) (g i))
  (hsum :
    Filter.Tendsto (fun s ↦ ∑ i, g i s) (nhdsWithin 1 (Set.Ioi 1))
      (nhds 1))
  (i₀ : ι) :
  Filter.Tendsto (g i₀) (nhdsWithin 1 (Set.Ioi 1))
    (nhds (↑(Fintype.card ι))⁻¹)

theorem Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one.{u_3}
  {ι : Type u_3} [Fintype ι]
  (g : ι → ℝ → ℝ)
  (hlo :
    ∀ (i : ι),
      (↑(Fintype.card ι))⁻¹ ≤
        Filter.liminf (g i)
          (nhdsWithin 1 (Set.Ioi 1)))
  (hbelow :
    ∀ (i : ι),
      Filter.IsBoundedUnder
        (fun x1 x2 ↦ x1 ≥ x2)
        (nhdsWithin 1 (Set.Ioi 1)) (g i))
  (hsum :
    Filter.Tendsto (fun s ↦ ∑ i, g i s)
      (nhdsWithin 1 (Set.Ioi 1)) (nhds 1))
  (i₀ : ι) :
  Filter.Tendsto (g i₀)
    (nhdsWithin 1 (Set.Ioi 1))
    (nhds (↑(Fintype.card ι))⁻¹)

Pure real-analysis glue: a finite family `gᵢ` of functions, each with
`liminf gᵢ ≥ 1/N` (where `N` is the family size) and bounded below, whose sum
tends to `1`, must each tend to `1/N`. (The lower bounds and the sum-limit pin
every `gᵢ` to `1/N` by a pigeonhole on `liminf`/`limsup`.)

The below-boundedness hypothesis `hbelow` is genuinely needed: a finite `liminf`
lower bound alone does not force below-boundedness in a conditionally complete
order, so without it the statement is false (one `gᵢ` could dip to `-∞` while
keeping a spurious `liminf` and the sum still converging). At the only call site
(`chebotarev_abelian`) each `gᵢ` is a ratio of nonnegative Dirichlet sums, hence
`0 ≤ gᵢ`, so `hbelow` is immediate.

Proof for Lemma 5.7

uses 0

Pure real analysis: the lower bounds and the sum-limit pin every g_i to 1/N by a \liminf/\limsup pigeonhole.

Theorem5.8

Statement uses 5

Statement dependency previews

Preview

Definition 1.1

Loading preview

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

Used by 2

Reverse dependency previews

Preview

Theorem 6.3

Loading preview

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

✓L∃∀N

For a finite abelian Galois extension L/K of number fields with G = \Gal{L/K} and every \sigma \in G, \delta\bigl(\{\mathfrak{p} \subset \mathcal{O}_K : \sigma_\mathfrak{p} = \sigma\}\bigr) \;=\; \frac{1}{|G|}.

Definition 1.1 Definition 2.5 Lemma 5.5 Lemma 5.6 Lemma 5.7

Lean code for Theorem5.8●1 theorem

theoremdefined in CebotarevDensity/Abelian.lean

complete

theorem Chebotarev.chebotarev_abelian.{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 : IsMulCommutative Gal(L/K)] (σ : Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ}
    (↑(Nat.card Gal(L/K)))⁻¹

theorem Chebotarev.chebotarev_abelian.{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 : IsMulCommutative Gal(L/K)]
  (σ : Gal(L/K)) :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            ConjClasses.mk σ}
    (↑(Nat.card Gal(L/K)))⁻¹

**Chebotarev's theorem, abelian case** (Sharifi 7.2.2 Step 2).

For an abelian Galois extension `L/K` of number fields and any
`σ ∈ Gal(L/K)`, the Dirichlet density of primes `𝔭` of `𝓞 K` unramified in
`L` whose Frobenius equals `σ` is `1 / |Gal(L/K)|`.

**Composition**: the `|G|` fibres `S_σ` each have `liminf ≥ 1/|G|`
(`liminf_ratio_ge_inv_card_G`) and their density ratios sum to `1`
(`ratioSum_frobeniusFibres_tendsto_one`); the pigeonhole glue
`tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one` forces each to the
limit `1/|G|`.

Proof for Theorem 5.8

Proof uses 3

Proof dependency previews

Preview

Lemma 5.5

Loading preview

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

The |G| fibres each have \liminf \ge 1/|G| (Lemma 5.5) and their density ratios sum to 1 (Lemma 5.6); the pigeonhole glue Lemma 5.7 forces each fibre's ratio to the limit 1/|G|.

Lemma 5.5 Lemma 5.6 Lemma 5.7