Independence in Projective Space #

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

In this file we define independence and dependence of families of elements in projective space.

Implementation Details #

We use an inductive definition to define the independence of points in projective space, where the only constructor assumes an independent family of vectors from the ambient vector space. Similarly for the definition of dependence.

Results #

A family of elements is dependent if and only if it is not independent.
Two elements are dependent if and only if they are equal.

Future Work #

Define collinearity in projective space.
Prove the axioms of a projective geometry are satisfied by the dependence relation.
Define projective linear subspaces.

source

inductive projectivization.independent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] :

(ι → ℙ K V) → Prop

mk : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [_inst_1 : field K] [_inst_2 : add_comm_group V] [_inst_3 : module K V] (f : ι → V) (hf : ∀ (i : ι), f i ≠ 0), linear_independent K f → projectivization.independent (λ (i : ι), projectivization.mk K (f i) _)

A linearly independent family of nonzero vectors gives an independent family of points in projective space.

source

theorem projectivization.independent_iff {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} :

projectivization.independent f ↔ linear_independent K (projectivization.rep ∘ f)

A family of points in a projective space is independent if and only if the representative vectors determined by the family are linearly independent.

source

theorem projectivization.independent_iff_complete_lattice_independent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} :

projectivization.independent f ↔ complete_lattice.independent (λ (i : ι), (f i).submodule)

A family of points in projective space is independent if and only if the family of submodules which the points determine is independent in the lattice-theoretic sense.

source

inductive projectivization.dependent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] :

(ι → ℙ K V) → Prop

mk : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [_inst_1 : field K] [_inst_2 : add_comm_group V] [_inst_3 : module K V] (f : ι → V) (hf : ∀ (i : ι), f i ≠ 0), ¬linear_independent K f → projectivization.dependent (λ (i : ι), projectivization.mk K (f i) _)

A linearly dependent family of nonzero vectors gives a dependent family of points in projective space.

source

theorem projectivization.dependent_iff {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} :

projectivization.dependent f ↔ ¬linear_independent K (projectivization.rep ∘ f)

A family of points in a projective space is dependent if and only if their representatives are linearly dependent.

source

theorem projectivization.dependent_iff_not_independent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} :

projectivization.dependent f ↔ ¬projectivization.independent f

Dependence is the negation of independence.

source

theorem projectivization.independent_iff_not_dependent {ι : Type u_1} {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} :

projectivization.independent f ↔ ¬projectivization.dependent f

Independence is the negation of dependence.

source

@[simp]

theorem projectivization.dependent_pair_iff_eq {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] (u v : ℙ K V) :

projectivization.dependent ![u, v] ↔ u = v

Two points in a projective space are dependent if and only if they are equal.

source

@[simp]

theorem projectivization.independent_pair_iff_neq {K : Type u_2} {V : Type u_3} [field K] [add_comm_group V] [module K V] (u v : ℙ K V) :

projectivization.independent ![u, v] ↔ u ≠ v

Two points in a projective space are independent if and only if the points are not equal.