The Chebotarev Density Theorem in Lean

6.1. Corollaries🔗

The corollaries below are derived directly by composition from Theorem 6.3. The Lean derivations use four small helper sub-lemmas captured here.

Lemma6.1.1
uses 0used by 1✓L∃∀N

Let G be a finite group. The conjugacy class of the identity has cardinality 1: |(\operatorname{Conj}(G))_{\{1\}}| = 1.

Lean code for Lemma6.1.1●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.ConjClasses_mk_one_carrier_card_eq_one.{u_3} (G : Type u_3)
  [Monoid G] [Finite G] : Nat.card ↑(ConjClasses.mk 1).carrier = 1
    theorem Chebotarev.ConjClasses_mk_one_carrier_card_eq_one.{u_3}
  (G : Type u_3) [Monoid G] [Finite G] :
  Nat.card ↑(ConjClasses.mk 1).carrier = 1
    The identity conjugacy class in a finite monoid has carrier of cardinality `1`.
Proof for Lemma 6.1.1
uses 0

The carrier is \{1\} (by isConj_one_left, a is conjugate to 1 iff a = 1); a singleton has cardinality 1.

Lemma6.1.2
uses 0used by 1✓L∃∀N

In a commutative finite group, every conjugacy class is a singleton, so has cardinality 1.

Lean code for Lemma6.1.2●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.ConjClasses_carrier_card_eq_one_of_comm.{u_3} {G : Type u_3}
  [Monoid G] [IsMulCommutative G] [Finite G] (g : G) :
  Nat.card ↑(ConjClasses.mk g).carrier = 1
    theorem Chebotarev.ConjClasses_carrier_card_eq_one_of_comm.{u_3}
  {G : Type u_3} [Monoid G]
  [IsMulCommutative G] [Finite G]
  (g : G) :
  Nat.card ↑(ConjClasses.mk g).carrier = 1
    In a commutative finite monoid every conjugacy class is a singleton,
so `|C| = 1`.
Proof for Lemma 6.1.2
uses 0

By isConj_iff_eq (conjugacy is equality in a commutative monoid), the carrier of [g] is \{g\}.

Lemma6.1.3
uses 0used by 1✓L∃∀N

A set S of prime ideals with positive Dirichlet density is infinite.

Lean code for Lemma6.1.3●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.infinite_of_hasDirichletDensity_pos.{u_1} {K : Type u_1}
  [Field K] [NumberField K]
  {S : Set (Ideal (NumberField.RingOfIntegers K))} {δ : ℝ}
  (h : Chebotarev.HasDirichletDensity S δ) (hδ : 0 < δ) : S.Infinite
    theorem Chebotarev.infinite_of_hasDirichletDensity_pos.{u_1}
  {K : Type u_1} [Field K] [NumberField K]
  {S :
    Set
      (Ideal
        (NumberField.RingOfIntegers K))}
  {δ : ℝ}
  (h : Chebotarev.HasDirichletDensity S δ)
  (hδ : 0 < δ) : S.Infinite
    A set of prime ideals with positive Dirichlet density is infinite.
Proof for Lemma 6.1.3
uses 0

Contrapositive: a finite set of primes has density 0 by Lemma 1.1.1 (the finite case of Definition 1.1).

Lemma6.1.4
uses 0used by 1✓L∃∀N

Every conjugacy class in a finite group has cardinality at least 1 (it contains at least its own representative).

Lean code for Lemma6.1.4●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.ConjClasses_carrier_card_pos.{u_3} {G : Type u_3} [Monoid G]
  [Finite G] (C : ConjClasses G) : 0 < Nat.card ↑C.carrier
    theorem Chebotarev.ConjClasses_carrier_card_pos.{u_3}
  {G : Type u_3} [Monoid G] [Finite G]
  (C : ConjClasses G) :
  0 < Nat.card ↑C.carrier
    The carrier of a conjugacy class in a finite monoid has positive cardinality.
Proof for Lemma 6.1.4
uses 0

A representative a with [a] = C lies in the carrier (ConjClasses.mk_surjective together with mem_carrier_iff_mk_eq), so the carrier is nonempty; a nonempty finite set has positive cardinality.

Corollary6.1.5
Statement uses 2
Statement dependency previews
Preview
Theorem 6.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N

For a finite Galois extension L/K of number fields, the Dirichlet density of primes of \mathcal{O}_K that split completely in L equals 1/[L:K].

Theorem 6.3 Lemma 6.1.1

Lean code for Corollary6.1.5●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.density_split_completely.{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] :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk 1}
    (↑(Module.finrank K L))⁻¹
    theorem Chebotarev.density_split_completely.{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] :
  Chebotarev.HasDirichletDensity
    {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            ConjClasses.mk 1}
    (↑(Module.finrank K L))⁻¹
    **Density of completely split primes** (Sharifi 7.1.14, as a corollary of
Chebotarev applied to the identity conjugacy class).

