Module

Unramified.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.Filtered.Unramified

3 declarations indexed from sourceView source ↗

Module documentation

Artin filtrations of unramified local extensions

The Artin map kills valuation-ring units in an unramified finite extension, so every positive principal-unit image is trivial.

The Artin principal-unit filtration

Imports6

Imported by3

theorem

abelianLocalArtinMonoidHom_integerUnits_eq_one_of_unramifiedValuation

L36 ↗

LocalClassFieldTheory.abelianLocalArtinMonoidHom_integerUnits_eq_one_of_unramifiedValuation

Documentation

Every valuation-ring unit has trivial actual abelian Artin symbol in an unramified finite extension.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · statement

theorem
    abelianLocalArtinMonoidHom_integerUnits_eq_one_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (u : 𝒪[K]ˣ) :
    abelianLocalArtinMonoidHom K L
        (LocalFieldTheory.IsNonarchimedeanLocalField.integerUnitsToFieldUnits
          K u) = 1

theorem

artinPrincipalUnitGroup_eq_bot_of_unramifiedValuation

L60 ↗

LocalClassFieldTheory.artinPrincipalUnitGroup_eq_bot_of_unramifiedValuation

Documentation

Every integral Artin principal-unit group of an unramified finite abelian extension is trivial.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · statement

theorem artinPrincipalUnitGroup_eq_bot_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (n : ℕ) :
    artinPrincipalUnitGroup K L n = ⊥

theorem

artinPrincipalUnitStepGroup_eq_bot_of_unramifiedValuation

L84 ↗

LocalClassFieldTheory.artinPrincipalUnitStepGroup_eq_bot_of_unramifiedValuation

Documentation

The real ceiling-step Artin filtration is therefore trivial at every index on an unramified finite abelian extension.

Source context 8 commands

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

noncomputable section
namespace LocalClassFieldTheory
open LocalClassFieldTheory
open LocalFieldTheory
open RamificationTheory.HilbertRamification
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel

Lean source · statement

theorem artinPrincipalUnitStepGroup_eq_bot_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [UniformSpace L] [IsUniformAddGroup L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L]
    (t : ℝ) :
    artinPrincipalUnitStepGroup K L t = ⊥

Module documentation

Artin filtrations of unramified local extensions

The Artin principal-unit filtration

Declarations

abelianLocalArtinMonoidHom_integerUnits_eq_one_of_unramifiedValuation

artinPrincipalUnitGroup_eq_bot_of_unramifiedValuation

artinPrincipalUnitStepGroup_eq_bot_of_unramifiedValuation