NYLL
Module

MultiplicativeRigidity.lean

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

Module documentation

Reconstruction from two cyclic multiplicative subgroups

For a unit and its complementary unit of infinite order, their cyclic subgroups determine the original parameter. This is the algebraic, non-torsion step; no reconstruction of these subgroups from Galois data is postulated.

Imports2
Imported by2

Declarations

theorem

pow_six_eq_one_of_sq_sub_add_one_eq_zero

L25 ↗
AnabelianGeometry.ProjectiveLine.pow_six_eq_one_of_sq_sub_add_one_eq_zero
Documentation

Every root of the exceptional quadratic is a sixth root of unity.

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]
Lean source · statement
theorem pow_six_eq_one_of_sq_sub_add_one_eq_zero {x : K}
    (h : x ^ 2 - x + 1 = 0) : x ^ 6 = 1
theorem

units_eq_of_zpowers_eq_of_complement

L31 ↗
AnabelianGeometry.ProjectiveLine.units_eq_of_zpowers_eq_of_complement
Documentation

Equality of the cyclic subgroups generated by two complementary units recovers both units when the two original units have infinite order.

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]
Lean source · statement
theorem units_eq_of_zpowers_eq_of_complement
    {x y c d : Kˣ}
    (hc : (x : K) + (c : K) = 1) (hd : (y : K) + (d : K) = 1)
    (hx : ¬ IsOfFinOrder x) (hco : ¬ IsOfFinOrder c)
    (hxy : Subgroup.zpowers x = Subgroup.zpowers y)
    (hcd : Subgroup.zpowers c = Subgroup.zpowers d) : x = y ∧ c = d

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