Module

AlgEquivAdeleTopology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquivAdeleTopology

1 declaration indexed from sourceView source ↗

Module documentation

Continuity of adelic transport under a number-field equivalence

The archimedean factor is a product of continuous completion maps. The finite factor is a continuous map of restricted products because each completion map preserves the local valuation subring.

Imports2

Imported by2

theorem

continuous_adeleCongr

L30 ↗

Documentation

The existing algebraic transport of adeles is continuous.

Source context 5 commands

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

open scoped NumberField RestrictedProduct
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 continuous_adeleCongr (e : K ≃ₐ[ℚ] M) :
    Continuous (adeleCongr e)

Module documentation

Continuity of adelic transport under a number-field equivalence

Declarations

continuous_adeleCongr