NYLL
Module

SUnitLocalPowerKernel.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.SUnitPreparation.SUnitLocalPowerKernel
11 declarations indexed from sourceView source ↗

Module documentation

The local-power kernel of S-units

The localization map on S-units, its kernel, its quotient by global powers, and the associated Kummer radical.

Imports2
Imported by3

Declarations

def

sUnitLocalPowerMap

L32 ↗
KummerTheory.sUnitLocalPowerMap
Documentation

The diagonal localization map Kˢ → ∏ v ∈ T, K_vˣ / K_vˣⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitLocalPowerMap
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    SUnitGroup (K := K) S →*
      ∀ v : T,
        ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)ˣ ⧸
          (powMonoidHom (n : ℕ) :
            ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)ˣ →*
              ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)ˣ).range
def

sUnitLocalPowerKernel

L51 ↗
KummerTheory.sUnitLocalPowerKernel
Documentation

The subgroup Δ of S-units which are local n-th powers at every place in T.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitLocalPowerKernel
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (SUnitGroup (K := K) S)
theorem

mem_sUnitLocalPowerKernel_iff

L58 ↗
KummerTheory.mem_sUnitLocalPowerKernel_iff
Documentation

Elementwise description of the local-power kernel Δ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem mem_sUnitLocalPowerKernel_iff
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (x : SUnitGroup (K := K) S) :
    x ∈ sUnitLocalPowerKernel (K := K) n S T ↔
      ∀ v : T,
        Units.map
            (algebraMap K
              ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)).toMonoidHom
            (x : Kˣ) ∈
          (powMonoidHom (n : ℕ) :
            ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)ˣ →*
              ((v : HeightOneSpectrum (𝓞 K)).adicCompletion K)ˣ).range
theorem

nthPowerSubgroup_le_sUnitLocalPowerKernel

L82 ↗
KummerTheory.nthPowerSubgroup_le_sUnitLocalPowerKernel
Documentation

Global n-th powers are local n-th powers at every place.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem nthPowerSubgroup_le_sUnitLocalPowerKernel
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    (powMonoidHom (n : ℕ) :
        SUnitGroup (K := K) S →*
          SUnitGroup (K := K) S).range ≤
      sUnitLocalPowerKernel (K := K) n S T
def

sUnitLocalPowerKernelNthPowers

L105 ↗
KummerTheory.sUnitLocalPowerKernelNthPowers
Documentation

The copy of Kˢⁿ inside the local-power kernel Δ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitLocalPowerKernelNthPowers
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Subgroup (sUnitLocalPowerKernel (K := K) n S T)
def

sUnitLocalPowerKernelQuotientMap

L115 ↗
KummerTheory.sUnitLocalPowerKernelQuotientMap
Documentation

The canonical map Δ / Kˢⁿ → Kˢ / Kˢⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
def sUnitLocalPowerKernelQuotientMap
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    sUnitLocalPowerKernel (K := K) n S T ⧸
        sUnitLocalPowerKernelNthPowers (K := K) n S T →*
      SUnitGroup (K := K) S ⧸
        (powMonoidHom (n : ℕ) :
          SUnitGroup (K := K) S →*
            SUnitGroup (K := K) S).range
theorem

sUnitLocalPowerKernelQuotientMap_injective

L135 ↗
KummerTheory.sUnitLocalPowerKernelQuotientMap_injective
Documentation

Inclusion of Δ induces an injection on quotients by Kˢⁿ.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem sUnitLocalPowerKernelQuotientMap_injective
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Function.Injective
      (sUnitLocalPowerKernelQuotientMap (K := K) n S T)
instance

finite_sUnitLocalPowerKernelQuotient

L155 ↗
KummerTheory.finite_sUnitLocalPowerKernelQuotient
Documentation

The restricted radical quotient Δ / Kˢⁿ is finite.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
instance finite_sUnitLocalPowerKernelQuotient
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K))) :
    Finite
      (sUnitLocalPowerKernel (K := K) n S T ⧸
        sUnitLocalPowerKernelNthPowers (K := K) n S T)
theorem

card_sUnitLocalPowerKernelQuotient_le

L167 ↗
KummerTheory.card_sUnitLocalPowerKernelQuotient_le
Documentation

The restricted radical quotient has cardinality at most n ^ s.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem card_sUnitLocalPowerKernelQuotient_le
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Nat.card
        (sUnitLocalPowerKernel (K := K) n S T ⧸
          sUnitLocalPowerKernelNthPowers (K := K) n S T) ≤
      (n : ℕ) ^ totalPlaceCard (K := K) S
def

sUnitLocalPowerRadical

L182 ↗
KummerTheory.sUnitLocalPowerRadical
Documentation

The local-power kernel, regarded as an actual subgroup of Kˣ.

Source context 6 commands

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

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

mem_sUnitLocalPowerRadical_iff

L191 ↗
KummerTheory.mem_sUnitLocalPowerRadical_iff
Documentation

Membership in the local-power radical is membership in the kernel through the canonical S-unit inclusion.

Source context 6 commands

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

open scoped NumberField IsMulCommutative NNReal ValuativeRel
open NumberField IsDedekindDomain
open LocalFieldTheory
noncomputable section
namespace KummerTheory
variable {K : Type*} [Field K]
    [numberFieldK : NumberField K]
Lean source · statement
theorem mem_sUnitLocalPowerRadical_iff
    (n : ℕ+)
    (S T : Finset (HeightOneSpectrum (𝓞 K)))
    (x : Kˣ) :
    x ∈ sUnitLocalPowerRadical (K := K) n S T ↔
      ∃ hx : x ∈ SUnitGroup (K := K) S,
        (⟨x, hx⟩ : SUnitGroup (K := K) S) ∈
          sUnitLocalPowerKernel (K := K) n S T

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