NYLL
Module

NumberFieldPrimePowerSeparation.lean

Nyll.AnabelianGeometry.KummerTheory.NumberFieldPrimePowerSeparation
2 declarations indexed from sourceView source ↗

Module documentation

Prime-power separation over number fields

It suffices to compare cyclic subgroups modulo prime powers. The proof uses one saturated finitely generated S-unit group for both generators.

Imports2
Imported by1

Declarations

theorem

numberField_mem_zpowers_of_forall_mem_sup_prime_powers

L28 ↗
AnabelianGeometry.KummerTheory.numberField_mem_zpowers_of_forall_mem_sup_prime_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_prime_powers (a b : Kˣ)
    (h : ∀ p : ℕ, p.Prime → ∀ r : ℕ, a ∈ Subgroup.zpowers b ⊔
      (powMonoidHom (α := Kˣ) (p ^ r)).range) : a ∈ Subgroup.zpowers b
theorem

numberField_zpowers_eq_of_forall_sup_prime_powers_eq

L49 ↗
AnabelianGeometry.KummerTheory.numberField_zpowers_eq_of_forall_sup_prime_powers_eq
Documentation

Prime-power quotients determine actual cyclic subgroups, including their torsion.

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_prime_powers_eq (a b : Kˣ)
    (h : ∀ p : ℕ, p.Prime → ∀ r : ℕ,
      Subgroup.zpowers a ⊔ (powMonoidHom (α := Kˣ) (p ^ r)).range =
      Subgroup.zpowers b ⊔ (powMonoidHom (α := Kˣ) (p ^ r)).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.