Affine coordinates on the standard open subset of projective space, with injectivity and compatibility with homogeneous equations.

noncomputable def CCDN.projectiveAffineCoordinates {K : Type u_1} [Field K] {n : ℕ} (x : Projectivization K (Fin (n + 1) → K)) : Fin n → K

The affine coordinates (x₁ / x₀, …, xₙ / x₀) of a projective point x, computed from its chosen representative; meaningful on the standard chart x₀ ≠ 0.

Equations

• CCDN.projectiveAffineCoordinates x j = x.rep j.succ / x.rep 0

theorem CCDN.affineCoordinateVector_ne_zero {K : Type u_1} [Field K] {n : ℕ} (a : Fin n → K) : Fin.cons 1 a ≠ 0

The vector (1, a₁, …, aₙ) is nonzero.

theorem CCDN.projectiveAffineCoordinates_injective {K : Type u_1} [Field K] {n : ℕ} {x y : Projectivization K (Fin (n + 1) → K)} (hx : x.rep 0 ≠ 0) (hy : y.rep 0 ≠ 0) (hxy : projectiveAffineCoordinates x = projectiveAffineCoordinates y) : x = y

Projective points with nonzero first coordinate are determined by their affine coordinates.

theorem CCDN.projectiveAffineCoordinates_zero {K : Type u_1} [Field K] {n d : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous d) (x : Projectivization K (Fin (n + 1) → K)) (hx : x.rep 0 ≠ 0) (hxf : x ∈ projectiveZeroLocus f) : (MvPolynomial.eval (projectiveAffineCoordinates x)) ((affineChart n) f) = 0

If a projective point x with nonzero first coordinate lies on the zero locus of a homogeneous polynomial f, then the dehomogenization of f vanishes at the affine coordinates of x.

def CCDN.affineProjectivePoint {K : Type u_2} [Field K] {n : ℕ} (a : Fin n → K) : Projectivization K (Fin (n + 1) → K)

The point [1 : a] of projective space on the standard chart.

Equations

• CCDN.affineProjectivePoint a = Projectivization.mk K (Fin.cons 1 a) ⋯

theorem CCDN.affineProjectivePoint_injective {K : Type u_2} [Field K] (n : ℕ) : Function.Injective affineProjectivePoint

The map a ↦ [1 : a] from affine space to projective space is injective.