Documentation

Mathlib.LinearAlgebra.Projectivization.Basic

Projective Spaces #

This file contains the definition of the projectivization of a vector space over a field, as well as the bijection between said projectivization and the collection of all one dimensional subspaces of the vector space.

Notation #

ℙ K V is localized notation for Projectivization K V, the projectivization of a K-vector space V.

Constructing terms of ℙ K V. #

We have three ways to construct terms of ℙ K V:

Other definitions #

def projectivizationSetoid (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] :
Setoid { v : V // v 0 }

The setoid whose quotient is the projectivization of V.

Equations
Instances For
    def Projectivization (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] :
    Type u_2

    The projectivization of the K-vector space V. The notation ℙ K V is preferred.

    Equations
    Instances For

      We define notations ℙ K V for the projectivization of the K-vector space V.

      Equations
      Instances For
        def Projectivization.mk (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v 0) :

        Construct an element of the projectivization from a nonzero vector.

        Equations
        Instances For
          def Projectivization.mk' (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v : V // v 0 }) :

          A variant of Projectivization.mk in terms of a subtype. mk is preferred.

          Equations
          Instances For
            @[simp]
            theorem Projectivization.mk'_eq_mk (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v : V // v 0 }) :
            noncomputable def Projectivization.rep {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) :
            V

            Choose a representative of v : Projectivization K V in V.

            Equations
            Instances For
              def Projectivization.submodule {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) :

              Consider an element of the projectivization as a submodule of V.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Projectivization.mk_eq_mk_iff (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (w : V) (hv : v 0) (hw : w 0) :
                Projectivization.mk K v hv = Projectivization.mk K w hw ∃ (a : Kˣ), a w = v
                theorem Projectivization.mk_eq_mk_iff' (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (w : V) (hv : v 0) (hw : w 0) :
                Projectivization.mk K v hv = Projectivization.mk K w hw ∃ (a : K), a w = v

                Two nonzero vectors go to the same point in projective space if and only if one is a scalar multiple of the other.

                theorem Projectivization.exists_smul_eq_mk_rep (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v 0) :
                theorem Projectivization.ind {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {P : Projectivization K VProp} (h : ∀ (v : V) (h : v 0), P (Projectivization.mk K v h)) (p : Projectivization K V) :
                P p

                An induction principle for Projectivization. Use as induction v using Projectivization.ind.

                @[simp]
                theorem Projectivization.submodule_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v 0) :
                theorem Projectivization.submodule_injective {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] :
                Function.Injective Projectivization.submodule
                noncomputable def Projectivization.equivSubmodule (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] :

                The equivalence between the projectivization and the collection of subspaces of dimension 1.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  noncomputable def Projectivization.mk'' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (H : Submodule K V) (h : FiniteDimensional.finrank K H = 1) :

                  Construct an element of the projectivization from a subspace of dimension 1.

                  Equations
                  Instances For
                    def Projectivization.map {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) :

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Projectivization.map_mk {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) (v : V) (hv : v 0) :
                      theorem Projectivization.map_injective {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective f) :

                      Mapping with respect to a semilinear map over an isomorphism of fields yields an injective map on projective spaces.

                      @[simp]
                      theorem Projectivization.map_id {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] :
                      theorem Projectivization.map_comp {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {F : Type u_5} {U : Type u_6} [Field F] [AddCommGroup U] [Module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [RingHomCompTriple σ τ γ] (f : V →ₛₗ[σ] W) (hf : Function.Injective f) (g : W →ₛₗ[τ] U) (hg : Function.Injective g) :