Projective Spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 hvwherev : Vandhv : v ≠ 0.projectivization.mk' K vwherev : { w : V // w ≠ 0 }.projectivization.mk'' H hwhereH : submodule K Vandh : finrank H = 1.
Other definitions #
- For
v : ℙ K V,v.submodulegives the corresponding submodule ofV. projectivization.equiv_submoduleis the equivalence betweenℙ K Vand{ H : submodule K V // finrank H = 1 }.- For
v : ℙ K V,v.rep : Vis a representative ofv.
def
projectivization_setoid
(K : Type u_1)
(V : Type u_2)
[division_ring K]
[add_comm_group V]
[module K V] :
The setoid whose quotient is the projectivization of V.
Equations
@[nolint]
def
projectivization
(K : Type u_1)
(V : Type u_2)
[division_ring 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
- ℙ K V = quotient (projectivization_setoid K V)
Instances for projectivization
def
projectivization.mk
(K : Type u_1)
{V : Type u_2}
[division_ring 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
- projectivization.mk K v hv = quotient.mk' ⟨v, hv⟩
def
projectivization.mk'
(K : Type u_1)
{V : Type u_2}
[division_ring 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}
[division_ring K]
[add_comm_group V]
[module K V]
(v : {v // v ≠ 0}) :
projectivization.mk' K v = projectivization.mk K ↑v _
@[protected, instance]
def
projectivization.nonempty
(K : Type u_1)
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
[nontrivial V] :
@[protected]
noncomputable
def
projectivization.rep
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
V
Choose a representative of v : projectivization K V in V.
Equations
- v.rep = ↑(quotient.out' v)
theorem
projectivization.rep_nonzero
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
@[simp]
theorem
projectivization.mk_rep
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
projectivization.mk K v.rep _ = v
@[protected]
def
projectivization.submodule
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
submodule K V
Consider an element of the projectivization as a submodule of V.
Equations
- v.submodule = quotient.lift_on' v (λ (v : {v // v ≠ 0}), submodule.span K {↑v}) projectivization.submodule._proof_1
Instances for ↥projectivization.submodule
theorem
projectivization.mk_eq_mk_iff
(K : Type u_1)
{V : Type u_2}
[division_ring 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.mk_eq_mk_iff'
(K : Type u_1)
{V : Type u_2}
[division_ring 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
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}
[division_ring K]
[add_comm_group V]
[module K V]
(v : V)
(hv : v ≠ 0) :
theorem
projectivization.ind
{K : Type u_1}
{V : Type u_2}
[division_ring 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}
[division_ring K]
[add_comm_group V]
[module K V]
(v : V)
(hv : v ≠ 0) :
(projectivization.mk K v hv).submodule = submodule.span K {v}
theorem
projectivization.submodule_eq
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
v.submodule = submodule.span K {v.rep}
theorem
projectivization.finrank_submodule
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
finite_dimensional.finrank K ↥(v.submodule) = 1
@[protected, instance]
def
projectivization.submodule.finite_dimensional
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
finite_dimensional K ↥(v.submodule)
theorem
projectivization.submodule_injective
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V] :
noncomputable
def
projectivization.equiv_submodule
(K : Type u_1)
(V : Type u_2)
[division_ring K]
[add_comm_group V]
[module K V] :
ℙ K V ≃ {H // finite_dimensional.finrank K ↥H = 1}
The equivalence between the projectivization and the collection of subspaces of dimension 1.
Equations
- projectivization.equiv_submodule K V = equiv.of_bijective (λ (v : ℙ K V), ⟨v.submodule, _⟩) _
noncomputable
def
projectivization.mk''
{K : Type u_1}
{V : Type u_2}
[division_ring 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
- projectivization.mk'' H h = ⇑((projectivization.equiv_submodule K V).symm) ⟨H, h⟩
@[simp]
theorem
projectivization.submodule_mk''
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(H : submodule K V)
(h : finite_dimensional.finrank K ↥H = 1) :
(projectivization.mk'' H h).submodule = H
@[simp]
theorem
projectivization.mk''_submodule
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
(v : ℙ K V) :
projectivization.mk'' v.submodule _ = v
def
projectivization.map
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
{L : Type u_3}
{W : Type u_4}
[division_ring L]
[add_comm_group W]
[module L W]
{σ : K →+* L}
(f : V →ₛₗ[σ] W)
(hf : function.injective ⇑f) :
An injective semilinear map of vector spaces induces a map on projective spaces.
Equations
- projectivization.map f hf = quotient.map' (λ (v : {v // v ≠ 0}), ⟨⇑f ↑v, _⟩) _
theorem
projectivization.map_injective
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
{L : Type u_3}
{W : Type u_4}
[division_ring 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}
[division_ring K]
[add_comm_group V]
[module K V] :
@[simp]
theorem
projectivization.map_comp
{K : Type u_1}
{V : Type u_2}
[division_ring K]
[add_comm_group V]
[module K V]
{L : Type u_3}
{W : Type u_4}
[division_ring 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) :
projectivization.map (g.comp f) _ = projectivization.map g hg ∘ projectivization.map f hf