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 localized 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) [DivisionRing K] [AddCommGroup V] [Module K V] : Setoid { v : V // v ≠ 0 }

The setoid whose quotient is the projectivization of V.

def Projectivization (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Type u_2

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

def LinearAlgebra.Projectivization.termℙ : Lean.ParserDescr

We define notations ℙ K V for the projectivization of the K-vector space V.

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

Construct an element of the projectivization from a nonzero vector.

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

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

@[simp]

theorem Projectivization.mk'_eq_mk (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v : V // v ≠ 0 }) : mk' K v = mk K ↑v ⋯

instance Projectivization.instNonemptyOfNontrivial (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [Nontrivial V] : Nonempty (Projectivization K V)

def Projectivization.lift {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {α : Type u_3} (f : { v : V // v ≠ 0 } → α) (hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (x : Projectivization K V) : α

A function on non-zero vectors which is independent of scale, descends to a function on the projectivization.

@[simp]

theorem Projectivization.lift_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {α : Type u_3} (f : { v : V // v ≠ 0 } → α) (hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (v : V) (hv : v ≠ 0) : Projectivization.lift f hf (mk K v hv) = f ⟨v, hv⟩

noncomputable def Projectivization.rep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : V

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

theorem Projectivization.rep_nonzero {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : v.rep ≠ 0

@[simp]

theorem Projectivization.mk_rep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : mk K v.rep ⋯ = v

def Projectivization.submodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Submodule K V

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

theorem Projectivization.mk_eq_mk_iff (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ ∃ (a : Kˣ), a • w = v

theorem Projectivization.mk_eq_mk_iff' (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w 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} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : ∃ (a : Kˣ), a • v = (mk K v hv).rep

theorem Projectivization.ind {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {P : Projectivization K V → Prop} (h : ∀ (v : V) (h : v ≠ 0), P (mk K v h)) (p : Projectivization K V) : P p

An induction principle for Projectivization. Use as induction v.

@[simp]

theorem Projectivization.submodule_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : (mk K v hv).submodule = Submodule.span K {v}

theorem Projectivization.submodule_eq {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : v.submodule = Submodule.span K {v.rep}

theorem Projectivization.finrank_submodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Module.finrank K ↥v.submodule = 1

instance Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : FiniteDimensional K ↥v.submodule

theorem Projectivization.submodule_injective {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : Function.Injective Projectivization.submodule

noncomputable def Projectivization.equivSubmodule (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Projectivization K V ≃ { H : Submodule K V // Module.finrank K ↥H = 1 }

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

noncomputable def Projectivization.mk'' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (H : Submodule K V) (h : Module.finrank K ↥H = 1) : Projectivization K V

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

@[simp]

theorem Projectivization.submodule_mk'' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (H : Submodule K V) (h : Module.finrank K ↥H = 1) : (mk'' H h).submodule = H

@[simp]

theorem Projectivization.mk''_submodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : mk'' v.submodule ⋯ = v

def Projectivization.map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) : Projectivization K V → Projectivization L W

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

theorem Projectivization.map_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (v : V) (hv : v ≠ 0) : map f hf (mk K v hv) = mk L (f v) ⋯

theorem Projectivization.map_injective {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) : Function.Injective (map f 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} [DivisionRing K] [AddCommGroup V] [Module K V] : map LinearMap.id ⋯ = id

@[simp]

theorem Projectivization.map_comp {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {F : Type u_5} {U : Type u_6} [DivisionRing F] [AddCommGroup U] [Module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [RingHomCompTriple σ τ γ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (g : W →ₛₗ[τ] U) (hg : Function.Injective ⇑g) (hgf : Function.Injective ⇑(g ∘ₛₗ f) := ⋯) : map (g ∘ₛₗ f) hgf = map g hg ∘ map f hf