NYLL
Module

ShrinkLocalClassification.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Existence.ShrinkLocalClassification
2 declarations indexed from sourceView source ↗

Module documentation

Finite abelian local classification in arbitrary universes

The concrete classification for a small local field transfers to an arbitrary nonarchimedean local field. The transfer respects the actual field-norm subgroup.

Imports3
Imported by2

Declarations

def

shrinkFiniteAbelianFieldNormSubgroupOrderIso

L29 ↗
LocalFieldTheory.shrinkFiniteAbelianFieldNormSubgroupOrderIso
Documentation

The finite abelian classification after moving through the small representative of K.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def shrinkFiniteAbelianFieldNormSubgroupOrderIso :
    ClassFieldTheory.FiniteAbelianLocalExtension K ≃o
      (ClassFieldTheory.OpenFiniteIndexSubgroup K)ᵒᵈ
theorem

shrinkFiniteAbelianFieldNormSubgroupOrderIso_apply

L42 ↗
LocalFieldTheory.shrinkFiniteAbelianFieldNormSubgroupOrderIso_apply
Documentation

The transported order equivalence sends a finite abelian field to its actual field-norm subgroup.

Source context 4 commands

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

noncomputable section
namespace LocalFieldTheory
universe u
variable (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem shrinkFiniteAbelianFieldNormSubgroupOrderIso_apply
    (E : ClassFieldTheory.FiniteAbelianLocalExtension K) :
    (OrderDual.ofDual (shrinkFiniteAbelianFieldNormSubgroupOrderIso K E)).1 =
      E.normSubgroup

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.