Module

CrossRatioSeparation.lean

Nyll.AnabelianGeometry.ProjectiveLine.CrossRatioSeparation

6 declarations indexed from sourceView source ↗

Module documentation

Separation of projective points by a cross ratio

For a fixed nondegenerate ordered triple, the cross ratio separates fourth points in its affine chart. This is proved for homogeneous representatives and then for the actual projectivization quotient.

Imports3

Nyll.AnabelianGeometry.ProjectiveLine.CrossRatio
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.FieldSimp

Imported by3

theorem

bracket_eq_zero_of_homogeneousCrossRatio_eq

L26 ↗

AnabelianGeometry.ProjectiveLine.bracket_eq_zero_of_homogeneousCrossRatio_eq

Documentation

Equal cross ratios force the two fourth representatives to be collinear.

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 bracket_eq_zero_of_homogeneousCrossRatio_eq (a b c d e : K × K)
    (hba : bracket b a ≠ 0) (hca : bracket c a ≠ 0) (hcb : bracket c b ≠ 0)
    (hdb : bracket d b ≠ 0) (heb : bracket e b ≠ 0)
    (h : homogeneousCrossRatio a b c d = homogeneousCrossRatio a b c e) :
    bracket d e = 0

theorem

eq_smul_of_bracket_eq_zero

L43 ↗

AnabelianGeometry.ProjectiveLine.eq_smul_of_bracket_eq_zero

Documentation

Collinear homogeneous vectors are explicitly proportional on a bracket chart.

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_smul_of_bracket_eq_zero (a b c : K × K)
    (hac : bracket a c ≠ 0) (hab : bracket a b = 0) :
    b = (bracket b c / bracket a c) • a

theorem

eq_of_crossRatio_eq

L67 ↗

AnabelianGeometry.ProjectiveLine.eq_of_crossRatio_eq

Documentation

The fourth projective point is determined by its cross ratio on the complement of the second point of a nondegenerate reference triple.

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_crossRatio_eq (a b c d e : Projectivization K (K × K))
    (hba : bracket b.rep a.rep ≠ 0) (hca : bracket c.rep a.rep ≠ 0)
    (hcb : bracket c.rep b.rep ≠ 0)
    (hdb : bracket d.rep b.rep ≠ 0) (heb : bracket e.rep b.rep ≠ 0)
    (h : crossRatio a b c d = crossRatio a b c e) : d = e

theorem

exists_bracket_ne_zero

L82 ↗

AnabelianGeometry.ProjectiveLine.exists_bracket_ne_zero

Documentation

A nonzero homogeneous vector has a nonzero bracket with some vector.

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 exists_bracket_ne_zero (a : K × K) (ha : a ≠ 0) :
    ∃ c : K × K, bracket a c ≠ 0

theorem

bracket_rep_eq_zero_iff

L95 ↗

AnabelianGeometry.ProjectiveLine.bracket_rep_eq_zero_iff

Documentation

Equality of projective points is exactly vanishing of their representative bracket.

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 bracket_rep_eq_zero_iff (d e : Projectivization K (K × K)) :
    bracket d.rep e.rep = 0 ↔ d = e

theorem

eq_of_crossRatio_eq_of_ne

L111 ↗

AnabelianGeometry.ProjectiveLine.eq_of_crossRatio_eq_of_ne

Documentation

An intrinsic version of cross-ratio separation, using only inequalities between projective points rather than conditions on chosen coordinates.

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_crossRatio_eq_of_ne (a b c d e : Projectivization K (K × K))
    (hba : b ≠ a) (hca : c ≠ a) (hcb : c ≠ b) (hdb : d ≠ b) (heb : e ≠ b)
    (h : crossRatio a b c d = crossRatio a b c e) : d = e

Module documentation

Separation of projective points by a cross ratio

Declarations

bracket_eq_zero_of_homogeneousCrossRatio_eq

eq_smul_of_bracket_eq_zero

eq_of_crossRatio_eq

exists_bracket_ne_zero

bracket_rep_eq_zero_iff

eq_of_crossRatio_eq_of_ne