English
There is a natural equivalence between the projectivization ℙ_K(V) and the set of 1-dimensional subspaces of V.
Русский
Существует естественное биективное соответствие между ℙ_K(V) и множеством одномерных подпространств V.
LaTeX
$$$\mathbb{P}_K(V) \simeq \{ H \le V \mid \operatorname{finrank} H = 1 \}$$$
Lean4
/-- The equivalence between the projectivization and the
collection of subspaces of dimension 1. -/
noncomputable def equivSubmodule : ℙ K V ≃ { H : Submodule K V // finrank K H = 1 } :=
(Equiv.ofInjective _ submodule_injective).trans <|
.subtypeEquiv (.refl _) fun H ↦
by
refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩
use mk K (v : V) (Subtype.coe_injective.ne hv₀)
rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]
refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_
rcases hv ⟨x, hx⟩ with ⟨c, hc⟩
exact ⟨c, congr_arg Subtype.val hc⟩
