NYLL

theorem · Sawin’s totally real towers

Which finite fields lie in the maximal extension?

Admissibility is equivalent to containment in the constructed maximal extension.

Containment recovers the arithmetic conditions needed for discriminant and splitting arguments, making it useful when choosing finite subextensions of large degree inside an infinite extension. The reason is that a finite subfield of the directed compositum lies in a single admissible layer. This connects the finite-layer viewpoint of profinite Galois theory with the prescribed-ramification setting studied by Shafarevich.

SawinTotallyRealTowers on GitHub ↗

Mathematical statement

Write $M_{p,T}$ for the compositum in $\overline{\mathbb Q}$ of the finite Galois extensions that are totally real, unramified outside $T$, and have $p$-group Galois group. For prime $p$, this is the maximal totally real pro-$p$ extension unramified outside $T$.

Let $T$ be a set of finite places of $\mathbb Q$, and let $E$ be a finite Galois intermediate field of $\overline{\mathbb Q}/\mathbb Q$. Then $$E\subseteq M_{p,T}\quad\Longleftrightarrow\quad E\text{ is an admissible finite layer for }(p,T).$$

Admissibility means a $p$-group Galois group, no finite ramification outside $T$, and no infinite-place ramification. The declaration is stated for a natural-number parameter $p$; its later uses take $p$ prime. The finite Galois hypothesis on $E$ is part of the statement.

Lean code

ClassFieldTower.Sawin.isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside

Published library source ↗Same source in NYLL ↗

theorem isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsAdmissibleFiniteLayer p T E ↔
      E.toIntermediateField ≤ maximalRealProPOutside p T
In-scope Lean context
open scoped NumberField

open NumberField IsDedekindDomain

noncomputable section

namespace ClassFieldTower.Sawin
Full declaration and proof
/-- A finite Galois intermediate field lies in the maximal compositum
exactly when it satisfies the original arithmetic conditions. Directed
finite support and descent rule out additional inadmissible finite layers. -/
theorem isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsAdmissibleFiniteLayer p T E ↔
      E.toIntermediateField ≤ maximalRealProPOutside p T := by
  constructor
  · intro hE
    exact le_maximalRealProPOutside ⟨E, hE⟩
  · intro hE
    obtain ⟨C, hEC⟩ := finiteDimensional_le_iSup_realPExtension_exists_extension
      p T E.toIntermediateField hE
    exact IsAdmissibleFiniteLayer.of_le hEC C.property
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

  1. 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.
  2. Luis Ribes and Pavel Zalesskii. Profinite Groups. Springer-Verlag Berlin Heidelberg, 2010. Second edition; background for Frattini quotients, generator rank, and pro-p presentations.

Published source: 9c13deb1.

← All selected results in Sawin’s totally real towers