Module

PrincipalTopology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PrincipalTopology

7 declarations indexed from sourceView source ↗

Module documentation

The topology of the principal ideles

This file proves that the principal ideles form a discrete, and hence closed, subgroup of the idele group.

The proof uses the same arithmetic separation as the classical argument. The finite-place condition forces a principal idele into the ring of integers. Its infinite component then lies in the Minkowski integer lattice, whose topology is discrete.

Imports3

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.Core
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SPlaces
Mathlib.Topology.Algebra.IsUniformGroup.Basic

Imported by4

def

infiniteMixedEmbedding

L36 ↗

IdeleGroup.infiniteMixedEmbedding

Documentation

The infinite component of an idele, written in Minkowski space.

Source context 5 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

Lean source · statement

def infiniteMixedEmbedding (a : IdeleGroup K) :
    NumberField.mixedEmbedding.mixedSpace K

theorem

continuous_infiniteMixedEmbedding

L41 ↗

IdeleGroup.continuous_infiniteMixedEmbedding

Source context 5 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

Lean source · statement

theorem continuous_infiniteMixedEmbedding :
    Continuous (infiniteMixedEmbedding (K := K))

theorem

infiniteMixedEmbedding_principal

L81 ↗

IdeleGroup.infiniteMixedEmbedding_principal

Source context 5 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

Lean source · statement

theorem infiniteMixedEmbedding_principal (x : Kˣ) :
    infiniteMixedEmbedding (principalIdele K x) =
      NumberField.mixedEmbedding K (x : K)

theorem

mixedEmbedding_one_mem_integerLattice

L89 ↗

IdeleGroup.mixedEmbedding_one_mem_integerLattice

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
omit [NumberField K] in

Lean source · statement

theorem mixedEmbedding_one_mem_integerLattice :
    NumberField.mixedEmbedding K (1 : K) ∈
      NumberField.mixedEmbedding.integerLattice K

theorem

principal_infiniteMixedEmbedding_mem_integerLattice

L98 ↗

IdeleGroup.principal_infiniteMixedEmbedding_mem_integerLattice

Documentation

A principal idele that is a unit at every finite place has infinite component in the Minkowski integer lattice.

Source context 5 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

Lean source · statement

theorem principal_infiniteMixedEmbedding_mem_integerLattice
    (x : Kˣ)
    (hx : principalIdele K x ∈
      integralAtFinitePlaces (K := K)) :
    infiniteMixedEmbedding (principalIdele K x) ∈
      NumberField.mixedEmbedding.integerLattice K

instance

principalSubgroupDiscreteTopology

L135 ↗

IdeleGroup.principalSubgroupDiscreteTopology

Documentation

The principal ideles have the discrete subspace topology.

Source context 5 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

Lean source · statement

instance principalSubgroupDiscreteTopology :
    DiscreteTopology (principalSubgroup K)

theorem

principalSubgroup_isClosed

L223 ↗

IdeleGroup.principalSubgroup_isClosed

Documentation

The principal ideles form a closed subgroup.

Source context 5 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

Lean source · statement

theorem principalSubgroup_isClosed :
    IsClosed
      ((principalSubgroup K :
        Subgroup (IdeleGroup K)) : Set (IdeleGroup K))

Module documentation

The topology of the principal ideles

Declarations

infiniteMixedEmbedding

continuous_infiniteMixedEmbedding

infiniteMixedEmbedding_principal

mixedEmbedding_one_mem_integerLattice

principal_infiniteMixedEmbedding_mem_integerLattice

principalSubgroupDiscreteTopology

principalSubgroup_isClosed