Module

EmbeddedMultiplicativeRigidity.lean

Nyll.AnabelianGeometry.ProjectiveLine.EmbeddedMultiplicativeRigidity

3 declarations indexed from sourceView source ↗

Module documentation

Multiplicative reconstruction through a complex embedding

The archimedean argument handles the mixed torsion/non-torsion case. Together with the purely algebraic inversion argument, two cyclic multiplicative subgroups determine a parameter outside the explicit quadratic exceptional locus.

Imports2

Imported by2

theorem

norm_embedding_unit_eq_one

L26 ↗

AnabelianGeometry.ProjectiveLine.norm_embedding_unit_eq_one

Documentation

A finite-order unit has norm one under every complex embedding.

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 norm_embedding_unit_eq_one (e : K →+* ℂ) (x : Kˣ)
    (hx : IsOfFinOrder x) : ‖e (x : K)‖ = 1

theorem

units_eq_of_zpowers_eq_of_complement_of_embedding

L35 ↗

AnabelianGeometry.ProjectiveLine.units_eq_of_zpowers_eq_of_complement_of_embedding

Documentation

One non-torsion parameter suffices for reconstruction; its complement may be a 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 units_eq_of_zpowers_eq_of_complement_of_embedding
    (e : K →+* ℂ) {x y c d : Kˣ}
    (hc : (x : K) + (c : K) = 1) (hd : (y : K) + (d : K) = 1)
    (hx : ¬ IsOfFinOrder x)
    (hxy : Subgroup.zpowers x = Subgroup.zpowers y)
    (hcd : Subgroup.zpowers c = Subgroup.zpowers d) : x = y

theorem

units_eq_or_sq_sub_add_one_eq_zero_of_embedding

L75 ↗

AnabelianGeometry.ProjectiveLine.units_eq_or_sq_sub_add_one_eq_zero_of_embedding

Documentation

Equality of the parameter and complementary cyclic subgroups reconstructs the parameter, with only the explicit quadratic exceptional locus remaining.

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_or_sq_sub_add_one_eq_zero_of_embedding
    (e : K →+* ℂ) {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

Module documentation

Multiplicative reconstruction through a complex embedding

Declarations

norm_embedding_unit_eq_one

units_eq_of_zpowers_eq_of_complement_of_embedding

units_eq_or_sq_sub_add_one_eq_zero_of_embedding