Shafarevich’s relation-rank bound for odd primes

Mathematical statement

Let $F$ be a number field and $p$ an odd prime. Let $G$ be its maximal everywhere-unramified pro-$p$ Galois group, and let $d(G)$ be its finite topological generator rank. Write $r_1,r_2$ for its numbers of real and complex places and put $\delta=1$ if $F$ contains a primitive $p$th root of unity, and $\delta=0$ otherwise.

The theorem proves that $H^2_{\mathrm{cont}}(G,\mathbb F_p)$ is finite-dimensional and $$\dim_{\mathbb F_p}H^2_{\mathrm{cont}}(G,\mathbb F_p)\le d(G)+(r_1+r_2-1)+\delta.$$ The coefficient module is the trivial module.

Lean code

`ClassFieldTower.Martinet.Shafarevich.shafarevich_relation_rank_bound`

Published library source ↗Same source in NYLL ↗

theorem shafarevich_relation_rank_bound :
    FiniteDimensional (ZMod p)
      (continuousCohomologyZModP p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
    (open Classical in
      Module.finrank (ZMod p)
        (continuousCohomologyZModP p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
      finiteTopologicalGeneratorRank (MaxEverywhereUnramifiedProPGaloisGroup F p) +
        (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  exact maxEverywhereUnramified_smallH2_and_finiteGeneratorRank_bound_of_lifted F p hpOdd
    (NumberField.InfinitePlace.nrRealPlaces F + NumberField.InfinitePlace.nrComplexPlaces F - 1)
    (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)
    (shafarevich_relation_rank_bound_lifted F p hpOdd)

In-scope Lean context

open scoped NumberField Topology

noncomputable section

namespace ClassFieldTower.Martinet.Shafarevich

open ClassFieldTower.Cohomology ClassFieldTower.ProP ClassFieldTower.Martinet

open ProCGroups.Generation ProCGroups.FiniteGeneration

variable (F : Type) [Field F] [NumberField F]

variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)

include hpOdd

Full declaration and proof

/-- Shafarevich's bound with ordinary coefficients and finite-set generator rank. -/
theorem shafarevich_relation_rank_bound :
    FiniteDimensional (ZMod p)
      (continuousCohomologyZModP p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ∧
    (open Classical in
      Module.finrank (ZMod p)
        (continuousCohomologyZModP p (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) ≤
      finiteTopologicalGeneratorRank (MaxEverywhereUnramifiedProPGaloisGroup F p) +
        (NumberField.InfinitePlace.nrRealPlaces F +
          NumberField.InfinitePlace.nrComplexPlaces F - 1) +
          (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)) := by
  classical
  exact maxEverywhereUnramified_smallH2_and_finiteGeneratorRank_bound_of_lifted F p hpOdd
    (NumberField.InfinitePlace.nrRealPlaces F + NumberField.InfinitePlace.nrComplexPlaces F - 1)
    (if ∃ ζ : F, IsPrimitiveRoot ζ p then 1 else 0)
    (shafarevich_relation_rank_bound_lifted F p hpOdd)

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)
Statement adapted from Lean Eval:
https://github.com/leanprover/lean-eval/blob/4ae7061fe4b0b70dcb7fe24fdee067b68636226b/generated/shafarevich_relation_rank_bound/Challenge.lean
Lean Eval repository: Copyright 2026 Lean FRO, LLC; Apache 2.0.

References

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.
Igor R. Šafarevič. Extensions à points de ramification donnés (en russe). Publications Mathématiques de l’IHÉS, Institut des Hautes Études Scientifiques, 18, 71–92, 1963.