NYLL
Module

Configuration.lean

Nyll.AnabelianGeometry.ProjectiveLine.Configuration
9 declarations indexed from sourceView source ↗

Module documentation

Reconstruction of labelled projective configurations

Normalize a reference triple and compare the remaining affine coordinates. Equal cross ratios then give an explicit projective coordinate equivalence carrying every label of one configuration to the corresponding label of the other.

Imports1
Imported by1

Declarations

def

normalizeTriple

L23 ↗
AnabelianGeometry.ProjectiveLine.normalizeTriple
Documentation

The coordinate normalization of three distinct projective points.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
def normalizeTriple (a b c : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a) :
    Projectivization K (K × K) ≃ Projectivization K (K × K)
theorem

normalizeTriple_apply

L32 ↗
AnabelianGeometry.ProjectiveLine.normalizeTriple_apply
Documentation

The affine coordinate under normalization is the intrinsic cross ratio.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem normalizeTriple_apply (a b c d : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a) (hdb : d ≠ b) :
    normalizeTriple a b c hab hcb hca d = affinePoint (crossRatio a b c d)
theorem

normalizeTriple_second

L40 ↗
AnabelianGeometry.ProjectiveLine.normalizeTriple_second
Documentation

The middle reference point is the pole of the normalized affine coordinate.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem normalizeTriple_second (a b c : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a) :
    normalizeTriple a b c hab hcb hca b = infinityPoint
theorem

crossRatio_normalizeTriple

L52 ↗
AnabelianGeometry.ProjectiveLine.crossRatio_normalizeTriple
Documentation

Triple normalization preserves all cross ratios.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem crossRatio_normalizeTriple (a b c : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a)
    (w x y z : Projectivization K (K × K)) :
    crossRatio (normalizeTriple a b c hab hcb hca w)
      (normalizeTriple a b c hab hcb hca x)
      (normalizeTriple a b c hab hcb hca y)
      (normalizeTriple a b c hab hcb hca z) = crossRatio w x y z
def

matchTriples

L62 ↗
AnabelianGeometry.ProjectiveLine.matchTriples
Documentation

Change coordinates by normalizing the source and undoing target normalization.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
def matchTriples (a b c a' b' c' : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a)
    (hab' : a' ≠ b') (hcb' : c' ≠ b') (hca' : c' ≠ a') :
    Projectivization K (K × K) ≃ Projectivization K (K × K)
theorem

crossRatio_matchTriples

L70 ↗
AnabelianGeometry.ProjectiveLine.crossRatio_matchTriples
Documentation

The coordinate change matching two triples preserves cross ratios.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · full declaration
theorem crossRatio_matchTriples (a b c a' b' c' : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a)
    (hab' : a' ≠ b') (hcb' : c' ≠ b') (hca' : c' ≠ a')
    (w x y z : Projectivization K (K × K)) :
    let f := matchTriples a b c a' b' c' hab hcb hca hab' hcb' hca'
    crossRatio (f w) (f x) (f y) (f z) = crossRatio w x y z := by
  dsimp only
  rw [← crossRatio_normalizeTriple a' b' c' hab' hcb' hca']
  change crossRatio
    ((normalizeTriple a' b' c' hab' hcb' hca')
      ((normalizeTriple a' b' c' hab' hcb' hca').symm
        (normalizeTriple a b c hab hcb hca w)))
    ((normalizeTriple a' b' c' hab' hcb' hca')
      ((normalizeTriple a' b' c' hab' hcb' hca').symm
        (normalizeTriple a b c hab hcb hca x)))
    ((normalizeTriple a' b' c' hab' hcb' hca')
      ((normalizeTriple a' b' c' hab' hcb' hca').symm
        (normalizeTriple a b c hab hcb hca y)))
    ((normalizeTriple a' b' c' hab' hcb' hca')
      ((normalizeTriple a' b' c' hab' hcb' hca').symm
        (normalizeTriple a b c hab hcb hca z))) = _
  simp only [Equiv.apply_symm_apply]
  exact crossRatio_normalizeTriple a b c hab hcb hca w x y z
theorem

matchTriples_apply

L95 ↗
AnabelianGeometry.ProjectiveLine.matchTriples_apply
Documentation

Equal cross ratios determine the image of any point away from the pole.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem matchTriples_apply (a b c a' b' c' d d' : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a)
    (hab' : a' ≠ b') (hcb' : c' ≠ b') (hca' : c' ≠ a')
    (hdb : d ≠ b) (hdb' : d' ≠ b')
    (h : crossRatio a b c d = crossRatio a' b' c' d') :
    matchTriples a b c a' b' c' hab hcb hca hab' hcb' hca' d = d'
theorem

matchTriples_second

L109 ↗
AnabelianGeometry.ProjectiveLine.matchTriples_second
Documentation

The coordinate matching also carries the pole to the target pole.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem matchTriples_second (a b c a' b' c' : Projectivization K (K × K))
    (hab : a ≠ b) (hcb : c ≠ b) (hca : c ≠ a)
    (hab' : a' ≠ b') (hcb' : c' ≠ b') (hca' : c' ≠ a') :
    matchTriples a b c a' b' c' hab hcb hca hab' hcb' hca' b = b'
theorem

matchTriples_configuration

L122 ↗
AnabelianGeometry.ProjectiveLine.matchTriples_configuration
Documentation

A single projective coordinate change matches every label once the cross ratios relative to three distinct reference labels agree. The index type may be infinite; no point-by-point choice of coordinate change is made.

Source context 3 commands

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

namespace AnabelianGeometry.ProjectiveLine
universe u v
variable {K : Type u} [Field K]
Lean source · statement
theorem matchTriples_configuration {ι : Type v}
    (x y : ι → Projectivization K (K × K))
    (hx : Function.Injective x) (hy : Function.Injective y)
    (i₀ iInf i₁ : ι) (hZeroInf : i₀ ≠ iInf) (hOneInf : i₁ ≠ iInf) (h₁₀ : i₁ ≠ i₀)
    (h : ∀ i, crossRatio (x i₀) (x iInf) (x i₁) (x i) =
      crossRatio (y i₀) (y iInf) (y i₁) (y i)) (i : ι) :
    matchTriples (x i₀) (x iInf) (x i₁) (y i₀) (y iInf) (y i₁)
      (hx.ne hZeroInf) (hx.ne hOneInf) (hx.ne h₁₀)
      (hy.ne hZeroInf) (hy.ne hOneInf) (hy.ne h₁₀) (x i) = y i

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