NYLL
Module

NumberFieldRootFieldComparison.lean

Nyll.AnabelianGeometry.KummerTheory.NumberFieldRootFieldComparison
4 declarations indexed from sourceView source ↗

Module documentation

Uniform power comparison from root fields over number fields

We construct the relevant cyclotomic intermediate field in an algebraic closure and descend the resulting Kummer relation with the fixed loss given by the original field's roots-of-unity order. Equality at every exponent then identifies the cyclic subgroups generated by these fixed powers. The roots-of-unity ambiguity of the original generators is not removed.

Imports5
Imported by1

Declarations

theorem

exists_torsionOrder_power_relation_of_rootField_eq

L34 ↗
AnabelianGeometry.KummerTheory.exists_torsionOrder_power_relation_of_rootField_eq
Documentation

Equal root fields produce a power relation over the original number field with a bound independent of n. The cyclotomic extension used in the proof is constructed inside the algebraic closure.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem exists_torsionOrder_power_relation_of_rootField_eq
    (n : ℕ+) (a b : Kˣ)
    (h : rootField (L := AlgebraicClosure K) n (a : K) =
      rootField (L := AlgebraicClosure K) n (b : K)) :
    ∃ k : ℤ, ∃ d : Kˣ,
      b ^ NumberField.Units.torsionOrder K =
        (a ^ k) ^ NumberField.Units.torsionOrder K * d ^ (n : ℕ)
theorem

torsionOrder_power_mem_zpowers_of_forall_rootField_eq

L76 ↗
AnabelianGeometry.KummerTheory.torsionOrder_power_mem_zpowers_of_forall_rootField_eq
Documentation

All root-field comparisons determine the cyclic subgroup generated by the fixed roots-of-unity-order power. No exact recovery of the original cyclic subgroup is asserted by this theorem.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem torsionOrder_power_mem_zpowers_of_forall_rootField_eq
    (a b : Kˣ)
    (h : ∀ n : ℕ+, rootField (L := AlgebraicClosure K) n (a : K) =
      rootField (L := AlgebraicClosure K) n (b : K)) :
    b ^ NumberField.Units.torsionOrder K ∈
      Subgroup.zpowers (a ^ NumberField.Units.torsionOrder K)
theorem

zpowers_torsionOrder_eq_of_forall_rootField_eq

L96 ↗
AnabelianGeometry.KummerTheory.zpowers_torsionOrder_eq_of_forall_rootField_eq
Documentation

The fixed-power cyclic subgroups agree for two elements with identical full root fields at every positive exponent.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem zpowers_torsionOrder_eq_of_forall_rootField_eq
    (a b : Kˣ)
    (h : ∀ n : ℕ+, rootField (L := AlgebraicClosure K) n (a : K) =
      rootField (L := AlgebraicClosure K) n (b : K)) :
    Subgroup.zpowers (a ^ NumberField.Units.torsionOrder K) =
      Subgroup.zpowers (b ^ NumberField.Units.torsionOrder K)
theorem

exists_torsion_mul_or_inv_of_forall_rootField_eq

L110 ↗
AnabelianGeometry.KummerTheory.exists_torsion_mul_or_inv_of_forall_rootField_eq
Documentation

For a non-torsion element, equality of all full root fields leaves only inversion and multiplication by a root of unity in the original field.

Source context 4 commands

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

noncomputable section
open scoped IsMulCommutative
namespace AnabelianGeometry.KummerTheory
variable {K : Type*} [Field K] [NumberField K]
Lean source · statement
theorem exists_torsion_mul_or_inv_of_forall_rootField_eq
    (a b : Kˣ) (ha : ¬ IsOfFinOrder a)
    (h : ∀ n : ℕ+, rootField (L := AlgebraicClosure K) n (a : K) =
      rootField (L := AlgebraicClosure K) n (b : K)) :
    ∃ ζ : Kˣ, ζ ^ NumberField.Units.torsionOrder K = 1 ∧
      (b = ζ * a ∨ b = ζ * a⁻¹)

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