Documentation

Mathlib.LinearAlgebra.Projectivization.Subspace

Subspaces of Projective Space #

In this file we define subspaces of a projective space, and show that the subspaces of a projective space form a complete lattice under inclusion.

Implementation Details #

A subspace of a projective space ℙ K V is defined to be a structure consisting of a subset of ℙ K V such that if two nonzero vectors in V determine points in ℙ K V which are in the subset, and the sum of the two vectors is nonzero, then the point determined by the sum of the two vectors is also in the subset.

Results #

Future Work #

theorem Projectivization.Subspace.ext {K : Type u_1} {V : Type u_2} :
∀ {inst : Field K} {inst_1 : AddCommGroup V} {inst_2 : Module K V} (x y : Projectivization.Subspace K V), x.carrier = y.carrierx = y
theorem Projectivization.Subspace.ext_iff {K : Type u_1} {V : Type u_2} :
∀ {inst : Field K} {inst_1 : AddCommGroup V} {inst_2 : Module K V} (x y : Projectivization.Subspace K V), x = y x.carrier = y.carrier
structure Projectivization.Subspace (K : Type u_1) (V : Type u_2) [Field K] [AddCommGroup V] [Module K V] :
Type u_2

A subspace of a projective space is a structure consisting of a set of points such that: If two nonzero vectors determine points which are in the set, and the sum of the two vectors is nonzero, then the point determined by the sum is also in the set.

Instances For
    theorem Projectivization.Subspace.mem_add' {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (self : Projectivization.Subspace K V) (v : V) (w : V) (hv : v 0) (hw : w 0) (hvw : v + w 0) :
    Projectivization.mk K v hv self.carrierProjectivization.mk K w hw self.carrierProjectivization.mk K (v + w) hvw self.carrier

    The addition rule.

    Equations
    • Projectivization.Subspace.instSetLike = { coe := Projectivization.Subspace.carrier, coe_injective' := }
    @[simp]
    theorem Projectivization.Subspace.mem_carrier_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A : Projectivization.Subspace K V) (x : Projectivization K V) :
    x A.carrier x A
    theorem Projectivization.Subspace.mem_add {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (T : Projectivization.Subspace K V) (v : V) (w : V) (hv : v 0) (hw : w 0) (hvw : v + w 0) :
    Projectivization.mk K v hv TProjectivization.mk K w hw TProjectivization.mk K (v + w) hvw T
    inductive Projectivization.Subspace.spanCarrier {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) :

    The span of a set of points in a projective space is defined inductively to be the set of points which contains the original set, and contains all points determined by the (nonzero) sum of two nonzero vectors, each of which determine points in the span.

    Instances For

      The span of a set of points in projective space is a subspace.

      Equations
      Instances For

        The span of a set of points contains the set of points.

        def Projectivization.Subspace.gi {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] :
        GaloisInsertion Projectivization.Subspace.span SetLike.coe

        The span of a set of points is a Galois insertion between sets of points of a projective space and subspaces of the projective space.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]

          The span of a subspace is the subspace.

          The infimum of two subspaces exists.

          Equations

          Infimums of arbitrary collections of subspaces exist.

          Equations

          The subspaces of a projective space form a complete lattice.

          Equations
          Equations
          • Projectivization.Subspace.subspaceInhabited = { default := }
          @[simp]

          The span of the empty set is the bottom of the lattice of subspaces.

          @[simp]

          The span of the entire projective space is the top of the lattice of subspaces.

          The span of a set of points is contained in a subspace if and only if the set of points is contained in the subspace.

          theorem Projectivization.Subspace.monotone_span {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] :
          Monotone Projectivization.Subspace.span

          If a set of points is a subset of another set of points, then its span will be contained in the span of that set.

          The supremum of two subspaces is equal to the span of their union.

          theorem Projectivization.Subspace.span_iUnion {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {ι : Sort u_3} (s : ιSet (Projectivization K V)) :
          Projectivization.Subspace.span (⋃ (i : ι), s i) = ⨆ (i : ι), Projectivization.Subspace.span (s i)

          The supremum of a collection of subspaces is equal to the span of the union of the collection.

          The supremum of a subspace and the span of a set of points is equal to the span of the union of the subspace and the set of points.

          theorem Projectivization.Subspace.mem_span {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} (u : Projectivization K V) :

          A point in a projective space is contained in the span of a set of points if and only if the point is contained in all subspaces of the projective space which contain the set of points.

          The span of a set of points in a projective space is equal to the infimum of the collection of subspaces which contain the set.

          If a set of points in projective space is contained in a subspace, and that subspace is contained in the span of the set of points, then the span of the set of points is equal to the subspace.

          The spans of two sets of points in a projective space are equal if and only if each set of points is contained in the span of the other set.