Module

Localization.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.Localization

8 declarations indexed from sourceView source ↗

Module documentation

Localization of the relative integral lattice

Away from the finite exceptional set, this module compares the localized integer lattice with the integral closure and derives coordinatewise integrality after localization.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Adele.IntegralTensorSupport.Lattice

Imported by5

theorem

exists_notMem_smul_mem_scaledRelativeIntegerLattice

L37 ↗

Documentation

Uniform local denominator statement: outside the bad set a denominator avoiding the prime carries every algebraic integer into the scaled lattice.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem exists_notMem_smul_mem_scaledRelativeIntegerLattice
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L))
    (x : 𝓞 L) :
    ∃ d : 𝓞 K, d ∉ w.asIdeal ∧
      d • x ∈
        scaledRelativeIntegerLattice
          (K := K) (L := L)

abbrev

RelativeBaseIntegerLocalization

L54 ↗

Documentation

The local ring of K at a finite place.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

abbrev RelativeBaseIntegerLocalization
    (w : HeightOneSpectrum (𝓞 K))

abbrev

RelativeExtensionIntegerLocalization

L59 ↗

Documentation

The localization of 𝓞 L above the same finite place of K.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

abbrev RelativeExtensionIntegerLocalization
    (w : HeightOneSpectrum (𝓞 K))

def

relativeIntegerLocalizationLinearMap

L66 ↗

Documentation

The canonical localization map, regarded as an 𝓞 K-linear map.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def relativeIntegerLocalizationLinearMap
    (w : HeightOneSpectrum (𝓞 K)) :
    𝓞 L →ₗ[𝓞 K]
      RelativeExtensionIntegerLocalization
        (K := K) (L := L) w

def

localizedScaledRelativeIntegerLattice

L78 ↗

Documentation

The span of the scaled integral relative basis after localization at a finite place of K.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

def localizedScaledRelativeIntegerLattice
    (w : HeightOneSpectrum (𝓞 K)) :
    Submodule
      (RelativeBaseIntegerLocalization (K := K) w)
      (RelativeExtensionIntegerLocalization
        (K := K) (L := L) w)

theorem

relativeIntegerLocalizationLinearMap_mem_localizedLattice

L96 ↗

Documentation

Every element of the global scaled lattice maps into its localized span.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem relativeIntegerLocalizationLinearMap_mem_localizedLattice
    (w : HeightOneSpectrum (𝓞 K))
    {x : 𝓞 L}
    (hx : x ∈
      scaledRelativeIntegerLattice
        (K := K) (L := L)) :
    relativeIntegerLocalizationLinearMap
        (K := K) (L := L) w x ∈
      localizedScaledRelativeIntegerLattice
        (K := K) (L := L) w

theorem

algebraMap_mem_localizedScaledRelativeIntegerLattice_of_notMem

L130 ↗

Documentation

Away from the finite bad set, every algebraic integer of L maps into the span of the scaled relative integral basis.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem algebraMap_mem_localizedScaledRelativeIntegerLattice_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L))
    (x : 𝓞 L) :
    algebraMap (𝓞 L)
        (RelativeExtensionIntegerLocalization
          (K := K) (L := L) w) x ∈
      localizedScaledRelativeIntegerLattice
        (K := K) (L := L) w

theorem

localizedScaledRelativeIntegerLattice_eq_top_of_notMem

L190 ↗

Documentation

Outside the explicitly constructed finite set of bad places, the localized scaled lattice is the whole localization of 𝓞 L.

Source context 6 commands

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

open scoped NumberField TensorProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
universe u v
variable
    {K : Type u} {L : Type v}
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
    [FiniteDimensional K L]

Lean source · statement

theorem localizedScaledRelativeIntegerLattice_eq_top_of_notMem
    (w : HeightOneSpectrum (𝓞 K))
    (hw : w ∉ integralTensorBadPlaces
      (K := K) (L := L)) :
    localizedScaledRelativeIntegerLattice
        (K := K) (L := L) w = ⊤

Module documentation

Localization of the relative integral lattice

Declarations