Module

InfiniteAlgEquiv.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.InfiniteAlgEquiv

5 declarations indexed from sourceView source ↗

Module documentation

Infinite completions under a number-field equivalence

The completion maps along an isomorphism of number fields are mutually inverse. This is the archimedean local input for the topology of adeleCongr.

Imports2

Imported by2

def

infinitePlaceCompletionCongrHom

L29 ↗

Documentation

The map between the completions at corresponding infinite places.

Source context 5 commands

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

open scoped NumberField TensorProduct
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 infinitePlaceCompletionCongrHom
    (e : K ≃ₐ[ℚ] M) (W : InfinitePlace M) :
    ((ClassFieldTheory.infinitePlaceEquivOfRingEquiv e.toRingEquiv).symm W).Completion →+*
      W.Completion

theorem

infinitePlaceCompletionCongrHom_continuous

L43 ↗

Documentation

The archimedean completion map is continuous.

Source context 5 commands

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

open scoped NumberField TensorProduct
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 infinitePlaceCompletionCongrHom_continuous
    (e : K ≃ₐ[ℚ] M) (W : InfinitePlace M) :
    Continuous (infinitePlaceCompletionCongrHom e W)

def

infinitePlaceCompletionCongrEquiv

L58 ↗

Documentation

Transport along a field isomorphism is an equivalence of the corresponding infinite-place completions.

Source context 5 commands

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

open scoped NumberField TensorProduct
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 infinitePlaceCompletionCongrEquiv
    (e : K ≃ₐ[ℚ] M) (W : InfinitePlace M) :
    ((ClassFieldTheory.infinitePlaceEquivOfRingEquiv e.toRingEquiv).symm W).Completion ≃+*
      W.Completion

theorem

infinitePlaceCompletionCongrHom_algebraMap

L125 ↗

Documentation

The completion map agrees with the number-field equivalence on elements of the number field.

Source context 5 commands

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

open scoped NumberField TensorProduct
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 infinitePlaceCompletionCongrHom_algebraMap
    (e : K ≃ₐ[ℚ] M) (W : InfinitePlace M) (x : K) :
    infinitePlaceCompletionCongrHom e W
        (algebraMap K
          ((ClassFieldTheory.infinitePlaceEquivOfRingEquiv e.toRingEquiv).symm W).Completion x) =
      algebraMap M W.Completion (e x)

theorem

adeleCongr_infiniteComponent

L152 ↗

Documentation

On infinite coordinates, adeleCongr is the completion map at the corresponding infinite place.

Source context 5 commands

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

open scoped NumberField TensorProduct
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_infiniteComponent
    (e : K ≃ₐ[ℚ] M)
    (a : NumberField.AdeleRing (𝓞 K) K)
    (W : InfinitePlace M) :
    (adeleCongr e a).1 W =
      infinitePlaceCompletionCongrHom e W
        (a.1 ((ClassFieldTheory.infinitePlaceEquivOfRingEquiv e.toRingEquiv).symm W))

Module documentation

Infinite completions under a number-field equivalence

Declarations

infinitePlaceCompletionCongrHom

infinitePlaceCompletionCongrHom_continuous

infinitePlaceCompletionCongrEquiv

infinitePlaceCompletionCongrHom_algebraMap

adeleCongr_infiniteComponent