Module

IsUpperRamificationJump.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.IsUpperRamificationJump

2 declarations indexed from sourceView source ↗

Module documentation

Upper ramification jumps

The right-limit group is the supremum of upper groups at strictly larger indices. A jump occurs exactly when that right limit differs from the group at the index itself.

Imports1

Nyll.ClassFieldTheory.Definitions.HasseArf.UpperRamificationGroup

Imported by4

def

upperRamificationGroupAfter

L24 ↗

ClassFieldTheory.upperRamificationGroupAfter

Documentation

The upper ramification group immediately after a real index.

Source context 3 commands

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

noncomputable section
namespace ClassFieldTheory
universe u v

Lean source · statement

def upperRamificationGroupAfter
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (t : ℝ) :
    Subgroup (((ValuativeRel.valuation L).valuationSubring).decompositionSubgroup K)

def