nonZeroEquivProjectivizationProdUnits

English

There is a natural equivalence between the nonzero vectors and the product of the projectivization with the units of the field, i.e. { v ≠ 0 } ≃ ℙ_k(V) × kˣ.

Русский

Существует естественное эквивалентное отображение между ненулевыми векторами и произведением проективного пространства на единицы поля: {v ≠ 0} ≃ ℙ_k(V) × kˣ.

LaTeX

$$(k : Type*) → (V : Type*) → Equiv (Subtype fun v => v ≠ 0) (Projectivization k V × Units k)$$

Lean4

/-- The non-zero elements of `V` are equivalent to the product of `ℙ k V` with the units of `k`. -/
noncomputable def nonZeroEquivProjectivizationProdUnits : { v : V // v ≠ 0 } ≃ ℙ k V × kˣ :=
  let e :=
    MulAction.selfEquivOrbitsQuotientProd <| fun b ↦ by
      rw [(Units.nonZeroSubMul k V).stabilizer_of_subMul, Module.stabilizer_units_eq_bot_of_ne_zero k b.property]
  e.trans (Equiv.prodCongrLeft (fun _ ↦ (equivQuotientOrbitRel k V).symm))

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