Module

Topology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Topology

47 declarations indexed from sourceView source ↗

Module documentation

The congruence topology on the idele class group

The local higher-unit groups are open, the ray congruence subgroups are open (and hence closed) of finite index, and the congruence subgroups are cofinal among the closed finite-index subgroups of the idele class group.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.FullModulus
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.NormOneCompact
Mathlib.Analysis.Complex.Convex
Mathlib.Basic.Sign.Basic
Mathlib.Topology.Algebra.Ring.Compact
Mathlib.Topology.Connected.Clopen
Mathlib.Topology.Instances.Sign

Imported by16

def

localIntegralValue

L38 ↗

RayClass.localIntegralValue

Documentation

The integral representative of a unit in a finite completion.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def localIntegralValue
    (v : HeightOneSpectrum (𝓞 K))
    (y : (v.adicCompletionIntegers K).units) :
    v.adicCompletionIntegers K

theorem

localHigherUnitMap_eq_one_iff

L47 ↗

RayClass.localHigherUnitMap_eq_one_iff

Documentation

A local integral unit maps to one modulo the n-th maximal-ideal power exactly when its difference from one belongs to that power.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem localHigherUnitMap_eq_one_iff
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ)
    (y : (v.adicCompletionIntegers K).units) :
    localHigherUnitMap v n y = 1 ↔
      localIntegralValue v y - 1 ∈
          (IsLocalRing.maximalIdeal
            (v.adicCompletionIntegers K)) ^ n

theorem

localHigherUnitGroup_antitone

L69 ↗

RayClass.localHigherUnitGroup_antitone

Documentation

Local higher-unit groups are contravariant in their depth.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem localHigherUnitGroup_antitone
    (v : HeightOneSpectrum (𝓞 K))
    {m n : ℕ} (hmn : m ≤ n) :
    localHigherUnitGroup v n ≤ localHigherUnitGroup v m

theorem

isOpen_localHigherUnitGroup

L82 ↗

RayClass.isOpen_localHigherUnitGroup

Documentation

Every local higher-unit group is open in the multiplicative group of the finite completion.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isOpen_localHigherUnitGroup
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    IsOpen
      ((localHigherUnitGroup v n :
        Subgroup (v.adicCompletion K)ˣ) :
          Set (v.adicCompletion K)ˣ)

theorem

localHigherUnitGroup_le_finiteLocalUnits

L131 ↗

RayClass.localHigherUnitGroup_le_finiteLocalUnits

Documentation

The local higher-unit group lies in the local integral-unit group.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem localHigherUnitGroup_le_finiteLocalUnits
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    localHigherUnitGroup v n ≤
      (v.adicCompletionIntegers K).units

theorem

isOpen_finiteCongruenceSubgroup

L142 ↗

RayClass.isOpen_finiteCongruenceSubgroup

Documentation

The finite idele congruence subgroup is open.

Source context 7 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in

Lean source · statement

theorem isOpen_finiteCongruenceSubgroup (m : FiniteModulus K) :
    IsOpen
      ((finiteCongruenceSubgroup m :
        Subgroup (FiniteIdeleGroup K)) :
          Set (FiniteIdeleGroup K))

theorem

isOpen_infinitePositiveSubgroup

L203 ↗

RayClass.isOpen_infinitePositiveSubgroup

Documentation

At a real place the positivity subgroup is open; at a complex place it is the whole local multiplicative group.

Source context 8 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
omit [NumberField K] in

Lean source · statement

theorem isOpen_infinitePositiveSubgroup (v : InfinitePlace K) :
    IsOpen
      ((infinitePositiveSubgroup v : Subgroup v.Completionˣ) :
        Set v.Completionˣ)

theorem

isOpen_infinitePositivePiSubgroup

L233 ↗

RayClass.isOpen_infinitePositivePiSubgroup

Documentation

The positivity subgroup in the product of all infinite local groups is open.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · full declaration

