# mathlib3documentation

linear_algebra.projective_space.basic

# Projective Spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the definition of the projectivization of a vector space over a field, as well as the bijection between said projectivization and the collection of all one dimensional subspaces of the vector space.

## Notation #

ℙ K V is notation for projectivization K V, the projectivization of a K-vector space V.

## Constructing terms of ℙ K V. #

We have three ways to construct terms of ℙ K V:

• projectivization.mk K v hv where v : V and hv : v ≠ 0.
• projectivization.mk' K v where v : { w : V // w ≠ 0 }.
• projectivization.mk'' H h where H : submodule K V and h : finrank H = 1.

## Other definitions #

• For v : ℙ K V, v.submodule gives the corresponding submodule of V.
• projectivization.equiv_submodule is the equivalence between ℙ K V and { H : submodule K V // finrank H = 1 }.
• For v : ℙ K V, v.rep : V is a representative of v.
def projectivization_setoid (K : Type u_1) (V : Type u_2) [ V] :
setoid {v // v 0}

The setoid whose quotient is the projectivization of V.

Equations
@[nolint]
def projectivization (K : Type u_1) (V : Type u_2) [ V] :
Type u_2

The projectivization of the K-vector space V. The notation ℙ K V is preferred.

Equations
Instances for projectivization
def projectivization.mk (K : Type u_1) {V : Type u_2} [ V] (v : V) (hv : v 0) :
K V

Construct an element of the projectivization from a nonzero vector.

Equations
def projectivization.mk' (K : Type u_1) {V : Type u_2} [ V] (v : {v // v 0}) :
K V

A variant of projectivization.mk in terms of a subtype. mk is preferred.

Equations
@[simp]
theorem projectivization.mk'_eq_mk (K : Type u_1) {V : Type u_2} [ V] (v : {v // v 0}) :
@[protected, instance]
def projectivization.nonempty (K : Type u_1) {V : Type u_2} [ V] [nontrivial V] :
@[protected]
noncomputable def projectivization.rep {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
V

Choose a representative of v : projectivization K V in V.

Equations
theorem projectivization.rep_nonzero {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
v.rep 0
@[simp]
theorem projectivization.mk_rep {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
_ = v
@[protected]
def projectivization.submodule {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
V

Consider an element of the projectivization as a submodule of V.

Equations
• v.submodule = (λ (v : {v // v 0}), {v}) projectivization.submodule._proof_1
Instances for ↥projectivization.submodule
theorem projectivization.mk_eq_mk_iff (K : Type u_1) {V : Type u_2} [ V] (v w : V) (hv : v 0) (hw : w 0) :
hv = hw (a : Kˣ), a w = v
theorem projectivization.mk_eq_mk_iff' (K : Type u_1) {V : Type u_2} [ V] (v w : V) (hv : v 0) (hw : w 0) :
hv = hw (a : K), a w = v

Two nonzero vectors go to the same point in projective space if and only if one is a scalar multiple of the other.

theorem projectivization.exists_smul_eq_mk_rep (K : Type u_1) {V : Type u_2} [ V] (v : V) (hv : v 0) :
(a : Kˣ), a v = hv).rep
theorem projectivization.ind {K : Type u_1} {V : Type u_2} [ V] {P : K V Prop} (h : (v : V) (h : v 0), P h)) (p : K V) :
P p

An induction principle for projectivization. Use as induction v using projectivization.ind.

@[simp]
theorem projectivization.submodule_mk {K : Type u_1} {V : Type u_2} [ V] (v : V) (hv : v 0) :
hv).submodule = {v}
theorem projectivization.submodule_eq {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
theorem projectivization.finrank_submodule {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
@[protected, instance]
def projectivization.submodule.finite_dimensional {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
theorem projectivization.submodule_injective {K : Type u_1} {V : Type u_2} [ V] :
noncomputable def projectivization.equiv_submodule (K : Type u_1) (V : Type u_2) [ V] :
K V {H //

The equivalence between the projectivization and the collection of subspaces of dimension 1.

Equations
noncomputable def projectivization.mk'' {K : Type u_1} {V : Type u_2} [ V] (H : V) (h : = 1) :
K V

Construct an element of the projectivization from a subspace of dimension 1.

Equations
@[simp]
theorem projectivization.submodule_mk'' {K : Type u_1} {V : Type u_2} [ V] (H : V) (h : = 1) :
= H
@[simp]
theorem projectivization.mk''_submodule {K : Type u_1} {V : Type u_2} [ V] (v : K V) :
def projectivization.map {K : Type u_1} {V : Type u_2} [ V] {L : Type u_3} {W : Type u_4} [ W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : function.injective f) :
K V L W

An injective semilinear map of vector spaces induces a map on projective spaces.

Equations
theorem projectivization.map_injective {K : Type u_1} {V : Type u_2} [ V] {L : Type u_3} {W : Type u_4} [ W] {σ : K →+* L} {τ : L →+* K} [ τ] (f : V →ₛₗ[σ] W) (hf : function.injective f) :

Mapping with respect to a semilinear map over an isomorphism of fields yields an injective map on projective spaces.

@[simp]
theorem projectivization.map_id {K : Type u_1} {V : Type u_2} [ V] :
@[simp]
theorem projectivization.map_comp {K : Type u_1} {V : Type u_2} [ V] {L : Type u_3} {W : Type u_4} [ W] {F : Type u_5} {U : Type u_6} [field F] [ U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [ γ] (f : V →ₛₗ[σ] W) (hf : function.injective f) (g : W →ₛₗ[τ] U) (hg : function.injective g) :