Module

IdealToCompletion.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.UnramifiedComparison.IdealToCompletion

9 declarations indexed from sourceView source ↗

Module documentation

From ideal-theoretic to completed unramifiedness

This file proves that ideal-theoretic unramifiedness at the centre of the actual chosen finite-place extension implies unramifiedness of its localized completion.

Imports3

Imported by17

structure

FinitePlaceCompletionIntegralUniformizer

L39 ↗

Documentation

A uniformizer of a finite-place completion induced by an element of the global integer ring, together with its valuation and comparison properties.

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 · full declaration

structure FinitePlaceCompletionIntegralUniformizer
    {F : Type} [Field F] [NumberField F]
    (v : HeightOneSpectrum (𝓞 F)) where
  /-- The inducing element of the global integer ring. -/
  integer : 𝓞 F
  /-- The corresponding element of the completion integer ring. -/
  completionInteger :
    𝒪[ChosenFinitePlaceBaseCompletion (K := F) v]
  /-- The inducing global integer has normalized valuation `-1`. -/
  intValuation_eq_exp_neg_one :
    v.intValuation integer = WithZero.exp (-1 : ℤ)
  /-- The completion element is the image of the global integer. -/
  coe_completionInteger :
    (completionInteger :
        ChosenFinitePlaceBaseCompletion (K := F) v) =
      algebraMap F
        (ChosenFinitePlaceBaseCompletion (K := F) v)
        (integer : F)
  /-- The completion element is a uniformizer for the intrinsic valuation. -/
  completionInteger_isUniformizer :
    (ValuativeRel.valuation
        (ChosenFinitePlaceBaseCompletion (K := F) v)).IsUniformizer
      (completionInteger :
        ChosenFinitePlaceBaseCompletion (K := F) v)
  /-- The completion element lies in the completion's maximal ideal. -/
  completionInteger_mem_maximalIdeal :
    completionInteger ∈
      (𝓂[ChosenFinitePlaceBaseCompletion (K := F) v] :
        Ideal
          𝒪[ChosenFinitePlaceBaseCompletion (K := F) v])

def

chosenFinitePlaceCompletionIntegralUniformizer

L72 ↗

Documentation

A chosen global integral uniformizer and its image in a finite-place 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 chosenFinitePlaceCompletionIntegralUniformizer
    {F : Type} [Field F] [NumberField F]
    (v : HeightOneSpectrum (𝓞 F)) :
    FinitePlaceCompletionIntegralUniformizer v

theorem

chosenFinitePlace_integral_uniformizer_not_mem_maximalIdeal_sq

L193 ↗

Documentation

If the centre of the chosen finite-place extension has ramification index one, a global integral uniformizer remains a uniformizer after passing to the chosen localized completion. In particular it is not in the square of the target maximal ideal.

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 chosenFinitePlace_integral_uniformizer_not_mem_maximalIdeal_sq
    (v : HeightOneSpectrum (𝓞 K))
    (π : 𝓞 K)
    (πBase :
      𝒪[ChosenFinitePlaceBaseCompletion (K := K) v])
    (hπ :
      v.intValuation π = WithZero.exp (-1 : ℤ))
    (hπBase :
      (πBase :
          ChosenFinitePlaceBaseCompletion (K := K) v) =
        algebraMap K
          (ChosenFinitePlaceBaseCompletion (K := K) v)
          (π : K))
    (hglobal :
      v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal =
        1) :
    algebraMap
        𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]
        𝒪[ChosenFinitePlaceLocalizedCompletion
          (K := K) (L := L) v] πBase ∉
      (𝓂[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v] :
          Ideal
            𝒪[ChosenFinitePlaceLocalizedCompletion
              (K := K) (L := L) v]) ^ 2

theorem

chosenFinitePlace_maximalIdeal_map_not_le_sq_of_centre_ramificationIdx_eq_one

L317 ↗

Documentation

