Module

ArithmeticStageChosenUnramified.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.ArithmeticStageChosenUnramified

1 declaration indexed from sourceView source ↗

Module documentation

Chosen finite-place completions of an unramified arithmetic stage

The stage's everywhere-unramified certificate applies at the actual global centre of the chosen finite-place extension. The ideal-to-completion comparison therefore supplies unramifiedness for the chosen local completion, without a new local hypothesis.

Imports2

Imported by3

theorem

openNormalArithmeticStage_chosenFinitePlaceIsUnramified

L28 ↗

ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_chosenFinitePlaceIsUnramified

Documentation

Every chosen finite-place completion of the arithmetic stage is unramified.

Source context 5 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem openNormalArithmeticStage_chosenFinitePlaceIsUnramified
    (hpOdd : Odd p)
    (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
    (v : HeightOneSpectrum (𝓞 F)) :
    ChosenFinitePlaceIsUnramified
      (K := F) (L := (openNormalArithmeticStage F p hpOdd U).field) v

Module documentation

Chosen finite-place completions of an unramified arithmetic stage

Declarations

openNormalArithmeticStage_chosenFinitePlaceIsUnramified