NYLL
Module

MaximalRealProPOutside.lean

Nyll.SawinTotallyRealTowers.MaximalRealProPOutside
5 declarations indexed from sourceView source ↗

Module documentation

The maximal real compositum with prescribed ramification support

The field is formed from the concrete directed family of finite layers. Galoisness and total reality follow from the corresponding properties of those layers. The pro-p property and arithmetic rank estimates are separate theorems, not inputs to this construction.

Imports4
Imported by18

Declarations

def

maximalRealProPOutside

L30 ↗
ClassFieldTower.Sawin.maximalRealProPOutside
Documentation

The compositum of all admissible finite real p-extensions of ℚ inside its fixed algebraic closure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
def maximalRealProPOutside (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IntermediateField ℚ (AlgebraicClosure ℚ)
theorem

le_maximalRealProPOutside

L35 ↗
ClassFieldTower.Sawin.le_maximalRealProPOutside
Documentation

Every admissible finite layer is contained in the maximal compositum.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
theorem le_maximalRealProPOutside {p : ℕ}
    {T : Set (HeightOneSpectrum (𝓞 ℚ))}
    (E : FiniteRealPExtension p T) :
    E.val.toIntermediateField ≤ maximalRealProPOutside p T
theorem

maximalRealProPOutside_isGalois

L42 ↗
ClassFieldTower.Sawin.maximalRealProPOutside_isGalois
Documentation

The constructed maximal compositum is Galois over ℚ.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
theorem maximalRealProPOutside_isGalois (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T)
theorem

maximalRealProPOutside_isTotallyReal

L56 ↗
ClassFieldTower.Sawin.maximalRealProPOutside_isTotallyReal
Documentation

Total reality is preserved by the full, possibly infinite compositum.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
theorem maximalRealProPOutside_isTotallyReal (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsTotallyReal (maximalRealProPOutside p T)
theorem

isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside

L75 ↗
ClassFieldTower.Sawin.isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside
Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
Lean source · statement
theorem isAdmissibleFiniteLayer_iff_le_maximalRealProPOutside
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) :
    IsAdmissibleFiniteLayer p T E ↔
      E.toIntermediateField ≤ maximalRealProPOutside p T

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.