A weak nonsplitting theorem for number fields

This file proves the global fact needed by the inverse-cyclotomic argument: a nontrivial finite Galois extension of number fields has a finite prime that does not split completely.

The proof uses only the pinned Mathlib. Two hypothetical prime lifts above every base prime give a norm-multiplying injection from pairs of nonzero ideals into nonzero ideals of the extension. Regrouping the Dedekind zeta series by ideals then forces the zeta function of the extension to dominate the square of the base zeta function, contradicting the simple poles supplied by the class-number formula.

The conceptual route was identified during the prior-art audit of DE0CH/flt-lean recorded in docs/PRIOR_ART.md; no source text is copied from that unlicensed repository. The finite-fibre counting identity below is adapted from the Apache-2.0 Mathlib proof of NumberField.tendsto_sub_one_mul_dedekindZeta_nhdsGT, authored by Xavier Roblot.

Unique-factorization encoding of pairs of ideals

noncomputable def NumberTheory.WeakChebotarev.spectrumFactors (R : Type u_1) [CommRing R] [IsDedekindDomain R] (I : Ideal R) : Multiset (IsDedekindDomain.HeightOneSpectrum R)

The normalized prime factors of an ideal, regarded as finite primes.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.WeakChebotarev.spectrumFactors_map_asIdeal (R : Type u_1) [CommRing R] [IsDedekindDomain R] (I : Ideal R) : Multiset.map IsDedekindDomain.HeightOneSpectrum.asIdeal (spectrumFactors R I) = UniqueFactorizationMonoid.normalizedFactors I

theorem NumberTheory.WeakChebotarev.spectrumFactors_prod_asIdeal (R : Type u_1) [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ 0) : (Multiset.map IsDedekindDomain.HeightOneSpectrum.asIdeal (spectrumFactors R I)).prod = I

theorem NumberTheory.WeakChebotarev.disjSum_injective (R : Type u_1) [CommRing R] : Function.Injective fun (st : Multiset (IsDedekindDomain.HeightOneSpectrum R) × Multiset (IsDedekindDomain.HeightOneSpectrum R)) => st.1.disjSum st.2

@[reducible, inline]

abbrev NumberTheory.WeakChebotarev.FinitePrime (K : Type u_2) [Field K] [NumberField K] : Type u_2

A finite prime of a number field, represented by a nonzero prime ideal.

Equations

• NumberTheory.WeakChebotarev.FinitePrime K = IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)

theorem NumberTheory.WeakChebotarev.exists_normProductIdealEmbedding {K : Type u_2} {F : Type u_3} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] (h : ∀ (v : FinitePrime K), ∃ (q₁ : FinitePrime F) (q₂ : FinitePrime F), q₁ ≠ q₂ ∧ Ideal.under (NumberField.RingOfIntegers K) q₁.asIdeal = v.asIdeal ∧ Ideal.under (NumberField.RingOfIntegers K) q₂.asIdeal = v.asIdeal ∧ Ideal.absNorm q₁.asIdeal = Ideal.absNorm v.asIdeal ∧ Ideal.absNorm q₂.asIdeal = Ideal.absNorm v.asIdeal) : ∃ (Φ : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) × ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) → ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers F)))), Function.Injective Φ ∧ ∀ (IJ : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K))) × ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), Ideal.absNorm ↑(Φ IJ) = Ideal.absNorm ↑IJ.1 * Ideal.absNorm ↑IJ.2

Two disjoint, norm-preserving choices of primes above every base prime extend multiplicatively to an injective norm-product map on pairs of nonzero ideals.

Regrouping the Dedekind zeta series by nonzero ideals

theorem NumberTheory.WeakChebotarev.tendsto_sum_card_absNorm_eq_div (K : Type u_1) [Field K] [NumberField K] : Filter.Tendsto (fun (n : ℕ) => (∑ m ∈ Finset.Icc 1 n, ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = m })) / ↑n) Filter.atTop (nhds (NumberField.dedekindZeta_residue K))

The partial sums of the norm-fibre cardinalities have the residue of the Dedekind zeta function as their linear asymptotic. The finite-fibre rewrite is adapted from the pinned Mathlib class-number-formula proof.

theorem NumberTheory.WeakChebotarev.lseriesSummable_dedekindZeta (K : Type u_1) [Field K] [NumberField K] {s : ℝ} (hs : 1 < s) : LSeriesSummable (fun (n : ℕ) => ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n })) ↑s

Absolute convergence of the coefficient presentation of the Dedekind zeta series for real s > 1.

noncomputable def NumberTheory.WeakChebotarev.idealZeta (K : Type u_1) [Field K] [NumberField K] (s : ℝ) : ℝ

The real Dirichlet series indexed directly by nonzero integral ideals.

Equations

• NumberTheory.WeakChebotarev.idealZeta K s = ∑' (I : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ }), ↑(Ideal.absNorm ↑I) ^ (-s)

theorem NumberTheory.WeakChebotarev.dedekindZeta_re_eq_idealZeta (K : Type u_1) [Field K] [NumberField K] (s : ℝ) (hs : 1 < s) : (NumberField.dedekindZeta K ↑s).re = idealZeta K s

For s > 1, Mathlib's coefficient definition of Dedekind zeta is the sum of N(I)⁻ˢ over nonzero ideals.

Square domination and the pole contradiction

From complete splitting to the two prime lifts

theorem NumberTheory.WeakChebotarev.exists_nonSplitFinitePrime {K : Type u_1} {F : Type u_2} [Field K] [NumberField K] [Field F] [NumberField F] [Algebra K F] [IsGalois K F] (hdeg : 1 < Module.finrank K F) : ∃ (v : FinitePrime K), (v.asIdeal.primesOver (NumberField.RingOfIntegers F)).ncard ≠ Module.finrank K F

Every nontrivial finite Galois extension of number fields has a finite prime that does not split completely.