theorem isOpen_infinitePositivePiSubgroup :
    IsOpen
      ((Subgroup.pi Set.univ (fun v : InfinitePlace K ↦
          infinitePositiveSubgroup v) :
        Subgroup ((v : InfinitePlace K) → v.Completionˣ)) :
          Set ((v : InfinitePlace K) → v.Completionˣ)) := by
  change IsOpen
    (Set.univ.pi fun v : InfinitePlace K ↦
      (infinitePositiveSubgroup v : Set v.Completionˣ))
  exact isOpen_set_pi Set.finite_univ fun v _ ↦
    isOpen_infinitePositiveSubgroup v

theorem

isOpen_narrowInfiniteCongruenceSubgroup

L246 ↗

RayClass.isOpen_narrowInfiniteCongruenceSubgroup

Documentation

The narrow archimedean congruence subgroup is open.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isOpen_narrowInfiniteCongruenceSubgroup :
    IsOpen
      ((narrowInfiniteCongruenceSubgroup (K := K) :
        Subgroup (InfiniteIdeleGroup K)) :
          Set (InfiniteIdeleGroup K))

theorem

isOpen_infiniteCongruenceSubgroup

L255 ↗

RayClass.isOpen_infiniteCongruenceSubgroup

Documentation

The archimedean congruence subgroup selected by a full modulus is open.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isOpen_infiniteCongruenceSubgroup (m : Modulus K) :
    IsOpen
      ((m.infiniteCongruenceSubgroup :
        Subgroup (InfiniteIdeleGroup K)) :
          Set (InfiniteIdeleGroup K))

theorem

isOpen_ideleCongruenceSubgroup

L289 ↗

RayClass.isOpen_ideleCongruenceSubgroup

Documentation

The idele congruence subgroup I_K^m is open.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isOpen_ideleCongruenceSubgroup (m : Modulus K) :
    IsOpen
      ((m.ideleCongruenceSubgroup :
        Subgroup (IdeleGroup K)) :
          Set (IdeleGroup K))

theorem

localHigherUnit_norm_sub_one_le

L299 ↗

RayClass.localHigherUnit_norm_sub_one_le

Documentation

Membership in the n-th local higher-unit group bounds the norm of the difference from one by the n-th power of a uniformizer norm.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem localHigherUnit_norm_sub_one_le
    (v : HeightOneSpectrum (𝓞 K))
    (ϖ : v.adicCompletionIntegers K) (hϖ : Irreducible ϖ)
    (n : ℕ) {x : (v.adicCompletion K)ˣ}
    (hx : x ∈ localHigherUnitGroup v n) :
    ‖(x : v.adicCompletion K) - 1‖ ≤ ‖ϖ‖ ^ n

theorem

local_irreducible_norm_lt_one

L366 ↗

RayClass.local_irreducible_norm_lt_one

Documentation

An irreducible element of the valuation ring of a finite completion has norm strictly less than one.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem local_irreducible_norm_lt_one
    (v : HeightOneSpectrum (𝓞 K))
    {ϖ : v.adicCompletionIntegers K} (hϖ : Irreducible ϖ) :
    ‖ϖ‖ < 1

theorem

exists_localHigherUnitGroup_subset

L380 ↗

RayClass.exists_localHigherUnitGroup_subset

Documentation

The higher-unit groups form a neighborhood basis of 1 in a finite local multiplicative group.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem exists_localHigherUnitGroup_subset
    (v : HeightOneSpectrum (𝓞 K))
    {U : Set (v.adicCompletion K)ˣ}
    (hU : U ∈ 𝓝 (1 : (v.adicCompletion K)ˣ)) :
    ∃ n : ℕ,
      (localHigherUnitGroup v n :
        Set (v.adicCompletion K)ˣ) ⊆ U

theorem

exists_finiteCongruenceSubgroup_subset

L427 ↗

RayClass.exists_finiteCongruenceSubgroup_subset

