Module

AdicCompletionComparison.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.AdicCompletionComparison

9 declarations indexed from sourceView source ↗

Module documentation

Comparing the exact-extension and concrete adic-completion maps

The completion map attached to an exact extension of a finite-place absolute value agrees with the canonical map between the concrete adic completions at the corresponding finite places.

Imports9

Imported by8

def

finitePlaceExtensionAdicCompletionMap

L43 ↗

Documentation

The concrete homomorphism of adic completions associated with an exact extension of the normalized absolute value.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

def finitePlaceExtensionAdicCompletionMap
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    w.adicCompletion K →+*
      (finitePlaceExtensionCentre
        (K := K) (L := L) w a).adicCompletion L

theorem

finitePlaceExtensionAdicCompletionMap_coe

L58 ↗

Documentation

The exact-extension completion map agrees with the field embedding on elements of the base number field.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceExtensionAdicCompletionMap_coe
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : K) :
    finitePlaceExtensionAdicCompletionMap K L w a
        (x : w.adicCompletion K) =
      (algebraMap K L x :
        (finitePlaceExtensionCentre
          (K := K) (L := L) w a).adicCompletion L)

theorem

finitePlaceExtensionAdicCompletionMap_continuous

L94 ↗

Documentation

The completion map defined using an exact absolute-value extension is continuous.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceExtensionAdicCompletionMap_continuous
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L) :
    Continuous
      (finitePlaceExtensionAdicCompletionMap K L w a)

theorem

finitePlaceExtensionAdicCompletionMap_eq_finitePlaceAdicCompletionMap

L118 ↗

Documentation

The exact-extension construction and the canonical completion of the field embedding agree. Equality on the dense copy of K is extended by continuity.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceExtensionAdicCompletionMap_eq_finitePlaceAdicCompletionMap
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : w.adicCompletion K) :
    finitePlaceExtensionAdicCompletionMap K L w a x =
      finitePlaceAdicCompletionMap K L w
        (finitePlaceExtensionEquivAbove
          (K := K) (L := L) w a) x

theorem

finitePlaceAdicCompletionMap_moduleFinite

L182 ↗

Documentation

The concrete completion at a finite place above w is finite over the concrete completion at w, for the canonical completion map.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · full declaration

theorem finitePlaceAdicCompletionMap_moduleFinite
    [FiniteDimensional K L]
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w}) :
    letI : Algebra (w.adicCompletion K) (W.1.adicCompletion L) :=
      (finitePlaceAdicCompletionMap K L w W).toAlgebra
    Module.Finite (w.adicCompletion K) (W.1.adicCompletion L) := by
  classical
  obtain ⟨a, rfl⟩ :=
    (finitePlaceExtensionEquivAbove
      (K := K) (L := L) w).surjective W
  let vK := HeightOneSpectrum.adicAbv K w
  let hvK : vK.IsNontrivial :=
    RayClass.adicAbv_isNontrivial w
  let : Algebra
      (w.adicCompletion K)
      ((finitePlaceExtensionEquivAbove
        (K := K) (L := L) w a).1.adicCompletion L) :=
    (finitePlaceAdicCompletionMap K L w
      (finitePlaceExtensionEquivAbove
        (K := K) (L := L) w a)).toAlgebra
  let : Module
      (w.adicCompletion K)
      ((finitePlaceExtensionEquivAbove
        (K := K) (L := L) w a).1.adicCompletion L) :=
    Algebra.toModule
  let : Algebra (w.adicCompletion K) vK.Completion :=
    (relativeFinitePlaceCompletionAlgEquiv w).symm.toRingHom.toAlgebra
  let : Algebra vK.Completion a.1.Completion :=
    AbsoluteValue.completionAlgebra vK a.1 a.2
  let : Algebra (w.adicCompletion K) a.1.Completion :=
    ((algebraMap vK.Completion a.1.Completion).comp
      (relativeFinitePlaceCompletionAlgEquiv w).symm.toRingHom).toAlgebra
  let : IsScalarTower
      (w.adicCompletion K) vK.Completion a.1.Completion :=
    IsScalarTower.of_algebraMap_eq' rfl
  let : Module.Finite (w.adicCompletion K) vK.Completion :=
    Module.Finite.of_surjective
      (Algebra.linearMap (w.adicCompletion K) vK.Completion)
      (relativeFinitePlaceCompletionAlgEquiv w).symm.surjective
  let : Module.Finite vK.Completion a.1.Completion :=
    completionModuleFinite vK hvK a
  let : Module.Finite (w.adicCompletion K) a.1.Completion :=
    Module.Finite.trans vK.Completion a.1.Completion
  let e :
      a.1.Completion ≃ₐ[w.adicCompletion K]
        (finitePlaceExtensionEquivAbove
          (K := K) (L := L) w a).1.adicCompletion L :=
    { __ :=
        finitePlaceExtensionAdicCompletionRingEquiv
          (K := K) (L := L) w a
      commutes' := fun x => by
        change
          finitePlaceExtensionAdicCompletionMap K L w a x =
            finitePlaceAdicCompletionMap K L w
              (finitePlaceExtensionEquivAbove
                (K := K) (L := L) w a) x
        exact
          finitePlaceExtensionAdicCompletionMap_eq_finitePlaceAdicCompletionMap
            K L w a x }
  exact Module.Finite.equiv e.toLinearEquiv

theorem

finitePlaceExtensionAdicCompletionMap_norm

L247 ↗

Documentation

The norm of the image under the concrete adic-completion map is raised to the exact-extension exponent.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceExtensionAdicCompletionMap_norm
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : w.adicCompletion K) :
    ‖finitePlaceExtensionAdicCompletionMap K L w a x‖ =
      ‖x‖ ^ finitePlaceExtensionExponent
        (K := K) (L := L) w a

theorem

finitePlaceAdicCompletionMap_norm_le_one_iff

L273 ↗

Documentation

The canonical map between concrete adic completions preserves the valuation ring, expressed by the norm bound defining its unit ball.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceAdicCompletionMap_norm_le_one_iff
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : w.adicCompletion K) :
    ‖finitePlaceAdicCompletionMap K L w W x‖ ≤ 1 ↔
      ‖x‖ ≤ 1

theorem

finitePlaceExtensionAdicCompletionMap_valued

L301 ↗

Documentation

The valuation of the image under the concrete adic-completion map is multiplied by the ramification index. This extends the corresponding formula for elements of K to every element of the completion.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceExtensionAdicCompletionMap_valued
    (w : HeightOneSpectrum (𝓞 K))
    (a : AbsoluteValueExtension
      (HeightOneSpectrum.adicAbv K w) L)
    (x : w.adicCompletion K) :
    Valued.v (finitePlaceExtensionAdicCompletionMap K L w a x) =
      Valued.v x ^ w.asIdeal.ramificationIdx'
        (finitePlaceExtensionCentre
          (K := K) (L := L) w a).asIdeal

theorem

finitePlaceAdicCompletionMap_valued

L394 ↗

Documentation

Under the canonical map to a place above w, the completed valuation is raised to the ramification index.

Source context 6 commands

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

open scoped NumberField TensorProduct
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]

Lean source · statement

theorem finitePlaceAdicCompletionMap_valued
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : w.adicCompletion K) :
    Valued.v (finitePlaceAdicCompletionMap K L w W x) =
      Valued.v x ^ w.asIdeal.ramificationIdx' W.1.asIdeal

Module documentation

Comparing the exact-extension and concrete adic-completion maps

Declarations