The Dirichlet density of primes `𝔭` of `𝓞 K` that split completely in `L`
equals `1 / [L : K]`.
Proof for Corollary 6.1.5
Proof uses 2
Proof dependency previews
Preview
Theorem 6.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

A prime \mathfrak{p} splits completely in L iff every \mathfrak{P} \mid \mathfrak{p} has \Frob_\mathfrak{P} = 1, i.e. the Frobenius conjugacy class is the trivial class. Apply Theorem 6.3 at C = \operatorname{Conj}(G)_{\{1\}}; by Lemma 6.1.1 the numerator |C| = 1 and by mathlib's IsGalois.card_aut_eq_finrank the denominator |\Gal{L/K}| = [L:K], so the density equals 1/[L:K].

Theorem 6.3 Lemma 6.1.1

Corollary6.1.6
Statement uses 3
Statement dependency previews
Preview
Theorem 6.3
Loading preview
Statement dependency preview content is loaded from the Blueprint HTML cache.
used by 0✓L∃∀N

For a finite Galois extension L/K of number fields and any conjugacy class C \subseteq \Gal{L/K}, the set of primes \mathfrak{p} of \mathcal{O}_K unramified in L with Frobenius conjugacy class C is infinite.

Theorem 6.3 Lemma 6.1.3 Lemma 6.1.4

Lean code for Corollary6.1.6●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.infinite_setOf_frobenius_class.{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)) :
  {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L 𝔭 = C}.Infinite
    theorem Chebotarev.infinite_setOf_frobenius_class.{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)) :
  {𝔭 |
      𝔭.IsPrime ∧
        Chebotarev.UnramifiedIn K L 𝔭 ∧
          Chebotarev.frobeniusClass K L
              𝔭 =
            C}.Infinite
    Existence of *infinitely many* primes with each Frobenius conjugacy class
— a qualitative corollary of `chebotarev_density`.
Proof for Corollary 6.1.6
Proof uses 3
Proof dependency previews
Preview
Theorem 6.3
Loading preview
Proof dependency preview content is loaded from the Blueprint HTML cache.

Theorem 6.3 gives Dirichlet density |C|/|G|, which is positive since |C| \ge 1 (Lemma 6.1.4) and |G| \ge 1. Apply Lemma 6.1.3.

Theorem 6.3 Lemma 6.1.3 Lemma 6.1.4

Corollary6.1.7
uses 1used by 0✓L∃∀N

Dirichlet, density form. For n \ge 1 and a \in (\mathbb{Z}/n\mathbb{Z})^\times, the Dirichlet density of the rational primes p with p \equiv a \pmod{n} equals 1/\varphi(n).

Theorem 6.3

Lean code for Corollary6.1.7●1 theorem
  • theoremdefined in CebotarevDensity/Main.lean
    complete
    theorem Chebotarev.dirichlet_primes_in_AP (n : ℕ) (hn : 1 ≤ n) (a : ZMod n)
  (ha : IsUnit a) :
  Chebotarev.HasDirichletDensity
    ((fun p ↦ Ideal.span {↑p}) '' {p | Nat.Prime p ∧ ↑p = a})
    (↑n.totient)⁻¹
    theorem Chebotarev.dirichlet_primes_in_AP (n : ℕ)
  (hn : 1 ≤ n) (a : ZMod n)
  (ha : IsUnit a) :
  Chebotarev.HasDirichletDensity
    ((fun p ↦ Ideal.span {↑p}) ''
      {p | Nat.Prime p ∧ ↑p = a})
    (↑n.totient)⁻¹
    **Dirichlet's theorem on primes in arithmetic progressions**, as a
density refinement of `Nat.infinite_setOf_prime_and_eq_mod`.

For coprime integers `a, n` with `1 ≤ n` and `gcd a n = 1`, the Dirichlet
density of primes `p` with `p ≡ a mod n` equals `1 / φ(n)`. This is the
specialisation of Chebotarev to `K = ℚ`, `L = ℚ(μ_n)` (Sharifi 7.2.3).
Proof for Corollary 6.1.7
uses 0

Specialise Theorem 6.3 to K = \mathbb{Q}, L = \mathbb{Q}(\zeta_n). The cyclotomic character identifies \Gal{\mathbb{Q}(\zeta_n)/\mathbb{Q}} with (\mathbb{Z}/n\mathbb{Z})^\times; under this identification, the Frobenius \sigma_p at unramified p corresponds to p \bmod n. The Galois group is abelian, so each conjugacy class is a singleton; the set of primes with p \equiv a \pmod{n} is the Frobenius preimage of \{a\}, whose density is 1/\varphi(n).