# 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 #

- There is a Galois insertion between the subsets of points of a projective space and the subspaces of the projective space, which is given by taking the span of the set of points.
- The subspaces of a projective space form a complete lattice under inclusion.

# Future Work #

- Show that there is a one-to-one order-preserving correspondence between subspaces of a projective space and the submodules of the underlying vector space.

The set of points.

- mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ s.carrier → Projectivization.mk K w hw ∈ s.carrier → Projectivization.mk K (v + w) hvw ∈ s.carrier
The addition rule.

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

- of: ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {S : Set (ℙ K V)} (x : ℙ K V), x ∈ S → Projectivization.Subspace.spanCarrier S x
- mem_add: ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {S : Set (ℙ K V)} (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.Subspace.spanCarrier S (Projectivization.mk K v hv) → Projectivization.Subspace.spanCarrier S (Projectivization.mk K w hw) → Projectivization.Subspace.spanCarrier S (Projectivization.mk K (v + w) hvw)

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.

## Instances For

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.

## Instances For

The span of a subspace is the subspace.

The infimum of two subspaces exists.

Infimums of arbitrary collections of subspaces exist.

The subspaces of a projective space form a complete lattice.

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

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.

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.

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.

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.