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) [DivisionRing K] [AddCommGroup V] [Module K V] : Setoid { 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 termℙ : Lean.ParserDescr

def Projectivization.mk (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : ℙ 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 ≠ 0 }) : ℙ 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 ≠ 0 }) : Projectivization.mk' K v = Projectivization.mk K ↑v (_ : ↑v ≠ 0)

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

noncomputable def Projectivization.rep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : ℙ 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 : ℙ K V) : Projectivization.rep v ≠ 0

@[simp]

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

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

theorem Projectivization.ind {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup 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} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : Projectivization.submodule (Projectivization.mk K v hv) = Submodule.span K {v}

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

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

instance Projectivization.instFiniteDimensionalSubtypeMemSubmoduleToSemiringToDivisionSemiringToAddCommMonoidInstMembershipSetLikeSubmoduleAddCommGroupToRingModule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : ℙ K V) : FiniteDimensional K { x // x ∈ Projectivization.submodule v }

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] : ℙ K V ≃ { H // FiniteDimensional.finrank K { x // x ∈ 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 : FiniteDimensional.finrank K { x // x ∈ H } = 1) : ℙ 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 : FiniteDimensional.finrank K { x // x ∈ H } = 1) : Projectivization.submodule (Projectivization.mk'' H h) = H

@[simp]

theorem Projectivization.mk''_submodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : ℙ K V) : Projectivization.mk'' (Projectivization.submodule v) (_ : FiniteDimensional.finrank K { x // x ∈ Projectivization.submodule v } = 1) = 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) : ℙ K V → ℙ 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) : Projectivization.map f hf (Projectivization.mk K v hv) = Projectivization.mk L (↑f v) (_ : ↑f v ≠ 0)

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 (Projectivization.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] : Projectivization.map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) = id

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} [Field 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) : Projectivization.map (LinearMap.comp g f) (_ : Function.Injective (↑g ∘ fun x => ↑f x)) = Projectivization.map g hg ∘ Projectivization.map f hf