English
Let a point in the projective space ℙ_K(V) be represented by a nonzero vector v ∈ V. Then the corresponding subspace of V is the 1‑dimensional subspace generated by v, i.e. K·v.
Русский
Пусть точка в проективном пространстве ℙ_K(V) задана представителем v ≠ 0 в V. Тогда соответствующее подпространство V состоит из одномерного подпространства, порождаемого v, т.е. K·v.
LaTeX
$$$ v \in \mathbb{P}_K(V) \Rightarrow v.\mathrm{submodule} = \operatorname{span}_K\{ v.\mathrm{rep} \} $$$
Lean4
/-- Consider an element of the projectivization as a submodule of `V`. -/
protected def submodule (v : ℙ K V) : Submodule K V :=
(Quotient.liftOn' v fun v => K ∙ (v : V)) <|
by
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨x, rfl : x • b = a⟩
exact Submodule.span_singleton_group_smul_eq _ x _
