equivQuotientOrbitRel — Mathlib

English

There is a natural equivalence between ℙ_k(V) and the quotient of nonzero vectors by the kˣ action; i.e. projectivization equals orbit space under scalar multiplication by units.

Русский

Существует естественное эквиваленцное отображение между ℙ_k(V) и фактор-м множеством ненулевых векторов по действию kˣ; то есть проективное пространство — орбитное пространство под скалярами.

LaTeX

$$$ \mathbb{P}_k(V) \simeq \mathrm{Quotient} (\mathrm{MulAction.orbitRel}\ k^\times \{ v : V \setminus \{0\} \})$$$

Lean4

/-- `ℙ k V` is equivalent to the quotient of the non-zero elements of `V` by `kˣ`. -/
def equivQuotientOrbitRel : ℙ k V ≃ Quotient (MulAction.orbitRel kˣ { v : V // v ≠ 0 }) :=
  Quotient.congr (Equiv.refl _) (fun x y ↦ (Units.orbitRel_nonZero_iff k V x y).symm)

Похожие утверждения