NYLL
Module

SPlaces.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.SPlaces
17 declarations indexed from sourceView source ↗

Module documentation

Ideles and units with finite support

This file formalizes finite-support objects for ideles and units. Since every archimedean place is always included, a finite set S below records only its finite places.

Imports3
Imported by7

Declarations

def

supportedAt

L32 ↗
FiniteIdeleGroup.supportedAt
Documentation

The finite ideles that are integral units away from S.

Source context 5 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
Lean source · full declaration
def supportedAt (S : Set (HeightOneSpectrum (𝓞 K))) :
    Subgroup (FiniteIdeleGroup K) where
  carrier := {a | ∀ v, v ∉ S →
    a v ∈ (v.adicCompletionIntegers K).units}
  one_mem' _ _ := Submonoid.one_mem _
  mul_mem' ha hb v hv := Submonoid.mul_mem _
    (ha v hv) (hb v hv)
  inv_mem' ha v hv := Subgroup.inv_mem _
    (ha v hv)
theorem

mem_supportedAt_iff

L43 ↗
FiniteIdeleGroup.mem_supportedAt_iff
Source context 5 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
Lean source · statement
theorem mem_supportedAt_iff
    (S : Set (HeightOneSpectrum (𝓞 K)))
    (a : FiniteIdeleGroup K) :
    a ∈ supportedAt (K := K) S ↔
      ∀ v, v ∉ S →
        a v ∈ (v.adicCompletionIntegers K).units
theorem

supportedAt_mono

L51 ↗
FiniteIdeleGroup.supportedAt_mono
Source context 5 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
Lean source · statement
theorem supportedAt_mono {S T : Set (HeightOneSpectrum (𝓞 K))}
    (hST : S ⊆ T) :
    supportedAt (K := K) S ≤ supportedAt (K := K) T
theorem

mem_supportedAt_nonLocalUnits

L57 ↗
FiniteIdeleGroup.mem_supportedAt_nonLocalUnits
Source context 5 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
Lean source · statement
theorem mem_supportedAt_nonLocalUnits
    (a : FiniteIdeleGroup K) :
    a ∈ supportedAt (K := K)
      {v | a v ∉ (v.adicCompletionIntegers K).units}
theorem

exists_finset_supportedAt

L65 ↗
FiniteIdeleGroup.exists_finset_supportedAt
Documentation

Every finite idele is supported at some finite set of finite places.

Source context 5 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
Lean source · statement
theorem exists_finset_supportedAt (a : FiniteIdeleGroup K) :
    ∃ S : Finset (HeightOneSpectrum (𝓞 K)),
      a ∈ supportedAt (K := K) (S : Set _)
theorem

iSup_finset_supportedAt

L77 ↗
FiniteIdeleGroup.iSup_finset_supportedAt
Documentation

The union of the finite-support subgroups is the full finite idele group.

Source context 5 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
Lean source · statement
theorem iSup_finset_supportedAt :
    ⨆ S : Finset (HeightOneSpectrum (𝓞 K)),
      supportedAt (K := K) (S : Set _) = ⊤
theorem

supportedAt_empty

L87 ↗
FiniteIdeleGroup.supportedAt_empty
Documentation

The everywhere-integral subgroup is the subgroup supported at the empty set.

Source context 5 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
Lean source · statement
theorem supportedAt_empty :
    supportedAt (K := K)
      (∅ : Set (HeightOneSpectrum (𝓞 K))) =
      integralSubgroup (K := K)
theorem

isOpen_supportedAt

L97 ↗
FiniteIdeleGroup.isOpen_supportedAt
Documentation

For a finite set S, the S-finite-ideles form an open subgroup.

Source context 5 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
Lean source · statement
theorem isOpen_supportedAt (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IsOpen
      ((supportedAt (K := K) (S : Set _) :
        Subgroup (FiniteIdeleGroup K)) : Set (FiniteIdeleGroup K))
def

supportedAt

L112 ↗
IdeleGroup.supportedAt
Documentation

The group I_K^S, with all infinite places included and finite components integral away from S.

Source context 5 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
Lean source · statement
def supportedAt (S : Set (HeightOneSpectrum (𝓞 K))) :
    Subgroup (IdeleGroup K)
theorem

mem_supportedAt_iff

L118 ↗
IdeleGroup.mem_supportedAt_iff
Source context 5 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
Lean source · statement
theorem mem_supportedAt_iff
    (S : Set (HeightOneSpectrum (𝓞 K)))
    (a : IdeleGroup K) :
    a ∈ supportedAt (K := K) S ↔
      ∀ v, v ∉ S →
        a.2 v ∈ (v.adicCompletionIntegers K).units
theorem

supportedAt_mono

L126 ↗
IdeleGroup.supportedAt_mono
Source context 5 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
Lean source · statement
theorem supportedAt_mono {S T : Set (HeightOneSpectrum (𝓞 K))}
    (hST : S ⊆ T) :
    supportedAt (K := K) S ≤ supportedAt (K := K) T
theorem

exists_finset_supportedAt

L133 ↗
IdeleGroup.exists_finset_supportedAt
Documentation

Every idele lies in I_K^S for some finite set S.

Source context 5 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
Lean source · statement
theorem exists_finset_supportedAt (a : IdeleGroup K) :
    ∃ S : Finset (HeightOneSpectrum (𝓞 K)),
      a ∈ supportedAt (K := K) (S : Set _)
theorem

iSup_finset_supportedAt

L138 ↗
IdeleGroup.iSup_finset_supportedAt
Source context 5 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
Lean source · statement
theorem iSup_finset_supportedAt :
    ⨆ S : Finset (HeightOneSpectrum (𝓞 K)),
      supportedAt (K := K) (S : Set _) = ⊤
theorem

supportedAt_empty

L146 ↗
IdeleGroup.supportedAt_empty
Source context 5 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
Lean source · statement
theorem supportedAt_empty :
    supportedAt (K := K)
      (∅ : Set (HeightOneSpectrum (𝓞 K))) =
      integralAtFinitePlaces (K := K)
theorem

isOpen_supportedAt

L156 ↗
IdeleGroup.isOpen_supportedAt
Source context 5 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
Lean source · statement
theorem isOpen_supportedAt
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    IsOpen
      ((supportedAt (K := K) (S : Set _) :
        Subgroup (IdeleGroup K)) : Set (IdeleGroup K))
abbrev

SUnitGroup

L167 ↗
Documentation

The group of S-units of K, for a finite set of finite places. All infinite places are understood to lie in S.

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 SUnitGroup
    (S : Finset (HeightOneSpectrum (𝓞 K)))
theorem

mem_SUnitGroup_iff

L172 ↗
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
theorem mem_SUnitGroup_iff
    (S : Finset (HeightOneSpectrum (𝓞 K))) (x : Kˣ) :
    x ∈ SUnitGroup (K := K) S ↔
      ∀ v : HeightOneSpectrum (𝓞 K), v ∉ S →
        v.valuation K x = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.