definition · Sawin’s totally real towers

The maximal real pro-p extension with restricted ramification

The ambient arithmetic extension is built from its admissible finite Galois layers.

Taking composita preserves the required conditions, keeping finite portions of the extension accessible through finite Galois theory. At p equal to two, controlling finite ramification alone does not ensure total reality, so the infinite-place condition matters. Shafarevich’s 1963 work on prescribed ramification provides the arithmetic setting for studying such extensions through their generators and relations.

SawinTotallyRealTowers on GitHub ↗

Mathematical statement

Fix a prime $p$ and a set $T$ of finite places of $\mathbb Q$. A finite Galois intermediate field $E\subseteq\overline{\mathbb Q}$ is admissible when $\operatorname{Gal}(E/\mathbb Q)$ is a $p$-group, $E/\mathbb Q$ is unramified at finite places outside $T$, and it is unramified at infinite places.

The extension is defined inside a fixed algebraic closure by $$M_{p,T}=\bigvee_{\text{admissible }E}E.$$ Over $\mathbb Q$, the infinite-place condition says that the finite layer is totally real. The Lean definition allows a natural-number parameter; the prime case is the intended pro-$p$ application.

Lean code

`ClassFieldTower.Sawin.IsAdmissibleFiniteLayer`

Published library source ↗Same source in NYLL ↗

def IsAdmissibleFiniteLayer (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) : Prop

In-scope Lean context

open scoped NumberField

open NumberField IsDedekindDomain

noncomputable section

namespace ClassFieldTower.Sawin

private local instance finiteGaloisNumberField
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) : NumberField E :=
  NumberField.of_module_finite ℚ E

Full declaration and proof

/-- The finite layers permitted in the initial real pro-p tower. -/
def IsAdmissibleFiniteLayer (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) : Prop :=
  IsPGroup p (E ≃ₐ[ℚ] E) ∧
    IsUnramifiedAtFinitePlacesOutside ℚ E T ∧
      IsUnramifiedAtInfinitePlaces ℚ E

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

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.

Published source: 9c13deb1.

← All selected results in Sawin’s totally real towers