Module

FirstRamificationComparison.lean

Nyll.ValuedFieldTheory.Ramification.LocalField.FirstRamificationComparison

2 declarations indexed from sourceView source ↗

Module documentation

The first lower ramification group of a local field extension

The canonical complete-DVF valuation on a finite local extension specializes the general comparison between the first lower group and Hilbert's ramification group. The latter is transported from the decomposition group back to the full Galois group.

Imports2

Imported by2

theorem

localLowerRamificationGroup_one_eq_hilbertRamificationGroup

L31 ↗

RamificationTheory.LocalField.localLowerRamificationGroup_one_eq_hilbertRamificationGroup

Documentation

The first lower group of the chosen local extension is Hilbert's ramification group for its canonical valuation ring.

Source context 6 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

Lean source · statement

theorem localLowerRamificationGroup_one_eq_hilbertRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    localLowerRamificationGroup K L 1 =
      Subgroup.comap
        (RamificationTheory.HilbertRamification.CompleteDVF.galEquivDecompositionGroup
          (base := localCompleteDVF K)
          (target := chosenLocalExtensionCompleteDVF K L)).toMonoidHom
        (RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInDecomposition K
          (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring)

theorem

localLowerRamificationGroup_one_eq_bot_iff_hilbertRamificationGroup_eq_bot

L64 ↗

RamificationTheory.LocalField.localLowerRamificationGroup_one_eq_bot_iff_hilbertRamificationGroup_eq_bot