mathlib3 documentation

linear_algebra.projective_space.subspace

Subspaces of Projective Space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

@[ext]

structure projectivization.subspace (K : Type u_1) (V : Type u_2) [field K] [add_comm_group V] [module K V] :

Type u_2

carrier : set (ℙ K V)
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

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

projectivization.subspace.has_sizeof_inst
projectivization.subspace.projectivization.set_like
projectivization.subspace.has_inf
projectivization.subspace.has_Inf
projectivization.subspace.complete_lattice
projectivization.subspace.subspace_inhabited

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) :

x = y ↔ x.carrier = y.carrier

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

@[protected, instance]

def projectivization.subspace.projectivization.set_like {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

set_like (projectivization.subspace K V) (ℙ K V)

Equations

projectivization.subspace.projectivization.set_like = {coe := projectivization.subspace.carrier _inst_3, coe_injective' := _}

@[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 ∈ T → projectivization.mk K w hw ∈ T → projectivization.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)

of : ∀ {K : Type u_1} {V : Type u_2} [_inst_1 : field K] [_inst_2 : add_comm_group V] [_inst_3 : module K V] {S : set (ℙ K V)} (x : ℙ K V), x ∈ S → projectivization.subspace.span_carrier S x
mem_add : ∀ {K : Type u_1} {V : Type u_2} [_inst_1 : field K] [_inst_2 : add_comm_group V] [_inst_3 : module K V] {S : set (ℙ K V)} (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), projectivization.subspace.span_carrier S (projectivization.mk K v hv) → projectivization.subspace.span_carrier S (projectivization.mk K w hw) → projectivization.subspace.span_carrier 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.

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)) :

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.span_carrier S, mem_add' := _}

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)) :

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] [add_comm_group V] [module K V] :

galois_insertion projectivization.subspace.span 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

projectivization.subspace.gi = {choice := λ (S : set (ℙ K V)) (hS : ↑(projectivization.subspace.span S) ≤ S), projectivization.subspace.span S, gc := _, le_l_u := _, choice_eq := _}

@[simp]

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

projectivization.subspace.span ↑W = W

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] :

has_inf (projectivization.subspace K V)

The infimum of two subspaces exists.

Equations

projectivization.subspace.has_inf = {inf := λ (A B : projectivization.subspace K V), {carrier := ↑A ⊓ ↑B, mem_add' := _}}

@[protected, instance]

def projectivization.subspace.has_Inf {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

has_Inf (projectivization.subspace K V)

Infimums of arbitrary collections of subspaces exist.

Equations

projectivization.subspace.has_Inf = {Inf := λ (A : set (projectivization.subspace K V)), {carrier := has_Inf.Inf (coe '' A), mem_add' := _}}

@[protected, instance]

def projectivization.subspace.complete_lattice {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

complete_lattice (projectivization.subspace K V)

The subspaces of a projective space form a complete lattice.

Equations

projectivization.subspace.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf infer_instance, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := complete_lattice.top (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), bot := complete_lattice.bot (complete_lattice_of_Inf (projectivization.subspace K V) projectivization.subspace.complete_lattice._proof_1), le_top := _, bot_le := _}

@[protected, instance]

def projectivization.subspace.subspace_inhabited {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] :

inhabited (projectivization.subspace K V)

Equations

projectivization.subspace.subspace_inhabited = {default := ⊤}

@[simp]

theorem projectivization.subspace.span_empty {K : Type u_1} {V : Type u_2} [field K] [add_comm_group 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] [add_comm_group 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] [add_comm_group V] [module K V] {S : set (ℙ 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] [add_comm_group 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] [add_comm_group V] [module K V] {S T U : set (ℙ 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] [add_comm_group V] [module K V] (S T : set (ℙ 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_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.

theorem projectivization.subspace.sup_span {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} :

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] [add_comm_group V] [module K V] {S : set (ℙ 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] [add_comm_group V] [module K V] {S : set (ℙ K V)} (u : ℙ 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_Inf {K : Type u_1} {V : Type u_2} [field K] [add_comm_group V] [module K V] {S : set (ℙ K V)} :

projectivization.subspace.span S = has_Inf.Inf {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] [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) :

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] [add_comm_group V] [module K V] {S T : set (ℙ 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.