-
Notifications
You must be signed in to change notification settings - Fork 248
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728)
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
- Loading branch information
Showing
3 changed files
with
142 additions
and
14 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
125 changes: 125 additions & 0 deletions
125
Mathlib/LinearAlgebra/ProjectiveSpace/Independence.lean
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,125 @@ | ||
/- | ||
Copyright (c) 2022 Michael Blyth. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Michael Blyth | ||
! This file was ported from Lean 3 source module linear_algebra.projective_space.independence | ||
! leanprover-community/mathlib commit 1e82f5ec4645f6a92bb9e02fce51e44e3bc3e1fe | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
-/ | ||
import Mathlib.LinearAlgebra.ProjectiveSpace.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. | ||
-/ | ||
|
||
|
||
variable {ι K V : Type _} [Field K] [AddCommGroup 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 : LinearIndependent K f) : | ||
Independent fun i => mk K (f i) (hf i) | ||
#align projectivization.independent Projectivization.Independent | ||
|
||
/-- A family of points in a projective space is independent if and only if the representative | ||
vectors determined by the family are linearly independent. -/ | ||
theorem independent_iff : Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f) := by | ||
refine' ⟨_, fun h => _⟩ | ||
· rintro ⟨ff, hff, hh⟩ | ||
choose a ha using fun 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 | ||
· simp only [mk_rep, Function.comp_apply] | ||
· intro i | ||
apply rep_nonzero | ||
#align projectivization.independent_iff Projectivization.independent_iff | ||
|
||
/-- 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. -/ | ||
theorem independent_iff_completeLattice_independent : | ||
Independent f ↔ CompleteLattice.Independent fun i => (f i).submodule := by | ||
refine' ⟨_, fun h => _⟩ | ||
· rintro ⟨f, hf, hi⟩ | ||
simp only [submodule_mk] | ||
exact (CompleteLattice.independent_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi | ||
· rw [independent_iff] | ||
refine' h.linearIndependent (Projectivization.submodule ∘ f) (fun i => _) fun i => _ | ||
· simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _ | ||
· exact rep_nonzero (f i) | ||
#align projectivization.independent_iff_complete_lattice_independent Projectivization.independent_iff_completeLattice_independent | ||
|
||
/-- 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 : ¬LinearIndependent K f) : | ||
Dependent fun i => mk K (f i) (hf i) | ||
#align projectivization.dependent Projectivization.Dependent | ||
|
||
/-- A family of points in a projective space is dependent if and only if their | ||
representatives are linearly dependent. -/ | ||
theorem dependent_iff : Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f) := by | ||
refine' ⟨_, fun h => _⟩ | ||
· rintro ⟨ff, hff, hh1⟩ | ||
contrapose! hh1 | ||
choose a ha using fun 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_apply] | ||
· convert Dependent.mk _ _ h | ||
· simp only [mk_rep, Function.comp_apply] | ||
· exact fun i => rep_nonzero (f i) | ||
#align projectivization.dependent_iff Projectivization.dependent_iff | ||
|
||
/-- Dependence is the negation of independence. -/ | ||
theorem dependent_iff_not_independent : Dependent f ↔ ¬Independent f := by | ||
rw [dependent_iff, independent_iff] | ||
#align projectivization.dependent_iff_not_independent Projectivization.dependent_iff_not_independent | ||
|
||
/-- Independence is the negation of dependence. -/ | ||
theorem independent_iff_not_dependent : Independent f ↔ ¬Dependent f := by | ||
rw [dependent_iff_not_independent, Classical.not_not] | ||
#align projectivization.independent_iff_not_dependent Projectivization.independent_iff_not_dependent | ||
|
||
/-- Two points in a projective space are dependent if and only if they are equal. -/ | ||
@[simp] | ||
theorem dependent_pair_iff_eq (u v : ℙ K V) : Dependent ![u, v] ↔ u = v := by | ||
rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2, | ||
Function.comp_apply, Matrix.cons_val_one, Matrix.head_cons, Ne.def] | ||
simp only [Matrix.cons_val_zero, not_and, not_forall, Classical.not_not, Function.comp_apply, | ||
← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep, imp_iff_right_iff] | ||
exact Or.inl (rep_nonzero v) | ||
#align projectivization.dependent_pair_iff_eq Projectivization.dependent_pair_iff_eq | ||
|
||
/-- Two points in a projective space are independent if and only if the points are not equal. -/ | ||
@[simp] | ||
theorem 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] | ||
#align projectivization.independent_pair_iff_neq Projectivization.independent_pair_iff_neq | ||
|
||
end Projectivization |