Module

Topology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Topology

12 declarations indexed from sourceView source ↗

Module documentation

The idele topology

The idele group I_K carries the restricted-product topology. This file records the topological-group structure and the continuity of every local component map.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Basic

Imported by6

theorem

isOpen_finiteLocalUnits

L27 ↗

Documentation

The local integral-unit subgroup is open in the multiplicative group of a finite completion.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

theorem isOpen_finiteLocalUnits (v : HeightOneSpectrum (𝓞 K)) :
    IsOpen
      ((v.adicCompletionIntegers K).units :
        Set (v.adicCompletion K)ˣ)

instance

finiteLocalUnitsOpen

L33 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance finiteLocalUnitsOpen :
    Fact (∀ v : HeightOneSpectrum (𝓞 K),
      IsOpen
        ((v.adicCompletionIntegers K).units :
          Set (v.adicCompletion K)ˣ))

instance

finiteIdeleGroupIsTopologicalGroup

L40 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance finiteIdeleGroupIsTopologicalGroup :
    IsTopologicalGroup (FiniteIdeleGroup K)

instance

ideleGroupIsTopologicalGroup

L44 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance ideleGroupIsTopologicalGroup :
    IsTopologicalGroup (IdeleGroup K)

instance

finiteIdeleGroupT2Space

L48 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance finiteIdeleGroupT2Space :
    T2Space (FiniteIdeleGroup K)

instance

infiniteAdeleRingT2Space

L52 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance infiniteAdeleRingT2Space :
    T2Space (NumberField.InfiniteAdeleRing K)

instance

infiniteIdeleGroupT2Space

L57 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance infiniteIdeleGroupT2Space :
    T2Space (InfiniteIdeleGroup K)

instance

ideleGroupT2Space

L61 ↗

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]

Lean source · statement

instance ideleGroupT2Space :
    T2Space (IdeleGroup K)

def

infiniteComponentContinuous

L70 ↗

IdeleGroup.infiniteComponentContinuous

Documentation

Evaluation at an archimedean place is a continuous homomorphism.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace IdeleGroup
variable {K}

Lean source · full declaration

def infiniteComponentContinuous (v : InfinitePlace K) :
    IdeleGroup K →ₜ* v.Completionˣ where
  __ := infiniteComponent v
  continuous_toFun :=
    (continuous_apply v).comp
      (ContinuousMulEquiv.piUnits.continuous.comp continuous_fst)

def

finiteComponentContinuous

L78 ↗

IdeleGroup.finiteComponentContinuous

Documentation

Evaluation at a finite place is a continuous homomorphism.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace IdeleGroup
variable {K}

Lean source · full declaration

def finiteComponentContinuous (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup K →ₜ* (v.adicCompletion K)ˣ where
  __ := finiteComponent v
  continuous_toFun :=
    (RestrictedProduct.continuous_eval v).comp continuous_snd

theorem

infiniteComponentContinuous_apply

L85 ↗

IdeleGroup.infiniteComponentContinuous_apply

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace IdeleGroup
variable {K}

Lean source · statement

theorem infiniteComponentContinuous_apply
    (a : IdeleGroup K) (v : InfinitePlace K) :
    infiniteComponentContinuous v a =
      ContinuousMulEquiv.piUnits a.1 v

theorem

finiteComponentContinuous_apply

L92 ↗

IdeleGroup.finiteComponentContinuous_apply

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace IdeleGroup
variable {K}

Lean source · statement

theorem finiteComponentContinuous_apply
    (a : IdeleGroup K) (v : HeightOneSpectrum (𝓞 K)) :
    finiteComponentContinuous v a = a.2 v

Module documentation

The idele topology

Declarations