Module

Unramified.lean

Nyll.ValuedFieldTheory.Ramification.LocalField.Unramified

3 declarations indexed from sourceView source ↗

Module documentation

Ramification groups of unramified local extensions

This file connects the concrete unramified-valued-extension predicate with the actual upper ramification groups of a finite local extension.

Imports3

Imported by9

theorem

localCompleteDVF_valuation_eq_valuativeRel

L34 ↗

RamificationTheory.LocalField.localCompleteDVF_valuation_eq_valuativeRel

Documentation

The complete-DVF package used by local reciprocity contains the canonical valuation of the local field.

Source context 9 commands

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

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

Lean source · statement

theorem localCompleteDVF_valuation_eq_valuativeRel
    (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (localCompleteDVF K).valuation = ValuativeRel.valuation K

theorem

localLowerRamificationGroup_zero_eq_bot_of_unramifiedValuation

L44 ↗

RamificationTheory.LocalField.localLowerRamificationGroup_zero_eq_bot_of_unramifiedValuation

Documentation

The inertia group, equivalently the lower ramification group at zero, is trivial for an actual finite unramified Galois extension of local fields.

Source context 9 commands

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

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

Lean source · statement

theorem localLowerRamificationGroup_zero_eq_bot_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    localLowerRamificationGroup K L 0 = ⊥

theorem

localUpperRamificationGroup_eq_bot_of_unramifiedValuation

L164 ↗

RamificationTheory.LocalField.localUpperRamificationGroup_eq_bot_of_unramifiedValuation

Documentation

Every nonnegative upper ramification group of an actual finite unramified Galois extension of local fields is trivial.

Source context 9 commands

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

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

Lean source · statement

theorem localUpperRamificationGroup_eq_bot_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (t : ℝ) (ht : 0 ≤ t) :
    localUpperRamificationGroup K L t = ⊥

Module documentation

Ramification groups of unramified local extensions

Declarations

localCompleteDVF_valuation_eq_valuativeRel

localLowerRamificationGroup_zero_eq_bot_of_unramifiedValuation

localUpperRamificationGroup_eq_bot_of_unramifiedValuation