Module

FiniteExtensionCompleteDVF.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.FiniteExtensionCompleteDVF

11 declarations indexed from sourceView source ↗

Module documentation

Complete-DVF packages for local fields and their finite extensions

The canonical complete discrete valuation on a nonarchimedean local field, and an integral-closure valuation chosen on each finite separable extension.

The canonical complete discrete valuation

Chosen ramification data for an arbitrary finite local extension

Imports5

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.Basic
Mathlib.Algebra.Order.Hom.Units
Mathlib.NumberTheory.LocalField.Basic
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteIntegralClosure
Nyll.ValuedFieldTheory.Valuation.ValuedAdicComplete

Imported by19

def

localCompleteDVF

L36 ↗

LocalFieldTheory.localCompleteDVF

Documentation

The canonical valuation of a nonarchimedean local field, packaged as a complete discrete valuation field.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

def localCompleteDVF
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    CompleteDVF.{u, u} K

theorem

localCompleteDVFValuation_hasExtension

L59 ↗

LocalFieldTheory.localCompleteDVFValuation_hasExtension

Documentation

The canonical complete-DVF packages preserve an existing extension of the underlying valuative relations.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem localCompleteDVFValuation_hasExtension
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    (localCompleteDVF K).valuation.HasExtension
      (localCompleteDVF L).valuation

theorem

localCompleteDVF_integerRing_isIntegralClosure

L78 ↗

LocalFieldTheory.localCompleteDVF_integerRing_isIntegralClosure

Documentation

The valuation integer ring of a finite separable local extension is the integral closure of the base valuation integer ring.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem localCompleteDVF_integerRing_isIntegralClosure
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    IsIntegralClosure 𝒪[L] 𝒪[K] L

theorem

localCompleteDVF_integerRing_moduleFinite

L100 ↗

LocalFieldTheory.localCompleteDVF_integerRing_moduleFinite

Documentation

The valuation integer ring of a finite separable local extension is a finite module over the base valuation integer ring.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem localCompleteDVF_integerRing_moduleFinite
    (K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)] :
    Module.Finite 𝒪[K] 𝒪[L]

theorem

chosenLocalExtensionCompleteDVF_exists

L114 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF_exists

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · full declaration

theorem chosenLocalExtensionCompleteDVF_exists
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ∃ target : CompleteDVF.{0, 0} L,
      ∃ hExt : (localCompleteDVF K).valuation.HasExtension target.valuation,
        letI : (localCompleteDVF K).valuation.HasExtension target.valuation :=
          hExt
        IsIntegralClosure target.valuationSubring
          (localCompleteDVF K).valuationSubring L := by
  obtain ⟨target, hExt, hIntegralClosure, _hDefectless⟩ :=
    exists_integralClosure_standard_fundamental_identity
      (K := K) (L := L) (localCompleteDVF K)
  exact ⟨target, hExt, hIntegralClosure⟩

def

chosenLocalExtensionCompleteDVF

L132 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF

Documentation

A complete discrete valuation on an arbitrary finite separable extension of a nonarchimedean local field, chosen from its actual integral closure.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

def chosenLocalExtensionCompleteDVF
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    CompleteDVF.{0, 0} L

theorem

chosenLocalExtensionCompleteDVF_hasExtension

L142 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF_hasExtension

Documentation

The chosen valuation on a finite local extension extends the canonical valuation of its base field.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem chosenLocalExtensionCompleteDVF_hasExtension
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (localCompleteDVF K).valuation.HasExtension
      (chosenLocalExtensionCompleteDVF K L).valuation

instance

instHasExtension

L154 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF.instHasExtension

Documentation

Supplies the valuation-extension instance for the chosen finite local extension target.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

instance chosenLocalExtensionCompleteDVF.instHasExtension
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (localCompleteDVF K).valuation.HasExtension
      (chosenLocalExtensionCompleteDVF K L).valuation

theorem

chosenLocalExtensionCompleteDVF_isIntegralClosure

L165 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF_isIntegralClosure

Documentation

The chosen valuation ring is the actual integral closure of the canonical valuation ring of the base local field.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem chosenLocalExtensionCompleteDVF_isIntegralClosure
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    IsIntegralClosure
      (chosenLocalExtensionCompleteDVF K L).valuationSubring
      (localCompleteDVF K).valuationSubring L

theorem

chosenLocalExtensionCompleteDVF_valuationSubring_moduleFinite

L178 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF_valuationSubring_moduleFinite

Documentation

The chosen valuation ring of a finite separable local extension is a finite module over the canonical base valuation ring.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem chosenLocalExtensionCompleteDVF_valuationSubring_moduleFinite
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Module.Finite
      (localCompleteDVF K).valuationSubring
      (chosenLocalExtensionCompleteDVF K L).valuationSubring

theorem

chosenLocalExtensionCompleteDVF_hasUniqueValuationExtension

L195 ↗

LocalFieldTheory.chosenLocalExtensionCompleteDVF_hasUniqueValuationExtension

Documentation

Completeness of the base makes the chosen valuation extension unique.

Source context 6 commands

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

noncomputable section
namespace LocalFieldTheory
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
open scoped ValuativeRel
universe u v y

Lean source · statement

theorem chosenLocalExtensionCompleteDVF_hasUniqueValuationExtension
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    ValuedExtension.HasUniqueValuationExtension.{0, 0, 0, 0, y}
      (base := localCompleteDVF K)
      (target := chosenLocalExtensionCompleteDVF K L)

Module documentation

Complete-DVF packages for local fields and their finite extensions

The canonical complete discrete valuation

Chosen ramification data for an arbitrary finite local extension

Declarations