Module

UpperRamificationGroup.lean

Nyll.ClassFieldTheory.Definitions.HasseArf.UpperRamificationGroup

1 declaration indexed from sourceView source ↗

Module documentation

Real-index upper ramification groups

The upper group at t is the public real lower group at the inverse Herbrand index ψ(t).

Imports2

Imported by7

def

upperRamificationGroup

L25 ↗

ClassFieldTheory.upperRamificationGroup

Documentation

The upper ramification group of the canonical valuation ring of a finite Abelian local extension, using the inverse public Herbrand function.

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 upperRamificationGroup
    (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)

Module documentation

Real-index upper ramification groups

Declarations

upperRamificationGroup