Module

Basic.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Basic

18 declarations indexed from sourceView source ↗

Module documentation

Ideles of a number field

This file defines the ideles of a number field.

The finite ideles are defined as the restricted product of the multiplicative groups of the finite completions with respect to the unit groups of their valuation rings. This is deliberately not the topology induced from the finite adele ring: the latter is not the idele topology. The infinite factor is the unit group of the finite product of the archimedean completions.

Imports3

Mathlib.NumberTheory.NumberField.AdeleRing
Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Mathlib.Topology.Algebra.Group.Units

Imported by6

abbrev

FiniteIdeleGroupOf

L34 ↗

Documentation

The finite idele group attached to a Dedekind domain and its fraction field. The number-field definition below specializes this to the ring of integers.

Source context 4 commands

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

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

Lean source · statement

abbrev FiniteIdeleGroupOf
    (R : Type*) [CommRing R] [IsDedekindDomain R]
    (F : Type*) [Field F] [Algebra R F] [IsFractionRing R F]

abbrev

FiniteIdeleGroup

L41 ↗

Documentation

The group of finite ideles of a number field.

Source context 4 commands

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

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

Lean source · statement

abbrev FiniteIdeleGroup

abbrev

InfiniteIdeleGroup

L45 ↗

Documentation

The product of the multiplicative groups of the archimedean completions.

Source context 4 commands

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

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

Lean source · statement

abbrev InfiniteIdeleGroup

abbrev

IdeleGroup

L49 ↗

Documentation

The idele group I_K.

Source context 4 commands

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

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

Lean source · statement

abbrev IdeleGroup

def

component

L57 ↗

FiniteIdeleGroup.component

Documentation

Evaluation of a finite idele at a finite place.

Source context 6 commands

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

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

Lean source · full declaration

def component (v : HeightOneSpectrum (𝓞 K)) :
    FiniteIdeleGroup K →* (v.adicCompletion K)ˣ where
  toFun a := a v
  map_one' := rfl
  map_mul' _ _ := rfl

theorem

component_apply

L64 ↗

FiniteIdeleGroup.component_apply

Source context 6 commands

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

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

Lean source · statement

theorem component_apply (a : FiniteIdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    component v a = a v

theorem

eventually_mem_localUnits

L71 ↗

FiniteIdeleGroup.eventually_mem_localUnits

Documentation

A finite idele is a local integral unit at all but finitely many finite places.

Source context 6 commands

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

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

Lean source · statement

theorem eventually_mem_localUnits (a : FiniteIdeleGroup K) :
    ∀ᶠ v in Filter.cofinite,
      a v ∈ (v.adicCompletionIntegers K).units

def

component

L83 ↗

InfiniteIdeleGroup.component

Documentation

The component of an infinite idele at an archimedean place.

Source context 6 commands

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

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

Lean source · statement

def component (v : InfinitePlace K) :
    InfiniteIdeleGroup K →* v.Completionˣ

theorem

component_apply

L90 ↗

InfiniteIdeleGroup.component_apply

Source context 7 commands

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

open scoped NumberField RestrictedProduct
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace InfiniteIdeleGroup
variable {K}
omit [NumberField K] in

Lean source · statement

theorem component_apply (a : InfiniteIdeleGroup K) (v : InfinitePlace K) :
    component v a = ContinuousMulEquiv.piUnits a v

def

finiteEquivFiniteAdeleUnitsOf

L102 ↗

IdeleGroup.finiteEquivFiniteAdeleUnitsOf

Documentation

Algebraically, the finite ideles over a Dedekind domain are the units of its finite adele ring.

Source context 6 commands

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

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

Lean source · statement

def finiteEquivFiniteAdeleUnitsOf
  (R : Type*) [CommRing R] [IsDedekindDomain R]
    (F : Type*) [Field F] [Algebra R F] [IsFractionRing R F] :
    FiniteIdeleGroupOf R F ≃*
    (IsDedekindDomain.FiniteAdeleRing R F)ˣ

def

infiniteComponent

L115 ↗

IdeleGroup.infiniteComponent

Documentation

The component of an idele at an archimedean place.

Source context 6 commands

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

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

Lean source · statement

def infiniteComponent (v : InfinitePlace K) :
    IdeleGroup K →* v.Completionˣ

def

finiteComponent

L120 ↗

IdeleGroup.finiteComponent

Documentation

The component of an idele at a finite place.

Source context 6 commands

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

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

Lean source · statement

def finiteComponent (v : HeightOneSpectrum (𝓞 K)) :
    IdeleGroup K →* (v.adicCompletion K)ˣ

theorem

infiniteComponent_apply

L125 ↗

IdeleGroup.infiniteComponent_apply

Source context 6 commands

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

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

Lean source · statement

theorem infiniteComponent_apply (a : IdeleGroup K) (v : InfinitePlace K) :
    infiniteComponent v a = ContinuousMulEquiv.piUnits a.1 v

theorem

finiteComponent_apply

L130 ↗

IdeleGroup.finiteComponent_apply

Source context 6 commands

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

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

Lean source · statement

theorem finiteComponent_apply (a : IdeleGroup K)
    (v : HeightOneSpectrum (𝓞 K)) :
    finiteComponent v a = a.2 v

def

finiteEquivFiniteAdeleUnits

L138 ↗

IdeleGroup.finiteEquivFiniteAdeleUnits

Documentation

Algebraically, the finite ideles are the units of the finite adele ring. The topology on the left is the restricted-product topology and is not transported through this equivalence.

Source context 6 commands

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

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

Lean source · statement

def finiteEquivFiniteAdeleUnits :
    FiniteIdeleGroup K ≃*
      (IsDedekindDomain.FiniteAdeleRing (𝓞 K) K)ˣ

def

equivAdeleRingUnits

L148 ↗

IdeleGroup.equivAdeleRingUnits

Documentation

Algebraically, the idele group is the unit group of the adele ring.

This is only a multiplicative equivalence. It is intentionally not stated as a homeomorphism because the idele topology is finer than the topology induced from the adele ring.

Source context 6 commands

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

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

Lean source · statement

def equivAdeleRingUnits :
    IdeleGroup K ≃* (NumberField.AdeleRing (𝓞 K) K)ˣ

theorem

equivAdeleRingUnits_fst

L155 ↗

IdeleGroup.equivAdeleRingUnits_fst

Source context 6 commands

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

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

Lean source · statement

theorem equivAdeleRingUnits_fst (a : IdeleGroup K) :
    (MulEquiv.prodUnits (equivAdeleRingUnits a)).1 = a.1

theorem

equivAdeleRingUnits_snd

L160 ↗

IdeleGroup.equivAdeleRingUnits_snd

Source context 6 commands

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

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

Lean source · statement

theorem equivAdeleRingUnits_snd (a : IdeleGroup K) :
    (MulEquiv.prodUnits (equivAdeleRingUnits a)).2 =
      finiteEquivFiniteAdeleUnits (K := K) a.2

Module documentation

Ideles of a number field

Declarations