Module

FinitePlaceAdicCompletionCongrEquiv.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Completion.FinitePlaceAdicCompletionCongrEquiv

1 declaration indexed from sourceView source ↗

Module documentation

Adic completions under a number-field equivalence

The existing continuous maps of adic completions along an equivalence of number fields are mutual inverses. This bundles them as a field equivalence for transporting local Hilbert pairings.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquiv

Imported by3

def

finitePlaceAdicCompletionCongrEquiv

L29 ↗

Documentation

The finite completion at corresponding places, viewed as a field equivalence rather than merely a continuous 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
variable {K : Type u} {M : Type v}
  [Field K] [NumberField K] [Field M] [NumberField M]

Lean source · statement

def finitePlaceAdicCompletionCongrEquiv
    (e : K ≃ₐ[ℚ] M) (W : HeightOneSpectrum (𝓞 M)) :
    ((finitePlaceCongr e).symm W).adicCompletion K ≃+*
      W.adicCompletion M

Module documentation

Adic completions under a number-field equivalence

Declarations

finitePlaceAdicCompletionCongrEquiv