def ProjectiveSpace (k : Type u_1) [DivisionRing k] (n : ℕ) : Type u_1

Projective n-space P^n(k) as the projectivization of k^{n+1}.

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

Form the projective point [v] in P^n(k) from a nonzero vector v ∈ k^{n+1}.

def ProjectiveSpace.quotientMap {k : Type u_1} [DivisionRing k] {n : ℕ} : { v : Fin (n + 1) → k // v ≠ 0 } → ProjectiveSpace k n

The quotient map (k^{n+1} \ {0}) → P^n(k) sending a nonzero vector to its line.

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

Two nonzero vectors define the same projective point iff they differ by a nonzero scalar (unit version).

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

Two nonzero vectors define the same projective point iff they differ by a scalar (field-element version).

theorem ProjectiveSpace.quotientMap_surjective {k : Type u_1} [DivisionRing k] {n : ℕ} : Function.Surjective quotientMap

The quotient map (k^{n+1} \ {0}) → P^n(k) is surjective.

noncomputable def ProjectiveSpace.rep {k : Type u_1} [DivisionRing k] {n : ℕ} (p : ProjectiveSpace k n) : Fin (n + 1) → k

A choice of representative vector for a projective point.

theorem ProjectiveSpace.rep_nonzero {k : Type u_1} [DivisionRing k] {n : ℕ} (p : ProjectiveSpace k n) : p.rep ≠ 0

The chosen representative of a projective point is nonzero.

@[simp]

theorem ProjectiveSpace.mk_rep {k : Type u_1} [DivisionRing k] {n : ℕ} (p : ProjectiveSpace k n) : mk p.rep ⋯ = p

Forming a projective point from its chosen representative recovers the original point.

instance ProjectiveSpace.instNonempty {k : Type u_1} [DivisionRing k] {n : ℕ} : Nonempty (ProjectiveSpace k n)

Projective n-space P^n(k) is nonempty.