NYLL
Module

AdicCompletionMap.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.AdicCompletionMap
6 declarations indexed from sourceView source ↗

Module documentation

The canonical map between adic completions

A finite place above a base finite place determines the continuous extension of the number-field algebra map to their concrete adic completions.

Imports2
Imported by3

Declarations

def

finitePlaceAdicCompletionMap

L35 ↗
Documentation

The canonical map between adic completions at a finite place and a chosen place above it. It is obtained by completing the algebra map between the corresponding valued copies of the number fields.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
def finitePlaceAdicCompletionMap
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w}) :
    w.adicCompletion K →+* W.1.adicCompletion L
theorem

finitePlaceAdicCompletionMap_coe

L55 ↗
Documentation

On the dense copy of the base field, the canonical map of adic completions is the original field embedding.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem finitePlaceAdicCompletionMap_coe
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w})
    (x : K) :
    finitePlaceAdicCompletionMap K L w W
        (x : w.adicCompletion K) =
      (algebraMap K L x : W.1.adicCompletion L)
theorem

finitePlaceAdicCompletionMap_isScalarTower

L95 ↗
Documentation

The canonical map of adic completions is compatible with the original number-field tower.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · full declaration
theorem finitePlaceAdicCompletionMap_isScalarTower
    (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
    IsScalarTower K (w.adicCompletion K) (W.1.adicCompletion L) := by
  let : Algebra (w.adicCompletion K) (W.1.adicCompletion L) :=
    (finitePlaceAdicCompletionMap K L w W).toAlgebra
  apply IsScalarTower.of_algebraMap_eq
  intro x
  change
    (algebraMap K (W.1.adicCompletion L)) x =
      finitePlaceAdicCompletionMap K L w W
        (x : w.adicCompletion K)
  rw [finitePlaceAdicCompletionMap_coe K L w W x]
  exact IsScalarTower.algebraMap_apply K L (W.1.adicCompletion L) x
theorem

finitePlaceAdicCompletionMap_continuous

L114 ↗
Documentation

The canonical map between the two adic completions is continuous.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem finitePlaceAdicCompletionMap_continuous
    (w : HeightOneSpectrum (𝓞 K))
    (W : {W : HeightOneSpectrum (𝓞 L) //
      finitePlaceBelow (K := K) W = w}) :
    Continuous (finitePlaceAdicCompletionMap K L w W)
theorem

finitePlaceAdicCompletionMap_self_apply

L131 ↗
Documentation

The canonical map on a finite-place adic completion induced by the identity field extension is the identity map.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem finitePlaceAdicCompletionMap_self_apply
    (W : HeightOneSpectrum (𝓞 K))
    (x : W.adicCompletion K) :
    finitePlaceAdicCompletionMap K K W
        ⟨W, finitePlaceBelow_self W⟩ x =
      x
theorem

finitePlaceAdicCompletionMap_comp

L163 ↗
Documentation

Canonical maps between concrete adic completions compose in a number-field tower.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v w
variable
    (K : Type u) (L : Type v)
    [Field K] [NumberField K]
    [Field L] [NumberField L] [Algebra K L]
Lean source · statement
theorem finitePlaceAdicCompletionMap_comp
    {M : Type w}
    [Field M] [NumberField M]
    [Algebra K M] [Algebra M L]
    [IsScalarTower K M L]
    (vK : HeightOneSpectrum (𝓞 K))
    (vM : HeightOneSpectrum (𝓞 M))
    (vL : HeightOneSpectrum (𝓞 L))
    (hMK : finitePlaceBelow (K := K) vM = vK)
    (hLM : finitePlaceBelow (K := M) vL = vM)
    (hLK : finitePlaceBelow (K := K) vL = vK)
    (x : vK.adicCompletion K) :
    finitePlaceAdicCompletionMap M L vM ⟨vL, hLM⟩
        (finitePlaceAdicCompletionMap K M vK ⟨vM, hMK⟩ x) =
      finitePlaceAdicCompletionMap K L vK ⟨vL, hLK⟩ x

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