@[reducible, inline]

abbrev ProjectiveSpace.Space (n : ℕ) (k : Type u_1) [Field k] : Type u_1

$n$-dimensional projective space $\mathbb{P}^n(k)$ over $k$, realised as the projectivization of $k^{n+1}$.

def ProjectiveSpace.mk (n : ℕ) (k : Type u_1) [Field k] (v : Fin (n + 1) → k) (hv : v ≠ 0) : Space n k

The projective point $[v_0 : \cdots : v_n] \in \mathbb{P}^n(k)$ associated to a nonzero vector $v \in k^{n+1}$.

noncomputable def ProjectiveSpace.coord (n : ℕ) (k : Type u_1) [Field k] (P : Space n k) : Fin (n + 1) → k

A choice of homogeneous coordinates representing a projective point.

theorem ProjectiveSpace.coord_ne_zero (n : ℕ) (k : Type u_1) [Field k] (P : Space n k) : coord n k P ≠ 0

Homogeneous coordinates of a projective point are nonzero.

theorem ProjectiveSpace.mk_eq_mk_iff (n : ℕ) (k : Type u_1) [Field k] (v w : Fin (n + 1) → k) (hv : v ≠ 0) (hw : w ≠ 0) : mk n k v hv = mk n k w hw ↔ ∃ (a : kˣ), a • w = v

Two nonzero vectors in $k^{n+1}$ determine the same projective point iff they differ by a nonzero scalar.

theorem ProjectiveSpace.mk_eq_mk_iff' (n : ℕ) (k : Type u_1) [Field k] (v w : Fin (n + 1) → k) (hv : v ≠ 0) (hw : w ≠ 0) : mk n k v hv = mk n k w hw ↔ ∃ (a : k), a • w = v

Variant of mk_eq_mk_iff allowing the scalar to range over $k$; since $w \neq 0$, the scalar is automatically a unit.

@[simp]

theorem ProjectiveSpace.mk_coord (n : ℕ) (k : Type u_1) [Field k] (v : Fin (n + 1) → k) (hv : v ≠ 0) : Projectivization.mk k (coord n k (mk n k v hv)) ⋯ = mk n k v hv

Taking representative coordinates and forming a projective point recovers the original projective point.

@[reducible, inline]

abbrev ProjectiveSpace.Plane (k : Type u_1) [Field k] : Type u_1

The projective plane $\mathbb{P}^2(k)$.

@[reducible, inline]

abbrev ProjectiveSpace.Line (k : Type u_1) [Field k] : Type u_1

The projective line $\mathbb{P}^1(k)$.