# Documentation

Mathlib.LinearAlgebra.ProjectiveSpace.Basic

# Projective Spaces #

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.equivSubmodule 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 projectivizationSetoid (K : Type u_1) (V : Type u_2) [] [] [Module K V] :
Setoid { v // v 0 }

The setoid whose quotient is the projectivization of V.

Instances For
def Projectivization (K : Type u_1) (V : Type u_2) [] [] [Module K V] :
Type u_2

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

Instances For
Instances For
def Projectivization.mk (K : Type u_1) {V : Type u_2} [] [] [Module K V] (v : V) (hv : v 0) :
K V

Construct an element of the projectivization from a nonzero vector.

Instances For
def Projectivization.mk' (K : Type u_1) {V : Type u_2} [] [] [Module K V] (v : { v // v 0 }) :
K V

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

Instances For
@[simp]
theorem Projectivization.mk'_eq_mk (K : Type u_1) {V : Type u_2} [] [] [Module K V] (v : { v // v 0 }) :
= Projectivization.mk K v (_ : v 0)
instance Projectivization.instNonemptyProjectivization (K : Type u_1) {V : Type u_2} [] [] [Module K V] [] :
noncomputable def Projectivization.rep {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
V

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

Instances For
theorem Projectivization.rep_nonzero {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
@[simp]
theorem Projectivization.mk_rep {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
Projectivization.mk K () (_ : ) = v
def Projectivization.submodule {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :

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

Instances For
theorem Projectivization.mk_eq_mk_iff (K : Type u_1) {V : Type u_2} [] [] [Module K V] (v : V) (w : V) (hv : v 0) (hw : w 0) :
= a, a w = v
theorem Projectivization.mk_eq_mk_iff' (K : Type u_1) {V : Type u_2} [] [] [Module K V] (v : V) (w : V) (hv : v 0) (hw : w 0) :
= a, 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} [] [] [Module K V] (v : V) (hv : v 0) :
a, a v =
theorem Projectivization.ind {K : Type u_1} {V : Type u_2} [] [] [Module K V] {P : K VProp} (h : (v : V) → (h : v 0) → P ()) (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} [] [] [Module K V] (v : V) (hv : v 0) :
theorem Projectivization.submodule_eq {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
theorem Projectivization.finrank_submodule {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
theorem Projectivization.submodule_injective {K : Type u_1} {V : Type u_2} [] [] [Module K V] :
Function.Injective Projectivization.submodule
noncomputable def Projectivization.equivSubmodule (K : Type u_1) (V : Type u_2) [] [] [Module K V] :
K V { H // FiniteDimensional.finrank K { x // x H } = 1 }

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

Instances For
noncomputable def Projectivization.mk'' {K : Type u_1} {V : Type u_2} [] [] [Module K V] (H : ) (h : FiniteDimensional.finrank K { x // x H } = 1) :
K V

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

Instances For
@[simp]
theorem Projectivization.submodule_mk'' {K : Type u_1} {V : Type u_2} [] [] [Module K V] (H : ) (h : FiniteDimensional.finrank K { x // x H } = 1) :
@[simp]
theorem Projectivization.mk''_submodule {K : Type u_1} {V : Type u_2} [] [] [Module K V] (v : K V) :
def Projectivization.map {K : Type u_1} {V : Type u_2} [] [] [Module K V] {L : Type u_3} {W : Type u_4} [] [] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : ) :
K V L W

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

Instances For
theorem Projectivization.map_mk {K : Type u_1} {V : Type u_2} [] [] [Module K V] {L : Type u_3} {W : Type u_4} [] [] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : ) (v : V) (hv : v 0) :
Projectivization.map f hf () = Projectivization.mk L (f v) (_ : f v 0)
theorem Projectivization.map_injective {K : Type u_1} {V : Type u_2} [] [] [Module K V] {L : Type u_3} {W : Type u_4} [] [] [Module L W] {σ : K →+* L} {τ : L →+* K} [] (f : V →ₛₗ[σ] W) (hf : ) :

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} [] [] [Module K V] :
Projectivization.map LinearMap.id (_ : ) = id
theorem Projectivization.map_comp {K : Type u_1} {V : Type u_2} [] [] [Module K V] {L : Type u_3} {W : Type u_4} [] [] [Module L W] {F : Type u_5} {U : Type u_6} [] [] [Module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [] (f : V →ₛₗ[σ] W) (hf : ) (g : W →ₛₗ[τ] U) (hg : ) :
Projectivization.map () (_ : Function.Injective (g fun x => f x)) =