Documentation

Mathlib.LinearAlgebra.Projectivization.Collinear

Collinearity in Projective Space #

This file defines collinearity of points in projective space and proves the uniqueness of the line through two distinct points.

Main Results #

Tags #

Projective space, collinearity, projective geometry

source
def Projectivization.IsCollinear {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) :
Prop

If there exists a submodule of dimension at most 2 containing all points in S, then S is collinear. The finite-dimensionality is required so that this notion is meaningful even when V is infinite-dimensional.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Projectivization.IsCollinear_iff {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) :
    IsCollinear S ↔ ∃ (M : Subspace K V), Module.Finite K ↥(Subspace.submodule M) ∧ Module.finrank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
    source
    theorem Projectivization.IsCollinear_iff_rank {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) :
    IsCollinear S ↔ ∃ (M : Subspace K V), Module.rank K ↥(Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
    source
    @[simp]
    theorem Projectivization.isCollinear_empty {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] :
    IsCollinear ∅
    source
    theorem Projectivization.isCollinear_subset {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (s t : Set (Projectivization K V)) (hst : s ⊆ t) (h : IsCollinear t) :
    IsCollinear s
    source
    @[simp]
    theorem Projectivization.isCollinear_singleton' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a : Projectivization K V) :
    IsCollinear {a}
    source
    theorem Projectivization.isCollinear_subsingleton {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) (hS : S.Subsingleton) :
    IsCollinear S
    source
    theorem Projectivization.isCollinear_pair {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (a b : Projectivization K V) :
    IsCollinear {a, b}
    source
    theorem Projectivization.isCollinear_of_card_eq_two {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) (hS : S.ncard = 2) :
    IsCollinear S
    source
    theorem Projectivization.line_unique' {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {u v : V} (hu : u ≠ 0) (hv : v ≠ 0) (huv : LinearIndependent K ![u, v]) (p : Submodule K V) (hp1 : Module.finrank K ↥p = 2) (hp2 : mk K u hu ∈ Submodule.projectivization p) (hp3 : mk K v hv ∈ Submodule.projectivization p) :
    p = Submodule.span K {u, v}
    source
    theorem Projectivization.line_unique {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {x y : Projectivization K V} (hxy : x ≠ y) (p q : Submodule K V) (hp1 : Module.finrank K ↥p = 2) (hq1 : Module.finrank K ↥q = 2) (hp2 : x ∈ Submodule.projectivization p) (hp3 : y ∈ Submodule.projectivization p) (hq2 : x ∈ Submodule.projectivization q) (hq3 : y ∈ Submodule.projectivization q) :
    p = q