The convention sends the first three ordered points to 0, ∞, 1. Homogeneous coordinates include infinity without a separate affine chart. Independent rescaling does not change the ratio, and the projective definition is evaluated by the proved representative formula.
The alternating determinant of two homogeneous coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def bracket (a b : K × K) : KThe cross ratio in homogeneous coordinates, with convention (0, ∞, 1, t) ↦ t. As with field division, this is a total function; geometric applications use distinct points.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def homogeneousCrossRatio (a b c d : K × K) : KDeterminants multiply by both scalar factors.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem bracket_smul (a b : K × K) (s t : K) :
bracket (s • a) (t • b) = (s * t) * bracket a bSwapping the two coordinates of a determinant changes its sign.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem bracket_swap (a b : K × K) : bracket a b = -bracket b aIndependent nonzero rescaling of the four representatives preserves the cross ratio.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_smul (a b c d : K × K) (s t u v : K)
(hs : s ≠ 0) (ht : t ≠ 0) (hu : u ≠ 0) (hv : v ≠ 0) :
homogeneousCrossRatio (s • a) (t • b) (u • c) (v • d) =
homogeneousCrossRatio a b c dThe cross ratio of four points of the projective line.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def crossRatio (a b c d : Projectivization K (K × K)) : KThe projective cross ratio can be computed with any nonzero representatives.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem crossRatio_mk (a b c d : K × K)
(ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hd : d ≠ 0) :
crossRatio (Projectivization.mk K a ha) (Projectivization.mk K b hb)
(Projectivization.mk K c hc) (Projectivization.mk K d hd) =
homogeneousCrossRatio a b c dEvaluation in the normalized coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_zero_infty_one (t : K) :
homogeneousCrossRatio (0, 1) (1, 0) (1, 1) (t, 1) = tSimultaneously swapping the first pair and the last pair preserves the cross ratio.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_swap_pairs (a b c d : K × K) :
homogeneousCrossRatio b a d c = homogeneousCrossRatio a b c dSwapping the first two points inverts the cross ratio, even for degenerate coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_swap_first (a b c d : K × K) :
homogeneousCrossRatio b a c d = (homogeneousCrossRatio a b c d)⁻¹Four appropriate nonzero determinants give a nonzero cross ratio.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_ne_zero (a b c d : K × K)
(hda : bracket d a ≠ 0) (hcb : bracket c b ≠ 0)
(hdb : bracket d b ≠ 0) (hca : bracket c a ≠ 0) :
homogeneousCrossRatio a b c d ≠ 0The determinant identity underlying the six cross-ratio transformations.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem bracket_crossRatio_relation (a b c d : K × K) :
bracket d b * bracket c a - bracket d a * bracket c b =
bracket d c * bracket b aThe complementary cross ratio is another quotient of the same brackets.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem one_sub_homogeneousCrossRatio (a b c d : K × K)
(hdb : bracket d b ≠ 0) (hca : bracket c a ≠ 0) :
1 - homogeneousCrossRatio a b c d =
(bracket d c * bracket b a) / (bracket d b * bracket c a)The cross ratio cannot equal one when both pairs are distinct and its denominator is nonzero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_ne_one (a b c d : K × K)
(hdb : bracket d b ≠ 0) (hca : bracket c a ≠ 0)
(hdc : bracket d c ≠ 0) (hba : bracket b a ≠ 0) :
homogeneousCrossRatio a b c d ≠ 1A linear change of homogeneous coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def transform (α β γ δ : K) (a : K × K) : K × KA linear change multiplies each bracket by its determinant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem bracket_transform (α β γ δ : K) (a b : K × K) :
bracket (transform α β γ δ a) (transform α β γ δ b) =
(α * δ - β * γ) * bracket a bEvery invertible linear coordinate change preserves the homogeneous cross ratio.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem homogeneousCrossRatio_transform (α β γ δ : K)
(h : α * δ - β * γ ≠ 0) (a b c d : K × K) :
homogeneousCrossRatio (transform α β γ δ a) (transform α β γ δ b)
(transform α β γ δ c) (transform α β γ δ d) =
homogeneousCrossRatio a b c d