Documentation

Every identity neighborhood in the finite ideles contains a finite congruence subgroup.

Source context 7 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in

Lean source · statement

theorem exists_finiteCongruenceSubgroup_subset
    {U : Set (FiniteIdeleGroup K)}
    (hUopen : IsOpen U) (hUone : (1 : FiniteIdeleGroup K) ∈ U) :
    ∃ m : FiniteModulus K,
      (finiteCongruenceSubgroup m :
        Set (FiniteIdeleGroup K)) ⊆ U

def

realCompletionContinuousMulEquiv

L510 ↗

RayClass.realCompletionContinuousMulEquiv

Documentation

The multiplicative topological equivalence between a real infinite completion and ℝ.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · full declaration

def realCompletionContinuousMulEquiv
    (v : InfinitePlace K) (hv : v.IsReal) :
    v.Completion ≃ₜ* ℝ where
  __ :=
    (InfinitePlace.Completion.ringEquivRealOfIsReal hv).toMulEquiv
  continuous_toFun :=
    (InfinitePlace.Completion.isometryEquivRealOfIsReal hv).continuous
  continuous_invFun :=
    (InfinitePlace.Completion.isometryEquivRealOfIsReal hv).symm.continuous

def

complexCompletionContinuousMulEquiv

L522 ↗

RayClass.complexCompletionContinuousMulEquiv

Documentation

The multiplicative topological equivalence between a complex infinite completion and ℂ.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · full declaration

def complexCompletionContinuousMulEquiv
    (v : InfinitePlace K) (hv : v.IsComplex) :
    v.Completion ≃ₜ* ℂ where
  __ :=
    (InfinitePlace.Completion.ringEquivComplexOfIsComplex hv).toMulEquiv
  continuous_toFun :=
    (InfinitePlace.Completion.isometryEquivComplexOfIsComplex hv).continuous
  continuous_invFun :=
    (InfinitePlace.Completion.isometryEquivComplexOfIsComplex hv).symm.continuous

def

positiveRealUnit

L533 ↗

RayClass.positiveRealUnit

Documentation

A positive real number regarded as a unit.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def positiveRealUnit (x : Set.Ioi (0 : ℝ)) : ℝˣ

theorem

continuous_positiveRealUnit

L537 ↗

RayClass.continuous_positiveRealUnit

Documentation

The map from positive real numbers to real units is continuous.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem continuous_positiveRealUnit :
    Continuous positiveRealUnit

theorem

isConnected_infinitePositiveSubgroup

L553 ↗

RayClass.isConnected_infinitePositiveSubgroup

Documentation

The positive local multiplicative group at an infinite place is connected.

Source context 8 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
open scoped Classical in
omit [NumberField K] in

Lean source · statement

theorem isConnected_infinitePositiveSubgroup
    (v : InfinitePlace K) :
    IsConnected
      ((infinitePositiveSubgroup v : Subgroup v.Completionˣ) :
        Set v.Completionˣ)

theorem

isConnected_narrowInfiniteCongruenceSubgroup

L616 ↗

RayClass.isConnected_narrowInfiniteCongruenceSubgroup

Documentation

The narrow archimedean positivity subgroup is connected.

Source context 7 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
omit [NumberField K] in

Lean source · statement

theorem isConnected_narrowInfiniteCongruenceSubgroup :
    IsConnected
      ((narrowInfiniteCongruenceSubgroup (K := K) :
        Subgroup (InfiniteIdeleGroup K)) :
          Set (InfiniteIdeleGroup K))

def

realPlaceSign

L653 ↗

RayClass.realPlaceSign

Documentation

