Nyll.ValuedFieldTheory.Ramification.LocalField.InertiaCard

Module documentation

Inertia order and ramification index for a chosen local extension

The residue field of a nonarchimedean local field is finite. A finite extension of its chosen complete discrete valuation has finite-dimensional residue field, hence a separable residue extension. This supplies the residue-separability hypothesis of the general inertia-cardinality theorem.

theorem

chosenLocalExtension_inertia_card_eq_ramificationIndex

L32 ↗

RamificationTheory.LocalField.chosenLocalExtension_inertia_card_eq_ramificationIndex

Documentation

The inertia group of the chosen valuation ring has order equal to the ramification index of the chosen finite Galois local extension.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
namespace RamificationTheory.LocalField
open LocalFieldTheory
open RamificationTheory.HilbertRamification.CompleteDVF

Lean source · statement

theorem chosenLocalExtension_inertia_card_eq_ramificationIndex
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Nat.card
        ((chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring.inertiaSubgroup K) =
      ramificationIndex (localCompleteDVF K).toDVF
        (chosenLocalExtensionCompleteDVF K L).toDVF

Module documentation

Inertia order and ramification index for a chosen local extension

Declarations

chosenLocalExtension_inertia_card_eq_ramificationIndex