From 1e82f5ec4645f6a92bb9e02fce51e44e3bc3e1fe Mon Sep 17 00:00:00 2001 From: MichaelBlyth <39394803+Michael14071407@users.noreply.github.com> Date: Wed, 13 Jul 2022 21:11:24 +0000 Subject: [PATCH] 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 Co-authored-by: Oliver Nash Co-authored-by: Adam Topaz --- .../projective_space/basic.lean | 11 ++ .../projective_space/independence.lean | 116 ++++++++++++++++++ 2 files changed, 127 insertions(+) create mode 100644 src/linear_algebra/projective_space/independence.lean diff --git a/src/linear_algebra/projective_space/basic.lean b/src/linear_algebra/projective_space/basic.lean index b9d8b4656ce04..4be3ed2e0e4a0 100644 --- a/src/linear_algebra/projective_space/basic.lean +++ b/src/linear_algebra/projective_space/basic.lean @@ -92,6 +92,17 @@ lemma mk_eq_mk_iff (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ ∃ (a : Kˣ), a • w = v := quotient.eq' +/-- Two nonzero vectors go to the same point in projective space if and only if one is +a scalar multiple of the other. -/ +lemma mk_eq_mk_iff' (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : mk K v hv = mk K w hw ↔ + ∃ (a : K), a • w = v := +begin + rw mk_eq_mk_iff K v w hv hw, + split, + { rintro ⟨a, ha⟩, exact ⟨a, ha⟩ }, + { rintro ⟨a, ha⟩, refine ⟨units.mk0 a (λ c, hv.symm _), ha⟩, rwa [c, zero_smul] at ha } +end + lemma exists_smul_eq_mk_rep (v : V) (hv : v ≠ 0) : ∃ (a : Kˣ), a • v = (mk K v hv).rep := show (projectivization_setoid K V).rel _ _, from quotient.mk_out' ⟨v, hv⟩ diff --git a/src/linear_algebra/projective_space/independence.lean b/src/linear_algebra/projective_space/independence.lean new file mode 100644 index 0000000000000..f210d15c03dc1 --- /dev/null +++ b/src/linear_algebra/projective_space/independence.lean @@ -0,0 +1,116 @@ +/- +Copyright (c) 2022 Michael Blyth. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Michael Blyth +-/ + +import linear_algebra.projective_space.basic + +/-! +# Independence in Projective Space + +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. +-/ + + +variables {ι K V : Type*} [field K] [add_comm_group V] [module K V] {f : ι → ℙ K V} + +namespace projectivization + +/-- A linearly independent family of nonzero vectors gives an independent family of points +in projective space. -/ +inductive independent : (ι → ℙ K V) → Prop +| mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (hl : linear_independent K f) : + independent (λ i, mk K (f i) (hf i)) + +/-- A family of points in a projective space is independent if and only if the representative +vectors determined by the family are linearly independent. -/ +lemma independent_iff : independent f ↔ linear_independent K (projectivization.rep ∘ f) := +begin + refine ⟨_, λ h, _⟩, + { rintros ⟨ff, hff, hh⟩, + choose a ha using λ (i : ι), exists_smul_eq_mk_rep K (ff i) (hff i), + convert hh.units_smul a, + ext i, exact (ha i).symm }, + { convert independent.mk _ _ h, + { ext, simp only [mk_rep] }, + { intro i, apply rep_nonzero } } +end + +/-- 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. -/ +lemma independent_iff_complete_lattice_independent : + independent f ↔ (complete_lattice.independent $ λ i, (f i).submodule) := +begin + refine ⟨_, λ h, _⟩, + { rintros ⟨f, hf, hi⟩, + simpa [submodule_mk, complete_lattice.independent_iff_linear_independent_of_ne_zero hf] }, + { rw independent_iff, + refine h.linear_independent (projectivization.submodule ∘ f) (λ i, _) (λ i, _), + { simpa only [function.comp_app, submodule_eq] using submodule.mem_span_singleton_self _, }, + { exact rep_nonzero (f i) } }, +end + +/-- A linearly dependent family of nonzero vectors gives a dependent family of points +in projective space. -/ +inductive dependent : (ι → ℙ K V) → Prop +| mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (h : ¬linear_independent K f) : + dependent (λ i, mk K (f i) (hf i)) + +/-- A family of points in a projective space is dependent if and only if their +representatives are linearly dependent. -/ +lemma dependent_iff : dependent f ↔ ¬ linear_independent K (projectivization.rep ∘ f) := +begin + refine ⟨_, λ h, _⟩, + { rintros ⟨ff, hff, hh1⟩, + contrapose! hh1, + choose a ha using λ (i : ι), exists_smul_eq_mk_rep K (ff i) (hff i), + convert hh1.units_smul a⁻¹, + ext i, + simp only [← ha, inv_smul_smul, pi.smul_apply', pi.inv_apply, function.comp_app] }, + { convert dependent.mk _ _ h, + { ext i, simp only [mk_rep] }, + { exact λ i, rep_nonzero (f i) } } +end + +/-- Dependence is the negation of independence. -/ +lemma dependent_iff_not_independent : dependent f ↔ ¬ independent f := +by rw [dependent_iff, independent_iff] + +/-- Independence is the negation of dependence. -/ +lemma independent_iff_not_dependent : independent f ↔ ¬ dependent f := +by rw [dependent_iff_not_independent, not_not] + +/-- Two points in a projective space are dependent if and only if they are equal. -/ +@[simp] lemma dependent_pair_iff_eq (u v : ℙ K V) : dependent ![u, v] ↔ u = v := +begin + simp_rw [dependent_iff_not_independent, independent_iff, linear_independent_fin2, + function.comp_app, matrix.cons_val_one, matrix.head_cons, + ne.def, matrix.cons_val_zero, not_and, not_forall, not_not, + ← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep, + imp_iff_right_iff], + exact or.inl (rep_nonzero v), +end + +/-- Two points in a projective space are independent if and only if the points are not equal. -/ +@[simp] lemma independent_pair_iff_neq (u v : ℙ K V) : independent ![u, v] ↔ u ≠ v := +by rw [independent_iff_not_dependent, dependent_pair_iff_eq u v] + +end projectivization