Module

ComplexConfiguration.lean

Nyll.AnabelianGeometry.ProjectiveLine.ComplexConfiguration

4 declarations indexed from sourceView source ↗

Module documentation

The unit-circle exceptional locus

A complex parameter whose value and complement both have norm one lies on the quadratic exceptional locus. This supplies the archimedean step for the simultaneous torsion case in multiplicative reconstruction.

Imports6

Mathlib.Analysis.Complex.Basic
Mathlib.GroupTheory.OrderOfElement
Mathlib.Tactic.Linarith
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.Ring

Imported by2

theorem

sq_sub_add_one_eq_zero_of_norm_eq_one

L25 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_eq_zero_of_norm_eq_one

Documentation

Two unit-circle conditions force the sixth-cyclotomic quadratic.

Source context 1 command

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

namespace AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem sq_sub_add_one_eq_zero_of_norm_eq_one {z : ℂ}
    (hz : ‖z‖ = 1) (hc : ‖1 - z‖ = 1) : z ^ 2 - z + 1 = 0

theorem

sq_sub_add_one_eq_zero_of_isOfFinOrder

L43 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_eq_zero_of_isOfFinOrder

Documentation

A complex parameter and its complement cannot both be torsion outside the quadratic exceptional locus.

Source context 1 command

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

namespace AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem sq_sub_add_one_eq_zero_of_isOfFinOrder {z : ℂ}
    (hz : IsOfFinOrder z) (hc : IsOfFinOrder (1 - z)) : z ^ 2 - z + 1 = 0

theorem

sq_sub_add_one_eq_zero_of_isOfFinOrder_of_embedding

L53 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_eq_zero_of_isOfFinOrder_of_embedding

Documentation

The torsion exceptional-locus calculation descends through any complex embedding, in particular through an embedding of a number field.

Source context 1 command

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

namespace AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem sq_sub_add_one_eq_zero_of_isOfFinOrder_of_embedding
    {K : Type*} [Field K] (e : K →+* ℂ) {x : K}
    (hx : IsOfFinOrder x) (hc : IsOfFinOrder (1 - x)) : x ^ 2 - x + 1 = 0

theorem

sq_sub_add_one_eq_zero_of_complement_norms

L69 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_eq_zero_of_complement_norms

Documentation

If the complements of a nonzero parameter and its inverse both have norm one, that parameter lies on the same quadratic exceptional locus.

Source context 1 command

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

namespace AnabelianGeometry.ProjectiveLine

Lean source · statement

theorem sq_sub_add_one_eq_zero_of_complement_norms {z : ℂ} (hz : z ≠ 0)
    (hc : ‖1 - z‖ = 1) (hi : ‖1 - z⁻¹‖ = 1) : z ^ 2 - z + 1 = 0

Module documentation

The unit-circle exceptional locus

Declarations

sq_sub_add_one_eq_zero_of_norm_eq_one

sq_sub_add_one_eq_zero_of_isOfFinOrder

sq_sub_add_one_eq_zero_of_isOfFinOrder_of_embedding

sq_sub_add_one_eq_zero_of_complement_norms