Theorems · Definition · geometry

Projectivization.lift

{K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {α : Type u_3} →
            (f : { v // v ≠ 0 } → α) →
              (∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) → Projectivization K V → α

A function on non-zero vectors which is independent of scale, descends to a function on the projectivization.

Defined in

Mathlib.LinearAlgebra.Projectivization.Basic

Cited by

3 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModule