NYLL
Module

AlgEquivIdeleClassTopology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.AlgEquivIdeleClassTopology
6 declarations indexed from sourceView source ↗

Module documentation

Idèle and idèle-class transport under a number-field equivalence

The continuous adele-ring transport induces continuous transport of units and then of the quotient by principal idèles. These topological equivalences have the previously defined algebraic maps as their underlying maps.

Imports4
Imported by2

Declarations

theorem

adeleCongr_symm

L32 ↗
Documentation

Reversing the field equivalence reverses the adelic transport.

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 adeleCongr_symm (e : K ≃ₐ[ℚ] M) :
    (adeleCongr e).symm = adeleCongr e.symm
def

adeleCongrContinuousMulEquiv

L37 ↗
Documentation

Adelic field-isomorphism transport is a topological group equivalence.

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
def adeleCongrContinuousMulEquiv (e : K ≃ₐ[ℚ] M) :
    NumberField.AdeleRing (𝓞 K) K ≃ₜ*
      NumberField.AdeleRing (𝓞 M) M
def

ideleCongrContinuousMulEquiv

L49 ↗
Documentation

The existing idèle transport is an equivalence of topological groups.

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
def ideleCongrContinuousMulEquiv (e : K ≃ₐ[ℚ] M) :
    IdeleGroup K ≃ₜ* IdeleGroup M
theorem

ideleCongrContinuousMulEquiv_apply

L57 ↗
Documentation

The topological and algebraic transports of idèles agree.

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 ideleCongrContinuousMulEquiv_apply
    (e : K ≃ₐ[ℚ] M) (a : IdeleGroup K) :
    ideleCongrContinuousMulEquiv e a = ideleCongr e a
def

ideleClassCongrContinuousMulEquiv

L64 ↗
Documentation

The existing idèle-class transport is an equivalence of topological groups.

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
def ideleClassCongrContinuousMulEquiv
    (e : K ≃ₐ[ℚ] M) :
    IdeleClassGroup K ≃ₜ* IdeleClassGroup M
theorem

ideleClassCongrContinuousMulEquiv_apply

L90 ↗
Documentation

The topological and algebraic transports of idèle classes agree.

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 ideleClassCongrContinuousMulEquiv_apply
    (e : K ≃ₐ[ℚ] M) (a : IdeleClassGroup K) :
    ideleClassCongrContinuousMulEquiv e a = ideleClassCongr e a

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