NYLL
Module

NumberFieldConfiguration.lean

Nyll.AnabelianGeometry.ProjectiveLine.NumberFieldConfiguration
2 declarations indexed from sourceView source ↗

Module documentation

Multiplicative configuration reconstruction over number fields

Two cyclic multiplicative subgroups recover a normalized parameter up to an explicit quadratic exception. The same data for one chosen square root eliminates that exception. These statements concern actual field elements; recovering their cyclic subgroups from a fundamental group is a separate step.

Imports2
Imported by1

Declarations

theorem

units_eq_or_sq_sub_add_one_eq_zero

L27 ↗
AnabelianGeometry.ProjectiveLine.units_eq_or_sq_sub_add_one_eq_zero
Documentation

Over a number field, the parameter and complementary cyclic subgroups leave only the quadratic exceptional locus.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem units_eq_or_sq_sub_add_one_eq_zero
    {x y c d : Kˣ}
    (hc : (x : K) + (c : K) = 1) (hd : (y : K) + (d : K) = 1)
    (hxy : Subgroup.zpowers x = Subgroup.zpowers y)
    (hcd : Subgroup.zpowers c = Subgroup.zpowers d) :
    x = y ∨ (x : K) ^ 2 - (x : K) + 1 = 0
theorem

units_eq_of_cyclic_data_and_square_roots

L38 ↗
AnabelianGeometry.ProjectiveLine.units_eq_of_cyclic_data_and_square_roots
Documentation

Cyclic subgroup data for a parameter and one square-root lift recovers the parameter without an exceptional-locus restriction.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K] [NumberField K]
Lean source · statement
theorem units_eq_of_cyclic_data_and_square_roots
    {x y c d t u v w : Kˣ}
    (hc : (x : K) + (c : K) = 1) (hd : (y : K) + (d : K) = 1)
    (hv : (t : K) + (v : K) = 1) (hw : (u : K) + (w : K) = 1)
    (ht : (t : K) ^ 2 = (x : K)) (hu : (u : K) ^ 2 = (y : K))
    (hxy : Subgroup.zpowers x = Subgroup.zpowers y)
    (hcd : Subgroup.zpowers c = Subgroup.zpowers d)
    (htu : Subgroup.zpowers t = Subgroup.zpowers u)
    (hvw : Subgroup.zpowers v = Subgroup.zpowers w) : x = y

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