feat: port LinearAlgebra.ProjectiveSpace.Independence (#3728)

Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Author: Parcly-Taxel

Mathlib.lean

@@ -1451,6 +1451,7 @@ import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.Prod
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.ProjectiveSpace.Basic
+import Mathlib.LinearAlgebra.ProjectiveSpace.Independence
 import Mathlib.LinearAlgebra.Quotient
 import Mathlib.LinearAlgebra.QuotientPi
 import Mathlib.LinearAlgebra.Ray

Mathlib/LinearAlgebra/Dfinsupp.lean

@@ -550,24 +550,26 @@ See also `CompleteLattice.Independent.linearIndependent'`. -/
 theorem Independent.linearIndependent [NoZeroSMulDivisors R N] (p : ι → Submodule R N)
     (hp : Independent p) {v : ι → N} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) :
     LinearIndependent R v := by
-  classical
-    rw [linearIndependent_iff]
-    intro l hl
-    let a :=
-      Dfinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
-        l.toDfinsupp
-    have ha : a = 0 := by
-      apply hp.dfinsupp_lsum_injective
-      rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
-    ext i
-    apply smul_left_injective R (hv' i)
-    have : l i • v i = a i := rfl
-    simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
-    simpa
+  let _ := Classical.decEq ι
+  let _ := Classical.decEq R
+  rw [linearIndependent_iff]
+  intro l hl
+  let a :=
+    Dfinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
+      l.toDfinsupp
+  have ha : a = 0 := by
+    apply hp.dfinsupp_lsum_injective
+    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
+  ext i
+  apply smul_left_injective R (hv' i)
+  have : l i • v i = a i := rfl
+  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
+  simpa
 #align complete_lattice.independent.linear_independent CompleteLattice.Independent.linearIndependent
 
 theorem independent_iff_linearIndependent_of_ne_zero [NoZeroSMulDivisors R N] {v : ι → N}
     (h_ne_zero : ∀ i, v i ≠ 0) : (Independent fun i => R ∙ v i) ↔ LinearIndependent R v :=
+  let _ := Classical.decEq ι
   ⟨fun hv => hv.linearIndependent _ (fun i => Submodule.mem_span_singleton_self <| v i) h_ne_zero,
     fun hv => hv.independent_span_singleton⟩
 #align complete_lattice.independent_iff_linear_independent_of_ne_zero CompleteLattice.independent_iff_linearIndependent_of_ne_zero

Mathlib/LinearAlgebra/ProjectiveSpace/Independence.lean

@@ -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