Three distinct ordered points admit an explicit invertible coordinate change sending them to zero, infinity, and one. Its affine coordinate is the cross ratio.
A finite point in the standard affine chart.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def affinePoint (t : K) : Projectivization K (K × K)The point outside the standard affine chart.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def infinityPoint : Projectivization K (K × K)The determinant of the normalization matrix.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalization_determinant (a b c : K × K) :
(a.2 * bracket c b) * (-b.1 * bracket c a) -
(-a.1 * bracket c b) * (b.2 * bracket c a) =
bracket a b * bracket c b * bracket c aNormalize a triple of noncollinear homogeneous representatives.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]def normalizeCoordinates (a b c : K × K)
(hab : bracket a b ≠ 0) (hcb : bracket c b ≠ 0) (hca : bracket c a ≠ 0) :
Projectivization K (K × K) ≃ Projectivization K (K × K)The normalization matrix has the two cross-ratio factors as its coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalization_transform (a b c d : K × K) :
transform (a.2 * bracket c b) (-a.1 * bracket c b)
(b.2 * bracket c a) (-b.1 * bracket c a) d =
(bracket d a * bracket c b, bracket d b * bracket c a)On the complement of the second point, normalization is the affine cross ratio.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalizeCoordinates_mk (a b c d : K × K)
(hab : bracket a b ≠ 0) (hcb : bracket c b ≠ 0) (hca : bracket c a ≠ 0)
(hd : d ≠ 0) (hdb : bracket d b ≠ 0) :
normalizeCoordinates a b c hab hcb hca (Projectivization.mk K d hd) =
affinePoint (homogeneousCrossRatio a b c d)Normalization sends the first point to zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalizeCoordinates_first (a b c : K × K)
(hab : bracket a b ≠ 0) (hcb : bracket c b ≠ 0) (hca : bracket c a ≠ 0)
(ha : a ≠ 0) :
normalizeCoordinates a b c hab hcb hca (Projectivization.mk K a ha) =
affinePoint 0Normalization sends the third point to one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalizeCoordinates_third (a b c : K × K)
(hab : bracket a b ≠ 0) (hcb : bracket c b ≠ 0) (hca : bracket c a ≠ 0)
(hc : c ≠ 0) :
normalizeCoordinates a b c hab hcb hca (Projectivization.mk K c hc) =
affinePoint 1Normalization sends the second point to infinity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace AnabelianGeometry.ProjectiveLine
universe u
variable {K : Type u} [Field K]theorem normalizeCoordinates_second (a b c : K × K)
(hab : bracket a b ≠ 0) (hcb : bracket c b ≠ 0) (hca : bracket c a ≠ 0)
(hb : b ≠ 0) :
normalizeCoordinates a b c hab hcb hca (Projectivization.mk K b hb) =
infinityPoint