Ramification index one at the global centre prevents the image of the completed base maximal ideal from lying in the square of the target maximal ideal.

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 chosenFinitePlace_maximalIdeal_map_not_le_sq_of_centre_ramificationIdx_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hglobal :
      v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal =
        1) :
    ¬ (𝓂[ChosenFinitePlaceBaseCompletion (K := K) v] :
          Ideal
            𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]).map
        (algebraMap
          𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]
          𝒪[ChosenFinitePlaceLocalizedCompletion
            (K := K) (L := L) v]) ≤
      (𝓂[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v] :
          Ideal
            𝒪[ChosenFinitePlaceLocalizedCompletion
              (K := K) (L := L) v]) ^ 2

theorem

chosenFinitePlace_maximalIdeal_ramificationIdx'_eq_one_of_centre_ramificationIdx_eq_one

L357 ↗

Documentation

Ramification index one at the global centre gives ramification index one for the completed maximal ideals in the multiplicity formulation.

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 chosenFinitePlace_maximalIdeal_ramificationIdx'_eq_one_of_centre_ramificationIdx_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hglobal :
      v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal =
        1) :
    (𝓂[ChosenFinitePlaceBaseCompletion (K := K) v] :
        Ideal
          𝒪[ChosenFinitePlaceBaseCompletion (K := K) v]).ramificationIdx'
      (𝓂[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v] :
          Ideal
            𝒪[ChosenFinitePlaceLocalizedCompletion
              (K := K) (L := L) v]) =
      1

theorem

finitePlaceExtensionCentre_ramificationIdx_eq_one_of_isUnramifiedAt

L401 ↗

Documentation

Ideal-theoretic unramifiedness gives ramification index one at the actual centre of the chosen finite-place 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 [FiniteDimensional K L] in

Lean source · statement

theorem finitePlaceExtensionCentre_ramificationIdx_eq_one_of_isUnramifiedAt
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      Algebra.IsUnramifiedAt (𝓞 K)
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal) :
    v.asIdeal.ramificationIdx'
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal =
      1

theorem

chosenFinitePlace_maximalIdeal_ramificationIdx_eq_one_of_centre_ramificationIdx_eq_one

L428 ↗

Documentation

Ramification index one at the actual global centre gives ramification index one for the maximal ideals of the corresponding completed valued-field 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 chosenFinitePlace_maximalIdeal_ramificationIdx_eq_one_of_centre_ramificationIdx_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hglobal :
      v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal =
        1) :
    (𝓂[ChosenFinitePlaceLocalizedCompletion
        (K := K) (L := L) v] :
          Ideal
            𝒪[ChosenFinitePlaceLocalizedCompletion
              (K := K) (L := L) v]).ramificationIdx
        𝒪[ChosenFinitePlaceBaseCompletion (K := K) v] =
      1

theorem

chosenFinitePlaceIsUnramified_of_centre_ramificationIdx_eq_one

L480 ↗

Documentation

Ramification index one at the actual global centre implies unramifiedness of the corresponding completed valued-field 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 chosenFinitePlaceIsUnramified_of_centre_ramificationIdx_eq_one
    (v : HeightOneSpectrum (𝓞 K))
    (hglobal :
      v.asIdeal.ramificationIdx'
          (finitePlaceExtensionCentre
            (K := K) (L := L) v
            (chosenFinitePlaceExtension (L := L) v)).asIdeal =
        1) :
    ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v

theorem

chosenFinitePlaceIsUnramified_of_isUnramifiedAt

L504 ↗

Documentation

Algebraic unramifiedness of the centre of the chosen extension implies unramifiedness of the corresponding completed valued-field 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 chosenFinitePlaceIsUnramified_of_isUnramifiedAt
    (v : HeightOneSpectrum (𝓞 K))
    (hunram :
      Algebra.IsUnramifiedAt (𝓞 K)
        (finitePlaceExtensionCentre
          (K := K) (L := L) v
          (chosenFinitePlaceExtension (L := L) v)).asIdeal) :
    ChosenFinitePlaceIsUnramified
      (K := K) (L := L) v

Module documentation

From ideal-theoretic to completed unramifiedness

Declarations