Module

EqualCharacteristic.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.Filtered.EqualCharacteristic

1 declaration indexed from sourceView source ↗

Module documentation

Filtered local reciprocity in equal characteristic

Every finite abelian extension of a positive-characteristic local field embeds in a standard finite abelian compositum. Passing to the field range inside the fixed separable closure lets filtered reciprocity descend by restriction. A base-linear equivalence from the original extension to that field range then transports both the Artin and upper filtrations back.

Imports7

Imported by2

theorem

equalCharacteristic_filteredLocalReciprocity

L39 ↗

LocalClassFieldTheory.equalCharacteristic_filteredLocalReciprocity

Documentation

Real filtered local reciprocity for an arbitrary finite abelian extension of a positive-characteristic nonarchimedean local field.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem equalCharacteristic_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (t : ℝ) (ht : 0 ≤ t) :
    artinPrincipalUnitStepGroup K L t =
      localUpperRamificationGroup K L t

Module documentation

Filtered local reciprocity in equal characteristic

Declarations

equalCharacteristic_filteredLocalReciprocity