Module

AlgEquivTopology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquivTopology

1 declaration indexed from sourceView source ↗

Module documentation

Local continuity for transport under a number-field equivalence

The finite-completion map used by adeleCongr is continuous. This is the local continuity input for transporting the restricted-product topology.

Imports2

Imported by3

theorem

finitePlaceAdicCompletionCongrHom_continuous

L29 ↗

Documentation

Field-isomorphism transport is continuous on each finite completion.

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] [Algebra ℚ K]
  [Field M] [NumberField M] [Algebra ℚ M]

Lean source · statement

theorem finitePlaceAdicCompletionCongrHom_continuous
    (e : K ≃ₐ[ℚ] M) (W : HeightOneSpectrum (𝓞 M)) :
    Continuous (finitePlaceAdicCompletionCongrHom e W)

Module documentation

Local continuity for transport under a number-field equivalence

Declarations

finitePlaceAdicCompletionCongrHom_continuous