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.

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.

• carrier : Set (Projectivization K V)

  The set of points.

• mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ self.carrier → Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier

  The addition rule.

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.carrier → x = y

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.carrier → Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier

The addition rule.

instance Projectivization.Subspace.instSetLike {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : SetLike (Projectivization.Subspace K V) (Projectivization K V)

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 ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.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)) : 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.

• of: ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {S : Set (Projectivization 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 (Projectivization 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)

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

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

Equations

• Projectivization.Subspace.span S = { carrier := Projectivization.Subspace.spanCarrier S, mem_add' := ⋯ }

theorem Projectivization.Subspace.subset_span {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) : S ⊆ ↑(Projectivization.Subspace.span S)

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.

@[simp]

theorem Projectivization.Subspace.span_coe {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Projectivization.Subspace K V) : Projectivization.Subspace.span ↑W = W

The span of a subspace is the subspace.

instance Projectivization.Subspace.instInf {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Inf (Projectivization.Subspace K V)

The infimum of two subspaces exists.

Equations

• Projectivization.Subspace.instInf = { inf := fun (A B : Projectivization.Subspace K V) => { carrier := ↑A ⊓ ↑B, mem_add' := ⋯ } }

instance Projectivization.Subspace.instInfSet {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : InfSet (Projectivization.Subspace K V)

Infimums of arbitrary collections of subspaces exist.

Equations

• Projectivization.Subspace.instInfSet = { sInf := fun (A : Set (Projectivization.Subspace K V)) => { carrier := sInf (SetLike.coe '' A), mem_add' := ⋯ } }

instance Projectivization.Subspace.instCompleteLattice {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : CompleteLattice (Projectivization.Subspace K V)

The subspaces of a projective space form a complete lattice.

Equations

• Projectivization.Subspace.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Projectivization.Subspace.subspaceInhabited {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Inhabited (Projectivization.Subspace K V)

Equations

• Projectivization.Subspace.subspaceInhabited = { default := ⊤ }

@[simp]

theorem Projectivization.Subspace.span_empty {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Projectivization.Subspace.span ∅ = ⊥

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

@[simp]

theorem Projectivization.Subspace.span_univ {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Projectivization.Subspace.span Set.univ = ⊤

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] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : Projectivization.Subspace.span S ≤ W ↔ S ⊆ ↑W

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.

theorem Projectivization.Subspace.subset_span_trans {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {T : Set (Projectivization K V)} {U : Set (Projectivization K V)} (hST : S ⊆ ↑(Projectivization.Subspace.span T)) (hTU : T ⊆ ↑(Projectivization.Subspace.span U)) : S ⊆ ↑(Projectivization.Subspace.span U)

theorem Projectivization.Subspace.span_union {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) (T : Set (Projectivization K V)) : Projectivization.Subspace.span (S ∪ T) = Projectivization.Subspace.span S ⊔ Projectivization.Subspace.span T

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.

theorem Projectivization.Subspace.sup_span {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : W ⊔ Projectivization.Subspace.span S = Projectivization.Subspace.span (↑W ∪ S)

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.span_sup {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : Projectivization.Subspace.span S ⊔ W = Projectivization.Subspace.span (S ∪ ↑W)

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) : u ∈ Projectivization.Subspace.span S ↔ ∀ (W : Projectivization.Subspace K V), S ⊆ ↑W → u ∈ W

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_sInf {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} : Projectivization.Subspace.span S = sInf {W : Projectivization.Subspace K V | S ⊆ ↑W}

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] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} (hS : S ⊆ ↑W) (hW : W ≤ Projectivization.Subspace.span S) : Projectivization.Subspace.span S = W

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.

theorem Projectivization.Subspace.span_eq_span_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {T : Set (Projectivization K V)} : Projectivization.Subspace.span S = Projectivization.Subspace.span T ↔ S ⊆ ↑(Projectivization.Subspace.span T) ∧ T ⊆ ↑(Projectivization.Subspace.span S)

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.