The sign of a unit at a real infinite place.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def realPlaceSign
    (v : {w : InfinitePlace K // w.IsReal}) :
    v.1.Completionˣ →* SignTypeˣ

def

infiniteSign

L662 ↗

RayClass.infiniteSign

Documentation

The tuple of signs of an infinite idele at all real places.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def infiniteSign :
    InfiniteIdeleGroup K →*
      ((v : {w : InfinitePlace K // w.IsReal}) → SignTypeˣ)

theorem

infiniteSign_ker_eq_narrowInfiniteCongruenceSubgroup

L671 ↗

RayClass.infiniteSign_ker_eq_narrowInfiniteCongruenceSubgroup

Documentation

Positivity at all real places is exactly the kernel of the infinite sign map.

Source context 7 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass
omit [NumberField K] in

Lean source · statement

theorem infiniteSign_ker_eq_narrowInfiniteCongruenceSubgroup :
    (infiniteSign (K := K)).ker =
      narrowInfiniteCongruenceSubgroup (K := K)

instance

narrowInfiniteCongruenceSubgroupFiniteIndex

L709 ↗

RayClass.narrowInfiniteCongruenceSubgroupFiniteIndex

Documentation

The infinite positivity subgroup has finite index (its quotient is detected by the finitely many real signs).

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance narrowInfiniteCongruenceSubgroupFiniteIndex :
    (narrowInfiniteCongruenceSubgroup (K := K)).FiniteIndex

instance

infiniteCongruenceSubgroupFiniteIndex

L716 ↗

RayClass.Modulus.infiniteCongruenceSubgroupFiniteIndex

Documentation

Every selected-real-place congruence subgroup has finite index, because it contains the narrow positivity subgroup.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance Modulus.infiniteCongruenceSubgroupFiniteIndex
    (m : Modulus K) :
    m.infiniteCongruenceSubgroup.FiniteIndex

theorem

finiteCongruenceSubgroup_le_integralSubgroup

L729 ↗

RayClass.finiteCongruenceSubgroup_le_integralSubgroup

Documentation

The finite idele congruence subgroup lies in the everywhere-integral finite ideles.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem finiteCongruenceSubgroup_le_integralSubgroup
    (m : FiniteModulus K) :
    finiteCongruenceSubgroup m ≤
      FiniteIdeleGroup.integralSubgroup (K := K)

instance

finiteCongruenceSubgroupFiniteRelIndex

L738 ↗

RayClass.finiteCongruenceSubgroupFiniteRelIndex

Documentation

Within the compact group of everywhere-integral finite ideles, every finite congruence subgroup has finite index.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance finiteCongruenceSubgroupFiniteRelIndex
    (m : FiniteModulus K) :
    (finiteCongruenceSubgroup m).IsFiniteRelIndex
      (FiniteIdeleGroup.integralSubgroup (K := K))

theorem

finiteCongruenceSubgroup_antitone

L759 ↗

RayClass.finiteCongruenceSubgroup_antitone

Documentation

Finite congruence subgroups are contravariant in the finite modulus.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem finiteCongruenceSubgroup_antitone
    {m n : FiniteModulus K} (hmn : m ≤ n) :
    finiteCongruenceSubgroup n ≤ finiteCongruenceSubgroup m

theorem

infiniteCongruenceSubgroup_antitone

L769 ↗

RayClass.Modulus.infiniteCongruenceSubgroup_antitone

Documentation

Infinite congruence subgroups are contravariant in the selected real places of a full modulus.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem Modulus.infiniteCongruenceSubgroup_antitone
    {m n : Modulus K} (hmn : m ≤ n) :
    n.infiniteCongruenceSubgroup ≤ m.infiniteCongruenceSubgroup

theorem

ideleCongruenceSubgroup_antitone

L778 ↗

RayClass.Modulus.ideleCongruenceSubgroup_antitone

Documentation

Idèle congruence subgroups are contravariant in a full modulus.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem Modulus.ideleCongruenceSubgroup_antitone
    {m n : Modulus K} (hmn : m ≤ n) :
    n.ideleCongruenceSubgroup ≤ m.ideleCongruenceSubgroup

theorem

congruenceSubgroup_antitone

L787 ↗

RayClass.Modulus.congruenceSubgroup_antitone

Documentation

Ray congruence subgroups are contravariant in a full modulus.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem Modulus.congruenceSubgroup_antitone
    {m n : Modulus K} (hmn : m ≤ n) :
    n.congruenceSubgroup ≤ m.congruenceSubgroup

def

integralIdeleEquiv

L798 ↗

RayClass.integralIdeleEquiv

Documentation

Ideles integral at all finite places split as the infinite ideles times the compact group of integral finite ideles.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · full declaration

def integralIdeleEquiv :
    IdeleGroup.integralAtFinitePlaces (K := K) ≃*
      InfiniteIdeleGroup K ×
        FiniteIdeleGroup.integralSubgroup (K := K) where
  toFun a := (a.1.1, ⟨a.1.2, a.2⟩)
  invFun a := ⟨(a.1, a.2.1), a.2.2⟩
  left_inv a := by
    apply Subtype.ext
    rfl
  right_inv a := rfl
  map_mul' a b := rfl

theorem

map_ideleCongruenceSubgroup_subgroupOf_integral

L812 ↗

RayClass.map_ideleCongruenceSubgroup_subgroupOf_integral

Documentation

Under integralIdeleEquiv, the idele congruence subgroup maps to the product of its infinite and finite congruence factors.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem map_ideleCongruenceSubgroup_subgroupOf_integral (m : Modulus K) :
    ((m.ideleCongruenceSubgroup).subgroupOf
      (IdeleGroup.integralAtFinitePlaces (K := K))).map
        (integralIdeleEquiv (K := K)).toMonoidHom =
      m.infiniteCongruenceSubgroup.prod
        ((finiteCongruenceSubgroup m.finitePart).subgroupOf
          (FiniteIdeleGroup.integralSubgroup (K := K)))

instance

ideleCongruenceSubgroupFiniteRelIndex

L828 ↗

RayClass.ideleCongruenceSubgroupFiniteRelIndex

Documentation

The idele congruence subgroup has finite relative index in the ideles which are integral at every finite place.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance ideleCongruenceSubgroupFiniteRelIndex
    (m : Modulus K) :
    m.ideleCongruenceSubgroup.IsFiniteRelIndex
      (IdeleGroup.integralAtFinitePlaces (K := K))

instance

ordinaryIdealClassSubgroupFiniteIndex

L856 ↗

RayClass.ordinaryIdealClassSubgroupFiniteIndex

Documentation

The subgroup defining the ordinary ideal class group has finite index.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance ordinaryIdealClassSubgroupFiniteIndex :
    (IdeleGroup.integralAtFinitePlaces (K := K) ⊔
      IdeleGroup.principalSubgroup K).FiniteIndex

instance

ideleCongruenceSupPrincipalFiniteIndex

L869 ↗

RayClass.ideleCongruenceSupPrincipalFiniteIndex

Documentation

The subgroup I_K^m Kˣ has finite index in the idele group.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance ideleCongruenceSupPrincipalFiniteIndex
    (m : Modulus K) :
    (m.ideleCongruenceSubgroup ⊔
      IdeleGroup.principalSubgroup K).FiniteIndex

theorem

isOpen_congruenceSubgroup

L903 ↗

RayClass.isOpen_congruenceSubgroup

Documentation

The ray congruence subgroup in the idele class group is open.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isOpen_congruenceSubgroup (m : Modulus K) :
    IsOpen
      ((m.congruenceSubgroup :
        Subgroup (IdeleClassGroup K)) :
          Set (IdeleClassGroup K))

theorem

isClosed_congruenceSubgroup

L918 ↗

RayClass.isClosed_congruenceSubgroup

Documentation

Every ray congruence subgroup is closed.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isClosed_congruenceSubgroup (m : Modulus K) :
    IsClosed
      ((m.congruenceSubgroup :
        Subgroup (IdeleClassGroup K)) :
          Set (IdeleClassGroup K))

instance

congruenceSubgroupFiniteIndex

L927 ↗

RayClass.congruenceSubgroupFiniteIndex

Documentation

Every ray congruence subgroup has finite index.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

instance congruenceSubgroupFiniteIndex (m : Modulus K) :
    m.congruenceSubgroup.FiniteIndex

theorem

narrowInfiniteCongruenceSubgroup_mapsTo_openSubgroup

L939 ↗

RayClass.narrowInfiniteCongruenceSubgroup_mapsTo_openSubgroup

Documentation

The image of the connected narrow archimedean positivity subgroup lies in every open subgroup of the idele class group.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem narrowInfiniteCongruenceSubgroup_mapsTo_openSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hH : IsOpen (H : Set (IdeleClassGroup K)))
    {a : InfiniteIdeleGroup K}
    (ha : a ∈ narrowInfiniteCongruenceSubgroup (K := K)) :
    (((a, (1 : FiniteIdeleGroup K)) : IdeleGroup K) :
      IdeleClassGroup K) ∈ H

theorem

exists_congruenceSubgroup_le_of_isOpen

L977 ↗

RayClass.exists_congruenceSubgroup_le_of_isOpen

Documentation

Congruence subgroups are cofinal among the open subgroups of the idele class group.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem exists_congruenceSubgroup_le_of_isOpen
    (H : Subgroup (IdeleClassGroup K))
    (hH : IsOpen (H : Set (IdeleClassGroup K))) :
    ∃ m : Modulus K, m.congruenceSubgroup ≤ H

def

chosenModulusInside

L1046 ↗

RayClass.chosenModulusInside

Documentation

A modulus whose ray congruence subgroup lies in the given open subgroup.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def chosenModulusInside
    (H : Subgroup (IdeleClassGroup K))
    (hH : IsOpen (H : Set (IdeleClassGroup K))) :
    Modulus K

theorem

chosenModulusInside_spec

L1055 ↗

RayClass.chosenModulusInside_spec

Documentation

The chosen modulus has the required subgroup inclusion.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem chosenModulusInside_spec
    (H : Subgroup (IdeleClassGroup K))
    (hH : IsOpen (H : Set (IdeleClassGroup K))) :
    (chosenModulusInside H hH).congruenceSubgroup ≤ H

def

modulusInsideClosedFiniteIndex

L1064 ↗

RayClass.modulusInsideClosedFiniteIndex

Documentation

Closed finite-index subgroups are open, hence also contain a chosen ray congruence subgroup.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

def modulusInsideClosedFiniteIndex
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    Modulus K

theorem

modulusInsideClosedFiniteIndex_spec

L1074 ↗

RayClass.modulusInsideClosedFiniteIndex_spec

Documentation

Specification of the modulus selected for a closed finite-index subgroup.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem modulusInsideClosedFiniteIndex_spec
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (modulusInsideClosedFiniteIndex H hclosed).congruenceSubgroup ≤ H

theorem

isClosed_and_finiteIndex_iff_exists_congruenceSubgroup_le

L1084 ↗

RayClass.isClosed_and_finiteIndex_iff_exists_congruenceSubgroup_le

Documentation

A subgroup of the idele class group is closed of finite index exactly when it contains a ray congruence subgroup.

Source context 6 commands

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

open scoped NumberField RestrictedProduct WithZero
open NumberField IsDedekindDomain
open Topology
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace RayClass

Lean source · statement

theorem isClosed_and_finiteIndex_iff_exists_congruenceSubgroup_le
    (H : Subgroup (IdeleClassGroup K)) :
    (IsClosed (H : Set (IdeleClassGroup K)) ∧ H.FiniteIndex) ↔
      ∃ m : Modulus K, m.congruenceSubgroup ≤ H

Module documentation

The congruence topology on the idele class group

Declarations