Module

Basic.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.RayClass.Basic

11 declarations indexed from sourceView source ↗

Module documentation

Finite ray-modulus data

This file contains the finite local data used by ray congruence subgroups. A full modulus, including a selected set of real places, is defined in AlgebraicNumberTheory.RayClass.FullModulus.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.PrincipalTopology

Imported by6

abbrev

FiniteModulus

L31 ↗

RayClass.FiniteModulus

Documentation

A finite ray modulus. Its finite support records the prime powers dividing the modulus.

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 RayClass

Lean source · statement

abbrev FiniteModulus (K : Type*) [Field K] [NumberField K]

def

localHigherUnitMap

L36 ↗

RayClass.localHigherUnitMap

Documentation

Reduction of local integral units modulo the n-th power of the maximal ideal.

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 RayClass

Lean source · statement

def localHigherUnitMap
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    (v.adicCompletionIntegers K).units →*
      ((v.adicCompletionIntegers K) ⧸
        (IsLocalRing.maximalIdeal
          (v.adicCompletionIntegers K)) ^ n)ˣ

def

localHigherUnitGroup

L49 ↗

RayClass.localHigherUnitGroup

Documentation

The local higher unit group U_v^(n).

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 RayClass

Lean source · statement

def localHigherUnitGroup
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ) :
    Subgroup (v.adicCompletion K)ˣ

theorem

mem_localHigherUnitGroup_iff

L56 ↗

RayClass.mem_localHigherUnitGroup_iff

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 RayClass

Lean source · statement

theorem mem_localHigherUnitGroup_iff
    (v : HeightOneSpectrum (𝓞 K)) (n : ℕ)
    (x : (v.adicCompletion K)ˣ) :
    x ∈ localHigherUnitGroup v n ↔
      ∃ y : (v.adicCompletionIntegers K).units,
        (y : (v.adicCompletion K)ˣ) = x ∧
        localHigherUnitMap v n y = 1

theorem

localHigherUnitGroup_zero

L72 ↗

RayClass.localHigherUnitGroup_zero

Documentation

The zeroth higher unit group is the full group of local integral units.

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 RayClass

Lean source · statement

theorem localHigherUnitGroup_zero
    (v : HeightOneSpectrum (𝓞 K)) :
    localHigherUnitGroup v 0 =
      (v.adicCompletionIntegers K).units

def

infinitePositiveSubgroup

L100 ↗

RayClass.infinitePositiveSubgroup

Documentation

Positivity at a real infinite place. At a complex place the condition is vacuous, so this is the whole local multiplicative group.

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 RayClass

Lean source · full declaration

def infinitePositiveSubgroup (v : InfinitePlace K) :
    Subgroup v.Completionˣ where
  carrier := {x | ∀ hv : v.IsReal,
    0 < NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal
      hv (x : v.Completion)}
  one_mem' hv := by simp
  mul_mem' {x y} hx hy hv := by
    change 0 <
      NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal
        hv ((x : v.Completion) * (y : v.Completion))
    rw [map_mul]
    exact mul_pos (hx hv) (hy hv)
  inv_mem' {x} hx hv := by
    rw [Units.val_inv_eq_inv_val, map_inv₀]
    exact inv_pos.mpr (hx hv)

theorem

mem_infinitePositiveSubgroup_iff

L118 ↗

RayClass.mem_infinitePositiveSubgroup_iff

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

Lean source · statement

theorem mem_infinitePositiveSubgroup_iff
    (v : InfinitePlace K) (x : v.Completionˣ) :
    x ∈ infinitePositiveSubgroup v ↔
      ∀ hv : v.IsReal,
        0 < NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal
          hv (x : v.Completion)

def

finiteCongruenceSubgroup

L127 ↗

RayClass.finiteCongruenceSubgroup

Documentation

The finite idele congruence subgroup attached to a modulus.

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 RayClass

Lean source · full declaration

def finiteCongruenceSubgroup (m : FiniteModulus K) :
    Subgroup (FiniteIdeleGroup K) where
  carrier := {a | ∀ v, a v ∈ localHigherUnitGroup v (m v)}
  one_mem' v := (localHigherUnitGroup v (m v)).one_mem
  mul_mem' ha hb v :=
    (localHigherUnitGroup v (m v)).mul_mem (ha v) (hb v)
  inv_mem' ha v :=
    (localHigherUnitGroup v (m v)).inv_mem (ha v)

theorem

mem_finiteCongruenceSubgroup_iff

L137 ↗

RayClass.mem_finiteCongruenceSubgroup_iff

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 RayClass

Lean source · statement

theorem mem_finiteCongruenceSubgroup_iff
    (m : FiniteModulus K) (a : FiniteIdeleGroup K) :
    a ∈ finiteCongruenceSubgroup m ↔
      ∀ v, a v ∈ localHigherUnitGroup v (m v)

def

narrowInfiniteCongruenceSubgroup

L144 ↗

RayClass.narrowInfiniteCongruenceSubgroup

Documentation

Ideles positive at every real infinite place.

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 RayClass

Lean source · statement

def narrowInfiniteCongruenceSubgroup :
    Subgroup (InfiniteIdeleGroup K)

theorem

mem_narrowInfiniteCongruenceSubgroup_iff

L151 ↗

RayClass.mem_narrowInfiniteCongruenceSubgroup_iff

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

Lean source · statement

theorem mem_narrowInfiniteCongruenceSubgroup_iff
    (a : InfiniteIdeleGroup K) :
    a ∈ narrowInfiniteCongruenceSubgroup (K := K) ↔
      ∀ v, ContinuousMulEquiv.piUnits a v ∈
        infinitePositiveSubgroup v

Module documentation

Finite ray-modulus data

Declarations