Module

InversionRigidity.lean

Nyll.AnabelianGeometry.ProjectiveLine.InversionRigidity

4 declarations indexed from sourceView source ↗

Module documentation

Rigidity of a parameter and its complement under inversion

If both a parameter and its complement are known up to inversion, the only possible ambiguity lies on the polynomial X² - X + 1. These field identities are independent of the arithmetic mechanism that reconstructs the parameters.

Imports4

Mathlib.Algebra.Field.Basic
Mathlib.Tactic.FieldSimp
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.Ring

Imported by2

theorem

sq_sub_add_one_eq_zero_of_complement_inv

L28 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_eq_zero_of_complement_inv

Documentation

Simultaneous inversion of a parameter and its complement forces the sixth-cyclotomic polynomial to vanish.

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 sq_sub_add_one_eq_zero_of_complement_inv {x : K}
    (hx : x ≠ 0) (hx1 : x ≠ 1) (h : 1 - x⁻¹ = (1 - x)⁻¹) :
    x ^ 2 - x + 1 = 0

theorem

eq_or_sq_sub_add_one_eq_zero_of_inversion_choices

L43 ↗

AnabelianGeometry.ProjectiveLine.eq_or_sq_sub_add_one_eq_zero_of_inversion_choices

Documentation

A parameter and its complement, each determined up to inversion, determine that parameter except on an explicit quadratic 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]

Lean source · statement

theorem eq_or_sq_sub_add_one_eq_zero_of_inversion_choices {x y : K}
    (hx : x ≠ 0) (hx1 : x ≠ 1)
    (hxy : y = x ∨ y = x⁻¹)
    (hc : 1 - y = 1 - x ∨ 1 - y = (1 - x)⁻¹) :
    y = x ∨ x ^ 2 - x + 1 = 0

theorem

eq_of_inversion_choices

L58 ↗

AnabelianGeometry.ProjectiveLine.eq_of_inversion_choices

Documentation

Away from the quadratic exceptional locus, the two inversion choices recover the parameter uniquely.

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 eq_of_inversion_choices {x y : K}
    (hx : x ≠ 0) (hx1 : x ≠ 1) (he : x ^ 2 - x + 1 ≠ 0)
    (hxy : y = x ∨ y = x⁻¹)
    (hc : 1 - y = 1 - x ∨ 1 - y = (1 - x)⁻¹) : y = x

theorem

sq_sub_add_one_ne_zero_of_sq_eq

L68 ↗

AnabelianGeometry.ProjectiveLine.sq_sub_add_one_ne_zero_of_sq_eq

Documentation

In characteristic different from two, a square root of an exceptional parameter lies outside the same 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]

Lean source · statement

theorem sq_sub_add_one_ne_zero_of_sq_eq {x t : K}
    (h2 : (2 : K) ≠ 0) (hx : x ^ 2 - x + 1 = 0) (ht : t ^ 2 = x) :
    t ^ 2 - t + 1 ≠ 0

Module documentation

Rigidity of a parameter and its complement under inversion

Declarations

sq_sub_add_one_eq_zero_of_complement_inv

eq_or_sq_sub_add_one_eq_zero_of_inversion_choices

eq_of_inversion_choices

sq_sub_add_one_ne_zero_of_sq_eq