Theorems · Definition · geometry

Projectivization.map

{K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {L : Type u_3} →
            {W : Type u_4} →
              [inst_3 : DivisionRing L] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module L W] →
                    {σ : K →+* L} →
                      (f : V →ₛₗ[σ] W) → Function.Injective ⇑f → Projectivization K V → Projectivization L W

An injective semilinear map of vector spaces induces a map on projective spaces.

Defined in

Mathlib.LinearAlgebra.Projectivization.Basic

Cited by

7 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleDivisionRingAddCommGroupModule