Module

LocallyCompact.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.LocallyCompact

8 declarations indexed from sourceView source ↗

Module documentation

Local compactness of the idele group

The topology on the finite ideles is the restricted-product topology from AlgebraicNumberTheory.Idele.Topology. We prove local compactness by showing that every finite completion is proper, that its integral unit group is compact, and then applying the restricted-product theorem.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.Topology
Mathlib.LinearAlgebra.FreeModule.IdealQuotient
Mathlib.Topology.Algebra.Valued.LocallyCompact

Imported by8

theorem

exists_ringOfIntegers_approximation

L30 ↗

Documentation

An element integral at a finite place can be approximated by an algebraic integer to positive valuation.

Source context 4 commands

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

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

Lean source · statement

theorem exists_ringOfIntegers_approximation
    (v : HeightOneSpectrum (𝓞 K)) (y : K)
    (hy : v.valuation K y ≤ 1) :
    ∃ r : 𝓞 K, v.valuation K (y - algebraMap (𝓞 K) K r) < 1

def

ringOfIntegersQuotientEquivAdicResidueField

L75 ↗

GlobalClassFieldTheory.ClassFieldAxiom.ringOfIntegersQuotientEquivAdicResidueField

Documentation

The residue field of the adic completion at v is the global ring-of-integers quotient by v.

Source context 7 commands

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

open scoped NumberField RestrictedProduct Valued
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
namespace GlobalClassFieldTheory.ClassFieldAxiom
universe u
variable {K : Type u} [Field K] [NumberField K]

Lean source · statement

def ringOfIntegersQuotientEquivAdicResidueField
    (v : HeightOneSpectrum (𝓞 K)) :
    (𝓞 K ⧸ v.asIdeal) ≃+*
      Valued.ResidueField (v.adicCompletion K)

theorem

finite_adicCompletion_residueField

L244 ↗

Documentation

The residue field of a number-field completion at a finite place is finite.

Source context 4 commands

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

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

Lean source · statement

theorem finite_adicCompletion_residueField
    (v : HeightOneSpectrum (𝓞 K)) :
    Finite (Valued.ResidueField (v.adicCompletion K))

instance

adicCompletionProperSpace

L256 ↗

Documentation

Every nonarchimedean completion of a number field is a proper metric space.

Source context 5 commands

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

open scoped NumberField RestrictedProduct Valued
open NumberField IsDedekindDomain
noncomputable section
variable (K : Type*) [Field K] [NumberField K]
open _root_.Valued.integer in

Lean source · statement

instance adicCompletionProperSpace
    (v : HeightOneSpectrum (𝓞 K)) :
    ProperSpace (v.adicCompletion K)

theorem

isCompact_finiteLocalUnits

L266 ↗

Documentation

The integral unit group in a finite completion is compact.

Source context 4 commands

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

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

Lean source · statement

theorem isCompact_finiteLocalUnits
    (v : HeightOneSpectrum (𝓞 K)) :
    IsCompact
      ((v.adicCompletionIntegers K).units :
        Set (v.adicCompletion K)ˣ)

instance

finiteIdeleGroupLocallyCompactSpace

L279 ↗

Documentation

The correctly topologized finite idele group is locally compact.

Source context 4 commands

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

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

Lean source · statement

instance finiteIdeleGroupLocallyCompactSpace :
    LocallyCompactSpace (FiniteIdeleGroup K)

instance

infiniteIdeleGroupLocallyCompactSpace

L286 ↗

Documentation

The archimedean factor of the idele group is locally compact.

Source context 4 commands

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

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

Lean source · statement

instance infiniteIdeleGroupLocallyCompactSpace :
    LocallyCompactSpace (InfiniteIdeleGroup K)

instance

ideleGroupLocallyCompactSpace

L292 ↗

Documentation

The idele group, with its restricted-product topology, is locally compact.

Source context 4 commands

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

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

Lean source · statement

instance ideleGroupLocallyCompactSpace :
    LocallyCompactSpace (IdeleGroup K)

Module documentation

Local compactness of the idele group

Declarations