NYLL
Module

NumberFieldPowerSeparation.lean

Nyll.AnabelianGeometry.KummerTheory.NumberFieldPowerSeparation
5 declarations indexed from sourceView source ↗

Module documentation

Cyclic power separation over number fields

Although the entire multiplicative group of a number field is not finitely generated, two prescribed elements lie in one finitely generated S-unit group. This subgroup is saturated under roots in the original field. Consequently cyclic subgroups are determined by their images modulo all positive powers in the original number field.

The power relations here are over the original field. Descending relations obtained only after adjoining roots of unity is a separate arithmetic step.

Imports3
Imported by4

Declarations

theorem

exists_sUnitGroup_mem

L34 ↗
AnabelianGeometry.KummerTheory.exists_sUnitGroup_mem
Documentation

Every nonzero element has finite support at the finite places.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem exists_sUnitGroup_mem (a : Kˣ) :
    ∃ S : Finset (HeightOneSpectrum (𝓞 K)), a ∈ SUnitGroup (K := K) S
theorem

mem_sUnitGroup_of_pow_mem

L52 ↗
AnabelianGeometry.KummerTheory.mem_sUnitGroup_of_pow_mem
Documentation

An element of the number field whose positive power is an S-unit is itself an S-unit.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem mem_sUnitGroup_of_pow_mem
    (S : Finset (HeightOneSpectrum (𝓞 K))) (n : ℕ+) (y : Kˣ)
    (hy : y ^ (n : ℕ) ∈ SUnitGroup (K := K) S) :
    y ∈ SUnitGroup (K := K) S
theorem

numberField_mem_zpowers_of_forall_mem_sup_powers

L65 ↗
AnabelianGeometry.KummerTheory.numberField_mem_zpowers_of_forall_mem_sup_powers
Documentation

Cyclic subgroup membership is detected by all power quotients of the multiplicative group of the original number field.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem numberField_mem_zpowers_of_forall_mem_sup_powers (a b : Kˣ)
    (h : ∀ n : ℕ+, a ∈ Subgroup.zpowers b ⊔
      (powMonoidHom (α := Kˣ) (n : ℕ)).range) : a ∈ Subgroup.zpowers b
theorem

numberField_iInf_zpowers_sup_powers

L86 ↗
AnabelianGeometry.KummerTheory.numberField_iInf_zpowers_sup_powers
Documentation

Over a number field, intersecting all ambient-power enlargements of a cyclic subgroup recovers precisely that subgroup.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem numberField_iInf_zpowers_sup_powers (a : Kˣ) :
    (⨅ n : ℕ+, Subgroup.zpowers a ⊔
      (powMonoidHom (α := Kˣ) (n : ℕ)).range) = Subgroup.zpowers a
theorem

numberField_zpowers_eq_of_forall_sup_powers_eq

L97 ↗
AnabelianGeometry.KummerTheory.numberField_zpowers_eq_of_forall_sup_powers_eq
Documentation

Matching cyclic subgroups modulo every positive power in a number field implies equality of the actual cyclic subgroups.

Source context 5 commands

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

noncomputable section
open IsDedekindDomain
open scoped NumberField
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem numberField_zpowers_eq_of_forall_sup_powers_eq (a b : Kˣ)
    (h : ∀ n : ℕ+,
      Subgroup.zpowers a ⊔ (powMonoidHom (α := Kˣ) (n : ℕ)).range =
      Subgroup.zpowers b ⊔ (powMonoidHom (α := Kˣ) (n : ℕ)).range) :
    Subgroup.zpowers a = Subgroup.zpowers b

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