mathlib documentation

linear_algebra.projective_space.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:

Other definitions #

Projects #

Everything in this file can be done for division_rings instead of fields, but this would require a significant refactor of the results from linear_algebra.finite_dimensional and its imports.

def projectivization_setoid (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K 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) [field K] [add_comm_group V] [module K 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} [field K] [add_comm_group V] [module K 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} [field K] [add_comm_group V] [module K 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} [field K] [add_comm_group V] [module K V] (v : {v // v 0}) :
@[protected, instance]
def projectivization.nonempty (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] [nontrivial V] :
@[protected]
noncomputable def projectivization.rep {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K 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} [field K] [add_comm_group V] [module K V] (v : K V) :
v.rep 0
@[simp]
theorem projectivization.mk_rep {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :
@[protected]
def projectivization.submodule {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :

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

Equations
Instances for projectivization.submodule
theorem projectivization.mk_eq_mk_iff (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] (v w : V) (hv : v 0) (hw : w 0) :
projectivization.mk K v hv = projectivization.mk K w hw ∃ (a : Kˣ), a w = v
theorem projectivization.exists_smul_eq_mk_rep (K : Type u_1) {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : V) (hv : v 0) :
∃ (a : Kˣ), a v = (projectivization.mk K v hv).rep
theorem projectivization.ind {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {P : K V → Prop} (h : ∀ (v : V) (h : v 0), P (projectivization.mk K v 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} [field K] [add_comm_group V] [module K V] (v : V) (hv : v 0) :
theorem projectivization.submodule_eq {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :
theorem projectivization.finrank_submodule {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :
@[protected, instance]
def projectivization.submodule.finite_dimensional {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :
noncomputable def projectivization.equiv_submodule (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] :

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} [field K] [add_comm_group V] [module K V] (H : submodule K V) (h : finite_dimensional.finrank K 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} [field K] [add_comm_group V] [module K V] (H : submodule K V) (h : finite_dimensional.finrank K H = 1) :
@[simp]
theorem projectivization.mk''_submodule {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (v : K V) :
def projectivization.map {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {L : Type u_3} {W : Type u_4} [field L] [add_comm_group W] [module L 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} [field K] [add_comm_group V] [module K V] {L : Type u_3} {W : Type u_4} [field L] [add_comm_group W] [module L W] {σ : K →+* L} {τ : L →+* K} [ring_hom_inv_pair σ τ] (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} [field K] [add_comm_group V] [module K V] :
@[simp]
theorem projectivization.map_comp {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {L : Type u_3} {W : Type u_4} [field L] [add_comm_group W] [module L W] {F : Type u_5} {U : Type u_6} [field F] [add_comm_group U] [module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [ring_hom_comp_triple σ τ γ] (f : V →ₛₗ[σ] W) (hf : function.injective f) (g : W →ₛₗ[τ] U) (hg : function.injective g) :