NYLL
Module

FiniteRealPExtension.lean

Nyll.SawinTotallyRealTowers.FiniteRealPExtension
9 declarations indexed from sourceView source ↗

Module documentation

Finite layers of the real tower with prescribed ramification

We select actual finite Galois intermediate fields of the fixed algebraic closure of ℚ. The base field is a member and binary composita remain in the family. These constructors provide the directed family used to form the maximal tower; no infiniteness or presentation is assumed.

Imports4
Imported by7

Declarations

instance

finiteGaloisNumberField

L28 ↗
ClassFieldTower.Sawin.finiteGaloisNumberField
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
instance finiteGaloisNumberField
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) : NumberField E
def

IsAdmissibleFiniteLayer

L33 ↗
ClassFieldTower.Sawin.IsAdmissibleFiniteLayer
Documentation

The finite layers permitted in the initial real pro-p tower.

Source context 5 commands

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

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
Lean source · statement
def IsAdmissibleFiniteLayer (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)) : Prop
theorem

isAdmissibleFiniteLayer_bot

L42 ↗
ClassFieldTower.Sawin.isAdmissibleFiniteLayer_bot
Documentation

The identity layer satisfies the arithmetic conditions for every prime parameter and every permitted support.

Source context 5 commands

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

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
Lean source · statement
theorem isAdmissibleFiniteLayer_bot (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsAdmissibleFiniteLayer p T ⊥
theorem

sup

L64 ↗
ClassFieldTower.Sawin.IsAdmissibleFiniteLayer.sup
Documentation

Binary composita preserve all three finite-layer conditions, including when the prime parameter is two.

Source context 5 commands

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

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
Lean source · statement
theorem IsAdmissibleFiniteLayer.sup {p : ℕ}
    {T : Set (HeightOneSpectrum (𝓞 ℚ))}
    {E F : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)}
    (hE : IsAdmissibleFiniteLayer p T E)
    (hF : IsAdmissibleFiniteLayer p T F) :
    IsAdmissibleFiniteLayer p T (E ⊔ F)
theorem

of_le

L80 ↗
ClassFieldTower.Sawin.IsAdmissibleFiniteLayer.of_le
Documentation

A finite Galois subextension of an admissible layer remains admissible. The restriction map supplies its p-group structure, and the tower descent theorems supply both local conditions.

Source context 5 commands

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

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
Lean source · statement
theorem IsAdmissibleFiniteLayer.of_le {p : ℕ}
    {T : Set (HeightOneSpectrum (𝓞 ℚ))}
    {E F : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ)}
    (hEF : E ≤ F) (hF : IsAdmissibleFiniteLayer p T F) :
    IsAdmissibleFiniteLayer p T E
def

FiniteRealPExtension

L98 ↗
ClassFieldTower.Sawin.FiniteRealPExtension
Documentation

Actual admissible finite layers, indexed without duplicating Mathlib's finite Galois intermediate-field structure.

Source context 5 commands

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

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
Lean source · statement
def FiniteRealPExtension (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) : Type
def

bot

L105 ↗
ClassFieldTower.Sawin.FiniteRealPExtension.bot
Documentation

The bottom layer of the directed family.

Source context 6 commands

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

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
namespace FiniteRealPExtension
Lean source · statement
def bot (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    FiniteRealPExtension p T
def

sup

L110 ↗
ClassFieldTower.Sawin.FiniteRealPExtension.sup
Documentation

The concrete compositum of two admissible finite layers.

Source context 6 commands

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

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
namespace FiniteRealPExtension
Lean source · statement
def sup {p : ℕ} {T : Set (HeightOneSpectrum (𝓞 ℚ))}
    (E F : FiniteRealPExtension p T) : FiniteRealPExtension p T
theorem

directed

L115 ↗
ClassFieldTower.Sawin.FiniteRealPExtension.directed
Documentation

Every pair of finite layers is contained in their admissible compositum.

Source context 6 commands

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

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
namespace FiniteRealPExtension
Lean source · full declaration
theorem directed (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    Directed (· ≤ ·)
      (fun E : FiniteRealPExtension p T ↦ E.val.toIntermediateField) := by
  intro E F
  exact ⟨sup E F, le_sup_left, le_sup_right⟩

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