mathlib documentation

linear_algebra.projective_space.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 #

@[ext]
structure projectivization.subspace (K : Type u_1) (V : Type u_2) [field K] [add_comm_group 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 projectivization.subspace
theorem projectivization.subspace.ext_iff {K : Type u_1} {V : Type u_2} {_inst_1 : field K} {_inst_2 : add_comm_group V} {_inst_3 : module K V} (x y : projectivization.subspace K V) :
theorem projectivization.subspace.ext {K : Type u_1} {V : Type u_2} {_inst_1 : field K} {_inst_2 : add_comm_group V} {_inst_3 : module K V} (x y : projectivization.subspace K V) (h : x.carrier = y.carrier) :
x = y
@[simp]
theorem projectivization.subspace.mem_carrier_iff {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (A : projectivization.subspace K V) (x : K V) :
x A.carrier x A
theorem projectivization.subspace.mem_add {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (T : projectivization.subspace K 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.span_carrier {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (S : set ( K V)) :
set ( 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.

def projectivization.subspace.span {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (S : set ( K V)) :

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

Equations
theorem projectivization.subspace.subset_span {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] (S : set ( K V)) :

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

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
@[simp]

The span of a subspace is the subspace.

@[protected, instance]
def projectivization.subspace.has_inf {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

The infimum of two subspaces exists.

Equations
@[protected, instance]
def projectivization.subspace.has_Inf {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

Infimums of arbitrary collections of subspaces exist.

Equations
@[protected, instance]

The subspaces of a projective space form a complete lattice.

Equations
@[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.

theorem projectivization.subspace.span_le_subspace_iff {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {S : set ( K V)} {W : projectivization.subspace K V} :

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.

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_Union {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {ι : Sort u_3} (s : ι → set ( 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] [add_comm_group V] [module K V] {S : set ( K V)} (u : 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.

theorem projectivization.subspace.span_eq_Inf {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {S : set ( K V)} :

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.

theorem projectivization.subspace.span_eq_of_le {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {S : set ( K V)} {W : projectivization.subspace K V} (hS : S W) (hW : W projectivization.subspace.span S) :

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.