Module

ChosenLocalization.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.ChosenLocalization

33 declarations indexed from sourceView source ↗

Module documentation

The chosen localization at a finite place

This file equips the actual chosen localization of a finite number-field extension with its canonical valued local-field structures. It also defines unramifiedness for that actual completed extension.

Imports2

Imported by10

abbrev

ChosenFinitePlaceBaseCompletion

L36 ↗

Documentation

The completion of the base field at the chosen finite place.

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

abbrev ChosenFinitePlaceBaseCompletion
    (w₀ : HeightOneSpectrum (𝓞 K))

instance

chosenFinitePlaceExtensionCompletionAlgebra

L40 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceExtensionCompletionAlgebra
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Algebra K
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceExtensionCompletionSMul

L47 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceExtensionCompletionSMul
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    SMul K
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceCompletionAlgebra

L54 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceCompletionAlgebra
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Algebra
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceBaseValued

L64 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseValued
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Valued
      (ChosenFinitePlaceBaseCompletion (K := K) w₀) ℝ≥0

instance

chosenFinitePlaceBaseValuativeRel

L72 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseValuativeRel
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ValuativeRel
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceLocalizedValued

L80 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedValued
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Valued
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀) ℝ≥0

instance

chosenFinitePlaceLocalizedValuativeRel

L90 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedValuativeRel
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ValuativeRel
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedValuationHasExtension

L100 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceLocalizedValuationHasExtension
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Valuation.HasExtension
      (ValuativeRel.valuation
        (ChosenFinitePlaceBaseCompletion (K := K) w₀))
      (ValuativeRel.valuation
        (ChosenFinitePlaceLocalizedCompletion
          (K := K) (L := L) w₀))

instance

chosenFinitePlaceLocalizedIntegerAlgebra

L114 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIntegerAlgebra
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Algebra
      𝒪[ChosenFinitePlaceBaseCompletion (K := K) w₀]
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIsIntegralClosure

L123 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIsIntegralClosure
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsIntegralClosure
      𝒪[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀]
      𝒪[ChosenFinitePlaceBaseCompletion (K := K) w₀]
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceBaseNontriviallyNormedField

L137 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceBaseNontriviallyNormedField
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    NontriviallyNormedField
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceBaseLocallyCompactSpace

L146 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseLocallyCompactSpace
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    LocallyCompactSpace
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceBaseIsUltrametricDist

L153 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseIsUltrametricDist
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsUltrametricDist
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceBaseValuationIsNontrivial

L161 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceBaseValuationIsNontrivial
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    (Valued.v :
      Valuation
        (ChosenFinitePlaceBaseCompletion (K := K) w₀)
        ℝ≥0).IsNontrivial

instance

chosenFinitePlaceBaseValuationCompatible

L172 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseValuationCompatible
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    (Valued.v :
      Valuation
        (ChosenFinitePlaceBaseCompletion (K := K) w₀)
        ℝ≥0).Compatible

instance

chosenFinitePlaceBaseValuativeRelIsNontrivial

L180 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceBaseValuativeRelIsNontrivial
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ValuativeRel.IsNontrivial
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceBaseIsValuativeTopology

L191 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceBaseIsValuativeTopology
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsValuativeTopology
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceBaseIsNonarchimedeanLocalField

L198 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceBaseIsNonarchimedeanLocalField
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsNonarchimedeanLocalField
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)

instance

chosenFinitePlaceCompletionFiniteDimensional

L207 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceCompletionFiniteDimensional
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    FiniteDimensional
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceCompletionContinuousSMul

L217 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceCompletionContinuousSMul
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ContinuousSMul
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceCompletionLocallyCompactSpace

L228 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceCompletionLocallyCompactSpace
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    LocallyCompactSpace
      (chosenFinitePlaceExtension (L := L) w₀).1.Completion

instance

chosenFinitePlaceLocalizedFiniteDimensional

L236 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedFiniteDimensional
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    FiniteDimensional
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIsGalois

L247 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIsGalois
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsGalois
      (ChosenFinitePlaceBaseCompletion (K := K) w₀)
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedLocallyCompactSpace

L257 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceLocalizedLocallyCompactSpace
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    LocallyCompactSpace
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIsUltrametricDist

L275 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIsUltrametricDist
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsUltrametricDist
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedValuationCompatible

L285 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedValuationCompatible
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    (Valued.v :
      Valuation
        (ChosenFinitePlaceLocalizedCompletion
          (K := K) (L := L) w₀)
        ℝ≥0).Compatible

instance

chosenFinitePlaceLocalizedValuationIsNontrivial

L294 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceLocalizedValuationIsNontrivial
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    (ValuativeRel.valuation
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)).IsNontrivial

instance

chosenFinitePlaceLocalizedValuativeRelIsNontrivial

L307 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceLocalizedValuativeRelIsNontrivial
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    ValuativeRel.IsNontrivial
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIsValuativeTopology

L318 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIsValuativeTopology
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsValuativeTopology
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIsNonarchimedeanLocalField

L327 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance
    chosenFinitePlaceLocalizedIsNonarchimedeanLocalField
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    IsNonarchimedeanLocalField
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀)

instance

chosenFinitePlaceLocalizedIntegerModuleFinite

L337 ↗

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

instance chosenFinitePlaceLocalizedIntegerModuleFinite
    (w₀ : HeightOneSpectrum (𝓞 K)) :
    Module.Finite
      𝒪[ChosenFinitePlaceBaseCompletion (K := K) w₀]
      𝒪[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) w₀]

def

ChosenFinitePlaceIsUnramified

L357 ↗

Documentation

The chosen extension of the completed field is unramified, expressed using the intrinsic valuation on the algebraic localization. The canonical local-field instances for the chosen completion are exported from this module, so clients only supply the mathematical unramifiedness hypothesis.

Source context 7 commands

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

open scoped NumberField ValuativeRel NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]

Lean source · statement

def ChosenFinitePlaceIsUnramified
    (w₀ : HeightOneSpectrum (𝓞 K)) : Prop

Module documentation

The chosen localization at a finite place

Declarations