NYLL
Module

IdelePowerLocalUnitSubgroup.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.IdelePowerLocalUnitSubgroup
7 declarations indexed from sourceView source ↗

Module documentation

Power-local-unit subgroups of the idele group

This module defines the subgroup of ideles that are local powers at selected places and integral units elsewhere, together with its intersection with principal ideles and the corresponding subgroup of S-unit powers.

Imports2
Imported by4

Declarations

def

idelePowerLocalUnitSubgroup

L33 ↗
GlobalClassFieldTheory.ClassFieldAxiom.idelePowerLocalUnitSubgroup
Documentation

Ideles that are local n-th powers at the prescribed places and integral units away from S ∪ T.

Source context 7 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
def idelePowerLocalUnitSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (IdeleGroup K)
theorem

mem_idelePowerLocalUnitSubgroup_iff

L54 ↗
GlobalClassFieldTheory.ClassFieldAxiom.mem_idelePowerLocalUnitSubgroup_iff
Documentation

Membership in idelePowerLocalUnitSubgroup expressed componentwise.

Source context 7 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem mem_idelePowerLocalUnitSubgroup_iff
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (a : IdeleGroup K) :
    a ∈ idelePowerLocalUnitSubgroup (K := K) n S T ↔
      (∀ w : InfinitePlace K,
        IdeleGroup.infiniteComponent w a ∈
          (powMonoidHom (n : ℕ) :
            w.Completionˣ →* w.Completionˣ).range) ∧
      (∀ v : HeightOneSpectrum (𝓞 K), v ∈ S →
        IdeleGroup.finiteComponent v a ∈
          (powMonoidHom (n : ℕ) :
            (v.adicCompletion K)ˣ →*
              (v.adicCompletion K)ˣ).range) ∧
      (∀ v : HeightOneSpectrum (𝓞 K), v ∉ S ∪ T →
        IdeleGroup.finiteComponent v a ∈
          (v.adicCompletionIntegers K).units)
def

principalIdelePowerLocalUnitSubgroup

L76 ↗
GlobalClassFieldTheory.ClassFieldAxiom.principalIdelePowerLocalUnitSubgroup
Documentation

Field units whose principal ideles lie in the local power-unit subgroup.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
def principalIdelePowerLocalUnitSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup Kˣ
def

sUnitNthPowersInField

L84 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitNthPowersInField
Documentation

The subgroup of field units obtained as n-th powers of U-units.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
def sUnitNthPowersInField
    (n : ℕ+)
    (U : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup Kˣ
theorem

mem_sUnitNthPowersInField_iff

L96 ↗
GlobalClassFieldTheory.ClassFieldAxiom.mem_sUnitNthPowersInField_iff
Documentation

A field unit is an n-th power of an U-unit exactly when it is simultaneously an U-unit and an n-th power in the field. The reverse direction uses the valuation-theoretic saturation of SUnitGroup.

Source context 6 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem mem_sUnitNthPowersInField_iff
    (n : ℕ+)
    (U : Finset (HeightOneSpectrum (𝓞 K)))
    (x : Kˣ) :
    x ∈ sUnitNthPowersInField (K := K) n U ↔
      x ∈ SUnitGroup (K := K) U ∧
        x ∈ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range
theorem

sUnitNthPowersInField_le_principalIdelePowerLocalUnitSubgroup

L135 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitNthPowersInField_le_principalIdelePowerLocalUnitSubgroup
Documentation

An n-th power of an (S ∪ T)-unit satisfies all local power-unit conditions.

Source context 7 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem sUnitNthPowersInField_le_principalIdelePowerLocalUnitSubgroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    sUnitNthPowersInField (K := K) n (S ∪ T) ≤
      principalIdelePowerLocalUnitSubgroup (K := K) n S T
theorem

principalIdelePowerLocalUnitSubgroup_le_sUnitGroup

L193 ↗
GlobalClassFieldTheory.ClassFieldAxiom.principalIdelePowerLocalUnitSubgroup_le_sUnitGroup
Documentation

A principal idele satisfying the local power-unit conditions comes from an (S ∪ T)-unit.

Source context 7 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
open scoped Classical in
Lean source · statement
theorem principalIdelePowerLocalUnitSubgroup_le_sUnitGroup
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    principalIdelePowerLocalUnitSubgroup (K := K) n S T ≤
      SUnitGroup (K := K) (S ∪ T)

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