lift — Mathlib

English

A universally quantified statement about lifting to projectivization.

Русский

Универсальная формулировка лифта к проективному пространству.

LaTeX

$$$ \text{lift} : \{ f : (\{ v : V // v \neq 0 \} \to \alpha) \} \to (\mathbb{P}_K V \to \alpha) $ with hf ensuring well-definedness.$$

Lean4

/-- A function on non-zero vectors which is independent of scale, descends to a function on the
projectivization. -/
protected def lift {α : Type*} (f : { v : V // v ≠ 0 } → α)
    (hf : ∀ (a b : { v : V // v ≠ 0 }) (t : K), a = t • (b : V) → f a = f b) (x : ℙ K V) : α :=
  Quotient.lift f (by rintro ⟨-, hv⟩ ⟨w, hw⟩ ⟨⟨t, -⟩, rfl⟩; exact hf ⟨_, hv⟩ ⟨w, hw⟩ t rfl) x

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