Killing infinitely many Frobenius elements without making the group finite

Mathematical statement

Let $G=\operatorname{Gal}(M_{2,S}/\mathbb Q)$ with $S=\{3,5,7,11,13,17\}$, where $M_{2,S}$ is the maximal totally real pro-$2$ extension of $\mathbb Q$ unramified at finite primes outside $S$. There is a sequence of primes $q_n>n$, outside $S$ and congruent to one modulo four, with infinite range, for which $$G/\overline{\langle\!\langle\operatorname{Frob}_{q_n}:n\ge0\rangle\!\rangle}$$ is infinite.

The accompanying decomposition-group theorem states that the image of the entire decomposition group at each selected prime is trivial in this quotient. This is the group-theoretic condition that will force complete splitting in the corresponding fixed field.

Lean code

`ClassFieldTower.Sawin.exists_sawinInfinite_frobenius_quotient`

Published library source ↗Same source in NYLL ↗

theorem exists_sawinInfinite_frobenius_quotient :
    ∃ primes : ℕ → Nat.Primes,
      (∀ n : ℕ, n < (primes n).val ∧
        (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n) ∉
          sawinRationalPrimeSupport ∧
        (primes n).val % 4 = 1) ∧
      (Set.range primes).Infinite ∧
      Infinite ((maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) ⧸
        closedNormalClosure (Set.range (fun n : ℕ ↦
          maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
            ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n))))) := by
  obtain ⟨sourceData, r, P, hP, hr, primes, f, h⟩ := exists_sawinDeepFrobenius_sequence
  have hInfinite := P.infinite_target_quotient_of_countable_relator_budget
    (fun _ ↦ 2) (P.relatorZassenhausDepthAtLeast_two hP)
    f sawinFrobeniusDepth (fun n ↦ (h n).2.2.2.2)
    (t := (5 / 12 : ℝ)) (by norm_num) (by norm_num)
    (sawinGsPolynomial_frobenius_prefix_nonpos r hr)
  have hmap : P.quotient ∘ f = fun n : ℕ ↦
      maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
        ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n)) :=
    funext (fun n ↦ (h n).2.2.2.1)
  rw [hmap] at hInfinite
  refine ⟨primes, fun n ↦ ⟨(h n).1, (h n).2.1, (h n).2.2.1⟩, ?_, hInfinite⟩
  have hvalues : (Set.range (fun n : ℕ ↦ (primes n).val)).Infinite :=
    Set.infinite_of_forall_exists_gt (fun a ↦ ⟨(primes a).val, ⟨a, rfl⟩, (h a).1⟩)
  intro hfinite
  apply hvalues
  apply (hfinite.image (fun q : Nat.Primes ↦ q.val)).subset
  rintro _ ⟨n, rfl⟩
  exact ⟨primes n, ⟨n, rfl⟩, rfl⟩

In-scope Lean context

open scoped NumberField

open NumberField IsDedekindDomain

namespace ClassFieldTower.Sawin

open ProCGroups ProCGroups.Presentations ClassFieldTower.ProP

private local instance frobeniusSequencePrimeTwo : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩

private local instance frobeniusSequenceIsGalois :
    IsGalois ℚ (maximalRealProPOutside 2 sawinRationalPrimeSupport) :=
  maximalRealProPOutside_isGalois 2 sawinRationalPrimeSupport

Full declaration and proof

/-- Infinitely many selected rational primes are congruent to one modulo
four and outside the six ramified primes. Killing all their actual Frobenius
elements leaves an infinite quotient of the actual initial arithmetic group. -/
theorem exists_sawinInfinite_frobenius_quotient :
    ∃ primes : ℕ → Nat.Primes,
      (∀ n : ℕ, n < (primes n).val ∧
        (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n) ∉
          sawinRationalPrimeSupport ∧
        (primes n).val % 4 = 1) ∧
      (Set.range primes).Infinite ∧
      Infinite ((maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
        maximalRealProPOutside 2 sawinRationalPrimeSupport) ⧸
        closedNormalClosure (Set.range (fun n : ℕ ↦
          maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
            ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n))))) := by
  obtain ⟨sourceData, r, P, hP, hr, primes, f, h⟩ := exists_sawinDeepFrobenius_sequence
  have hInfinite := P.infinite_target_quotient_of_countable_relator_budget
    (fun _ ↦ 2) (P.relatorZassenhausDepthAtLeast_two hP)
    f sawinFrobeniusDepth (fun n ↦ (h n).2.2.2.2)
    (t := (5 / 12 : ℝ)) (by norm_num) (by norm_num)
    (sawinGsPolynomial_frobenius_prefix_nonpos r hr)
  have hmap : P.quotient ∘ f = fun n : ℕ ↦
      maximalRealProPArithmeticFrobenius 2 sawinRationalPrimeSupport
        ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm (primes n)) :=
    funext (fun n ↦ (h n).2.2.2.1)
  rw [hmap] at hInfinite
  refine ⟨primes, fun n ↦ ⟨(h n).1, (h n).2.1, (h n).2.2.1⟩, ?_, hInfinite⟩
  have hvalues : (Set.range (fun n : ℕ ↦ (primes n).val)).Infinite :=
    Set.infinite_of_forall_exists_gt (fun a ↦ ⟨(primes a).val, ⟨a, rfl⟩, (h a).1⟩)
  intro hfinite
  apply hvalues
  apply (hfinite.image (fun q : Nat.Primes ↦ q.val)).subset
  rintro _ ⟨n, rfl⟩
  exact ⟨primes n, ⟨n, rfl⟩, rfl⟩

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

Farshid Hajir, Christian Maire, and Ravi Ramakrishna. Cutting towers of number fields. 2019. Cited as the arXiv preprint; develops cutting methods with refined Golod–Shafarevich estimates.
E. S. Golod and I. R. Shafarevich. On the class field tower. Izvestiya Akademii Nauk SSSR. Seriya Matematicheskaya, 28 (2), 261–272, 1964. Original article in Russian.