Module

RealProPStageLocalConditions.lean

Nyll.SawinTotallyRealTowers.RealProPStageLocalConditions

4 declarations indexed from sourceView source ↗

Module documentation

Local conditions of actual finite real p-layers

The global ramification certificates on an admissible finite layer imply the actual chosen-completion conditions used by finite H² localization.

Imports3

Imported by2

instance

stageNumberField

L23 ↗

ClassFieldTower.Sawin.stageNumberField

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin

Lean source · statement

instance stageNumberField (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) : NumberField E.val

instance

stageIsGalois

L27 ↗

ClassFieldTower.Sawin.stageIsGalois

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
private local instance stageNumberField (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) : NumberField E.val :=
  NumberField.of_module_finite ℚ E.val

Lean source · statement

instance stageIsGalois (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) :
    IsGalois ℚ E.val.toIntermediateField

theorem

finiteRealPExtension_chosenFinitePlaceIsUnramified

L33 ↗

ClassFieldTower.Sawin.finiteRealPExtension_chosenFinitePlaceIsUnramified

Documentation

The actual chosen completion of an admissible layer is unramified at every finite place outside its allowed support.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
private local instance stageNumberField (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) : NumberField E.val :=
  NumberField.of_module_finite ℚ E.val
private local instance stageIsGalois (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) :
    IsGalois ℚ E.val.toIntermediateField := E.val.isGalois

Lean source · statement

theorem finiteRealPExtension_chosenFinitePlaceIsUnramified
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T)
    (v : HeightOneSpectrum (𝓞 ℚ)) (hv : v ∉ T) :
    ChosenFinitePlaceIsUnramified (K := ℚ) (L := E.val) v

theorem

finiteRealPExtension_chosenInfinitePlaceIsUnramified

L42 ↗

ClassFieldTower.Sawin.finiteRealPExtension_chosenInfinitePlaceIsUnramified

Documentation

Every chosen infinite place of an admissible layer is unramified.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
private local instance stageNumberField (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) : NumberField E.val :=
  NumberField.of_module_finite ℚ E.val
private local instance stageIsGalois (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T) :
    IsGalois ℚ E.val.toIntermediateField := E.val.isGalois

Lean source · statement

theorem finiteRealPExtension_chosenInfinitePlaceIsUnramified
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) (E : FiniteRealPExtension p T)
    (v : InfinitePlace ℚ) :
    (chosenInfinitePlaceAbove (L := E.val) v).IsUnramified ℚ

Module documentation

Local conditions of actual finite real p-layers

Declarations

stageNumberField

stageIsGalois

finiteRealPExtension_chosenFinitePlaceIsUnramified

finiteRealPExtension_chosenInfinitePlaceIsUnramified