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.

Equations

• projectivizationSetoid K V = Setoid.comap Subtype.val (MulAction.orbitRel Kˣ 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.

Equations

• Projectivization K V = Quotient (projectivizationSetoid K V)

def LinearAlgebra.Projectivization.termℙ : Lean.ParserDescr

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

Equations

• LinearAlgebra.Projectivization.termℙ = Lean.ParserDescr.node `LinearAlgebra.Projectivization.termℙ 1024 (Lean.ParserDescr.symbol "ℙ")

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.

Equations

• Projectivization.mk K v hv = Quotient.mk'' { val := v, property := hv }

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.

Equations

• Projectivization.mk' K v = Quotient.mk'' v

@[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 }) : Projectivization.mk' K v = Projectivization.mk K ↑v ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• Projectivization.rep v = ↑(Quotient.out' v)

theorem Projectivization.rep_nonzero {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization 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 : Projectivization K V) : Projectivization.mk K (Projectivization.rep v) ⋯ = 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.

Equations

• Projectivization.submodule v = Quotient.liftOn' v (fun (v : { v : V // v ≠ 0 }) => Submodule.span K {↑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 : 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 : V) (w : V) (hv : v ≠ 0) (hw : w ≠ 0) : Projectivization.mk K v hv = Projectivization.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 = 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 : Projectivization K V → Prop} (h : ∀ (v : V) (h : v ≠ 0), P (Projectivization.mk K v h)) (p : Projectivization 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 : Projectivization 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 : Projectivization K V) : FiniteDimensional.finrank K ↥(Projectivization.submodule v) = 1

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

Equations

• ⋯ = ⋯

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 // FiniteDimensional.finrank K ↥H = 1 }

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

Equations

• Projectivization.equivSubmodule K V = (Equiv.ofInjective Projectivization.submodule ⋯).trans (Equiv.subtypeEquiv (Equiv.refl (Submodule K V)) ⋯)

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 ↥H = 1) : Projectivization K V

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

Equations

• Projectivization.mk'' H h = (Projectivization.equivSubmodule K V).symm { val := H, property := h }

@[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 ↥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 : Projectivization K V) : Projectivization.mk'' (Projectivization.submodule v) ⋯ = 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.

Equations

• Projectivization.map f hf = Quotient.map' (fun (v : { v : V // v ≠ 0 }) => { val := f ↑v, property := ⋯ }) ⋯

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) ⋯

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 ⋯ = 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) ⋯ = Projectivization.map g hg ∘ Projectivization.map f hf