Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 1e82f5e

Browse files
Michael14071407adamtopazocfnash
committed
feat(linear_algebra/projectivization/independence): defines (in)dependence of points in projective space (#14542)
This PR only provides definitions and basic lemmas. In an upcoming pull request we use this to prove the axioms for an abstract projective space. Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Adam Topaz <github@adamtopaz.com>
1 parent f731315 commit 1e82f5e

2 files changed

Lines changed: 127 additions & 0 deletions

File tree

‎src/linear_algebra/projective_space/basic.lean‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,17 @@ lemma mk_eq_mk_iff (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) :
9292
mk K v hv = mk K w hw ↔ ∃ (a : Kˣ), a • w = v :=
9393
quotient.eq'
9494

95+
/-- Two nonzero vectors go to the same point in projective space if and only if one is
96+
a scalar multiple of the other. -/
97+
lemma mk_eq_mk_iff' (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔
98+
∃ (a : K), a • w = v :=
99+
begin
100+
rw mk_eq_mk_iff K v w hv hw,
101+
split,
102+
{ rintro ⟨a, ha⟩, exact ⟨a, ha⟩ },
103+
{ rintro ⟨a, ha⟩, refine ⟨units.mk0 a (λ c, hv.symm _), ha⟩, rwa [c, zero_smul] at ha }
104+
end
105+
95106
lemma exists_smul_eq_mk_rep
96107
(v : V) (hv : v ≠ 0) : ∃ (a : Kˣ), a • v = (mk K v hv).rep :=
97108
show (projectivization_setoid K V).rel _ _, from quotient.mk_out' ⟨v, hv⟩

‎src/linear_algebra/projective_space/independence.lean‎

Lines changed: 116 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
/-
2+
Copyright (c) 2022 Michael Blyth. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Michael Blyth
5+
-/
6+
7+
import linear_algebra.projective_space.basic
8+
9+
/-!
10+
# Independence in Projective Space
11+
12+
In this file we define independence and dependence of families of elements in projective space.
13+
14+
## Implementation Details
15+
16+
We use an inductive definition to define the independence of points in projective
17+
space, where the only constructor assumes an independent family of vectors from the
18+
ambient vector space. Similarly for the definition of dependence.
19+
20+
## Results
21+
22+
- A family of elements is dependent if and only if it is not independent.
23+
- Two elements are dependent if and only if they are equal.
24+
25+
# Future Work
26+
27+
- Define collinearity in projective space.
28+
- Prove the axioms of a projective geometry are satisfied by the dependence relation.
29+
- Define projective linear subspaces.
30+
-/
31+
32+
33+
variables {ι K V : Type*} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V}
34+
35+
namespace projectivization
36+
37+
/-- A linearly independent family of nonzero vectors gives an independent family of points
38+
in projective space. -/
39+
inductive independent : (ι → ℙ K V) → Prop
40+
| mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (hl : linear_independent K f) :
41+
independent (λ i, mk K (f i) (hf i))
42+
43+
/-- A family of points in a projective space is independent if and only if the representative
44+
vectors determined by the family are linearly independent. -/
45+
lemma independent_iff : independent f ↔ linear_independent K (projectivization.rep ∘ f) :=
46+
begin
47+
refine ⟨_, λ h, _⟩,
48+
{ rintros ⟨ff, hff, hh⟩,
49+
choose a ha using λ (i : ι), exists_smul_eq_mk_rep K (ff i) (hff i),
50+
convert hh.units_smul a,
51+
ext i, exact (ha i).symm },
52+
{ convert independent.mk _ _ h,
53+
{ ext, simp only [mk_rep] },
54+
{ intro i, apply rep_nonzero } }
55+
end
56+
57+
/-- A family of points in projective space is independent if and only if the family of
58+
submodules which the points determine is independent in the lattice-theoretic sense. -/
59+
lemma independent_iff_complete_lattice_independent :
60+
independent f ↔ (complete_lattice.independent $ λ i, (f i).submodule) :=
61+
begin
62+
refine ⟨_, λ h, _⟩,
63+
{ rintros ⟨f, hf, hi⟩,
64+
simpa [submodule_mk, complete_lattice.independent_iff_linear_independent_of_ne_zero hf] },
65+
{ rw independent_iff,
66+
refine h.linear_independent (projectivization.submodule ∘ f) (λ i, _) (λ i, _),
67+
{ simpa only [function.comp_app, submodule_eq] using submodule.mem_span_singleton_self _, },
68+
{ exact rep_nonzero (f i) } },
69+
end
70+
71+
/-- A linearly dependent family of nonzero vectors gives a dependent family of points
72+
in projective space. -/
73+
inductive dependent : (ι → ℙ K V) → Prop
74+
| mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (h : ¬linear_independent K f) :
75+
dependent (λ i, mk K (f i) (hf i))
76+
77+
/-- A family of points in a projective space is dependent if and only if their
78+
representatives are linearly dependent. -/
79+
lemma dependent_iff : dependent f ↔ ¬ linear_independent K (projectivization.rep ∘ f) :=
80+
begin
81+
refine ⟨_, λ h, _⟩,
82+
{ rintros ⟨ff, hff, hh1⟩,
83+
contrapose! hh1,
84+
choose a ha using λ (i : ι), exists_smul_eq_mk_rep K (ff i) (hff i),
85+
convert hh1.units_smul a⁻¹,
86+
ext i,
87+
simp only [← ha, inv_smul_smul, pi.smul_apply', pi.inv_apply, function.comp_app] },
88+
{ convert dependent.mk _ _ h,
89+
{ ext i, simp only [mk_rep] },
90+
{ exact λ i, rep_nonzero (f i) } }
91+
end
92+
93+
/-- Dependence is the negation of independence. -/
94+
lemma dependent_iff_not_independent : dependent f ↔ ¬ independent f :=
95+
by rw [dependent_iff, independent_iff]
96+
97+
/-- Independence is the negation of dependence. -/
98+
lemma independent_iff_not_dependent : independent f ↔ ¬ dependent f :=
99+
by rw [dependent_iff_not_independent, not_not]
100+
101+
/-- Two points in a projective space are dependent if and only if they are equal. -/
102+
@[simp] lemma dependent_pair_iff_eq (u v : ℙ K V) : dependent ![u, v] ↔ u = v :=
103+
begin
104+
simp_rw [dependent_iff_not_independent, independent_iff, linear_independent_fin2,
105+
function.comp_app, matrix.cons_val_one, matrix.head_cons,
106+
ne.def, matrix.cons_val_zero, not_and, not_forall, not_not,
107+
← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep,
108+
imp_iff_right_iff],
109+
exact or.inl (rep_nonzero v),
110+
end
111+
112+
/-- Two points in a projective space are independent if and only if the points are not equal. -/
113+
@[simp] lemma independent_pair_iff_neq (u v : ℙ K V) : independent ![u, v] ↔ u ≠ v :=
114+
by rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]
115+
116+
end projectivization

0 commit comments

Comments
 (0)