NYLL
Module

CompletionToIdeal.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.UnramifiedComparison.CompletionToIdeal
5 declarations indexed from sourceView source ↗

Module documentation

From completed to ideal-theoretic unramifiedness

This file recovers ideal-theoretic unramifiedness from the actual chosen localized completion and propagates it to every place above the base place in a finite Galois extension.

Imports4
Imported by12

Declarations

def

chosenFinitePlaceTargetIntegralUniformizer

L40 ↗
Documentation

The actual image of the chosen global integral uniformizer in the integer ring of the chosen localized completion.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
def chosenFinitePlaceTargetIntegralUniformizer
    (v : HeightOneSpectrum (𝓞 K)) :
    𝒪[ChosenFinitePlaceLocalizedCompletion
      (K := K) (L := L) v]
theorem

chosenFinitePlace_integralUniformizer_map_isUniformizer

L53 ↗
Documentation

In an unramified chosen localized completion, the canonical global integral uniformizer remains a uniformizer after scalar extension.

Source context 9 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField L] in
Lean source · statement
theorem chosenFinitePlace_integralUniformizer_map_isUniformizer
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    (ValuativeRel.valuation
      (ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v)).IsUniformizer
      ((chosenFinitePlaceTargetIntegralUniformizer
          (K := K) (L := L) v :
        𝒪[ChosenFinitePlaceLocalizedCompletion
          (K := K) (L := L) v]) :
        ChosenFinitePlaceLocalizedCompletion
          (K := K) (L := L) v)
theorem

finitePlaceExtensionCentre_ramificationIdx'_eq_one_of_chosenFinitePlaceIsUnramified

L128 ↗
Documentation

Completed unramifiedness forces ramification index one at the actual global centre of the chosen finite-place extension.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    finitePlaceExtensionCentre_ramificationIdx'_eq_one_of_chosenFinitePlaceIsUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    v.asIdeal.ramificationIdx'
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal =
      1
theorem

isUnramifiedAt_of_chosenFinitePlaceIsUnramified

L305 ↗
Documentation

Unramifiedness of the actual chosen localized completion forces ideal-theoretic unramifiedness at its global centre.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem isUnramifiedAt_of_chosenFinitePlaceIsUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    Algebra.IsUnramifiedAt (𝓞 K)
      (finitePlaceExtensionCentre
        (K := K) (L := L) v
        (chosenFinitePlaceExtension (L := L) v)).asIdeal
theorem

isUnramifiedAt_at_finitePlaceAbove_of_chosenFinitePlaceIsUnramified

L341 ↗
Documentation

In a finite Galois number-field extension, completed unramifiedness at the chosen place implies ideal-theoretic unramifiedness at every finite place above the same base place.

Source context 8 commands

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

open scoped NumberField NNReal ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open LocalClassFieldTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem
    isUnramifiedAt_at_finitePlaceAbove_of_chosenFinitePlaceIsUnramified
    (v : HeightOneSpectrum (𝓞 K))
    (P : HeightOneSpectrum (𝓞 L))
    (hP : finitePlaceBelow (K := K) P = v)
    (hunram :
      ChosenFinitePlaceIsUnramified
        (K := K) (L := L) v) :
    Algebra.IsUnramifiedAt (𝓞 K) P.asIdeal

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