NYLL
Module

FinitePlaceDecompositionAdicEquiv.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceDecompositionAdicEquiv
11 declarations indexed from sourceView source ↗

Module documentation

The actual decomposition--adic Galois equivalence

The previously constructed forward map is conjugation by algebraic-closure equivalences. Its inverse is continuous by the same semilinear conjugation theorem; no compactness instance or new Galois structure is installed.

Imports2
Imported by3

Declarations

theorem

fieldAlgebra_isTorsionFree_forAdicEquiv

L26 ↗
ClassFieldTower.Martinet.Shafarevich.fieldAlgebra_isTorsionFree_forAdicEquiv
Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
theorem fieldAlgebra_isTorsionFree_forAdicEquiv
    {K L : Type} [Field K] [Field L] [Algebra K L] :
    Module.IsTorsionFree K L
instance

finitePlaceCompletionClosureSourceTorsionFree

L35 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionClosureSourceTorsionFree
Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
Lean source · statement
instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion)
instance

finitePlaceCompletionClosureTargetTorsionFree

L41 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionClosureTargetTorsionFree
Source context 5 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F))
def

finitePlaceCompletionAlgebraicClosureRingEquiv

L47 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAlgebraicClosureRingEquiv
Documentation

The actual algebraic-closure equivalence underlying the completion comparison.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
def finitePlaceCompletionAlgebraicClosureRingEquiv
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion ≃+*
      AlgebraicClosure (v.adicCompletion F)
theorem

finitePlaceCompletionAlgebraicClosureRingEquiv_algebraMap

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAlgebraicClosureRingEquiv_algebraMap
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
theorem finitePlaceCompletionAlgebraicClosureRingEquiv_algebraMap
    (v : HeightOneSpectrum (RingOfIntegers F))
    (x : (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :
    finitePlaceCompletionAlgebraicClosureRingEquiv F v (algebraMap _ _ x) =
      algebraMap (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F))
        (relativeFinitePlaceCompletionAlgEquiv v x)
def

finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv

L62 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv
Documentation

The completion-model comparison, with its explicit continuous inverse.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
def finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Field.absoluteGaloisGroup
        (NumberField.HeightOneSpectrum.adicAbv F v).Completion ≃ₜ*
      Field.absoluteGaloisGroup (v.adicCompletion F)
theorem

finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv_apply

L88 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv_apply
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
theorem finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv_apply
    (v : HeightOneSpectrum (RingOfIntegers F))
    (sigma : Field.absoluteGaloisGroup
      (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :
    finitePlaceCompletionAbsoluteGaloisContinuousMulEquiv F v sigma =
      finitePlaceCompletionAbsoluteGaloisSemilinearCongr F v sigma
theorem

finitePlaceCompletionAbsoluteGaloisSemilinearCongr_bijective

L95 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAbsoluteGaloisSemilinearCongr_bijective
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
theorem finitePlaceCompletionAbsoluteGaloisSemilinearCongr_bijective
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Function.Bijective (finitePlaceCompletionAbsoluteGaloisSemilinearCongr F v)
theorem

finitePlaceDecompositionToAdicAbsoluteGaloisGroup_bijective

L100 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionToAdicAbsoluteGaloisGroup_bijective
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
theorem finitePlaceDecompositionToAdicAbsoluteGaloisGroup_bijective
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Function.Bijective (finitePlaceDecompositionToAdicAbsoluteGaloisGroup F v)
def

finitePlaceDecompositionAdicContinuousMulEquiv

L108 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionAdicContinuousMulEquiv
Documentation

The actual algebraic-localization map is a topological equivalence, with the same forward map used by finite-place cohomology restriction.

Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
def finitePlaceDecompositionAdicContinuousMulEquiv
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v ≃ₜ*
      Field.absoluteGaloisGroup (v.adicCompletion F)
theorem

finitePlaceDecompositionAdicContinuousMulEquiv_apply

L115 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionAdicContinuousMulEquiv_apply
Source context 6 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField IsDedekindDomain
variable (F : Type) [Field F] [NumberField F]
local instance finitePlaceCompletionClosureSourceTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (NumberField.HeightOneSpectrum.adicAbv F v).Completion
      (AlgebraicClosure (NumberField.HeightOneSpectrum.adicAbv F v).Completion) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
local instance finitePlaceCompletionClosureTargetTorsionFree
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    Module.IsTorsionFree (v.adicCompletion F) (AlgebraicClosure (v.adicCompletion F)) :=
  fieldAlgebra_isTorsionFree_forAdicEquiv
Lean source · statement
theorem finitePlaceDecompositionAdicContinuousMulEquiv_apply
    (v : HeightOneSpectrum (RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceDecompositionAdicContinuousMulEquiv F v sigma =
      finitePlaceDecompositionToAdicAbsoluteGaloisGroup F v sigma

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