feat(LinearIndependent): more API for linearIndepOn (#22368)

We add a few more API lemmas for `linearIndepOn`, in many cases generalizing `id` versions of existing lemmas to arbitrary functions.

Author: apnelson1

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -56,16 +56,35 @@ theorem LinearIndependent.sumElim_of_quotient
 @[deprecated (since := "2025-02-21")]
 alias LinearIndependent.sum_elim_of_quotient := LinearIndependent.sumElim_of_quotient
 
-theorem LinearIndepOn.union_of_quotient {M' : Submodule R M}
+theorem LinearIndepOn.union_of_quotient {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s)
+    (ht : LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t) : LinearIndepOn R f (s ∪ t) := by
+  apply hs.union ht.of_comp
+  convert (Submodule.range_ker_disjoint ht).symm
+  · simp
+  aesop
+
+theorem LinearIndepOn.union_id_of_quotient {M' : Submodule R M}
     {s : Set M} (hs : s ⊆ M') (hs' : LinearIndepOn R id s) {t : Set M}
-    (ht : LinearIndepOn R (Submodule.Quotient.mk (p := M')) t) : LinearIndepOn R id (s ∪ t) :=
-  have h := (LinearIndependent.sumElim_of_quotient (f := Set.embeddingOfSubset s M' hs)
-    (LinearIndependent.of_comp M'.subtype (by simpa using hs')) Subtype.val ht)
-  h.linearIndepOn_id' <| by
-    simp only [embeddingOfSubset_apply_coe, Sum.elim_range, Subtype.range_val]
+    (ht : LinearIndepOn R (mkQ M') t) : LinearIndepOn R id (s ∪ t) :=
+  hs'.union_of_quotient <| by
+    rw [image_id]
+    exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))
 
 @[deprecated (since := "2025-02-16")] alias LinearIndependent.union_of_quotient :=
-  LinearIndepOn.union_of_quotient
+  LinearIndepOn.union_id_of_quotient
+
+theorem linearIndepOn_union_iff_quotient {s t : Set ι} {f : ι → M} (hst : Disjoint s t) :
+    LinearIndepOn R f (s ∪ t) ↔
+    LinearIndepOn R f s ∧ LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t := by
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
+  · exact h.mono subset_union_left
+  apply (h.mono subset_union_right).map
+  simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm
+
+theorem LinearIndepOn.quotient_iff_union {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s)
+    (hst : Disjoint s t) :
+    LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t ↔ LinearIndepOn R f (s ∪ t) := by
+  rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]
 
 theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
     Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M := by

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

@@ -92,19 +92,19 @@ theorem exists_linearIndepOn_of_lt_rank [StrongRankCondition R]
     {s : Set M} (hs : LinearIndepOn R id s) :
     ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndepOn R id t := by
   obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)
-  choose sec hsec using Submodule.Quotient.mk_surjective (Submodule.span R s)
-  have hsec' : Submodule.Quotient.mk ∘ sec = _root_.id := funext hsec
+  choose sec hsec using Submodule.mkQ_surjective (Submodule.span R s)
+  have hsec' : (Submodule.mkQ _) ∘ sec = _root_.id := funext hsec
   have hst : Disjoint s (sec '' t) := by
     rw [Set.disjoint_iff]
     rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩
     apply ht'.ne_zero ⟨x, hxt⟩
-    rw [Subtype.coe_mk, ← hsec x, Submodule.Quotient.mk_eq_zero]
+    rw [Subtype.coe_mk, ← hsec x,mkQ_apply, Quotient.mk_eq_zero]
     exact Submodule.subset_span hxs
   refine ⟨s ∪ sec '' t, subset_union_left, ?_, ?_⟩
   · rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht,
       ← rank_quotient_add_rank (Submodule.span R s), add_comm, rank_span_set hs]
     exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩
-  · apply LinearIndepOn.union_of_quotient Submodule.subset_span hs
+  · apply LinearIndepOn.union_id_of_quotient Submodule.subset_span hs
     rwa [linearIndepOn_iff_image (hsec'.symm ▸ injective_id).injOn.image_of_comp,
       ← image_comp, hsec', image_id]
 

Mathlib/LinearAlgebra/LinearIndependent/Basic.lean

@@ -152,6 +152,21 @@ theorem LinearIndepOn.id_image (hs : LinearIndepOn R v s) : LinearIndepOn R id (
 @[deprecated (since := "2025-02-14")] alias
   LinearIndependent.image := LinearIndepOn.id_image
 
+theorem LinearIndepOn_iff_linearIndepOn_image_injOn [Nontrivial R] :
+    LinearIndepOn R v s ↔ LinearIndepOn R id (v '' s) ∧ InjOn v s :=
+  ⟨fun h ↦ ⟨h.id_image, h.injOn⟩, fun h ↦ (linearIndepOn_iff_image h.2).2 h.1⟩
+
+theorem linearIndepOn_congr {w : ι → M} (h : EqOn v w s) :
+    LinearIndepOn R v s ↔ LinearIndepOn R w s := by
+  rw [LinearIndepOn, LinearIndepOn]
+  convert Iff.rfl using 2
+  ext x
+  exact h.symm x.2
+
+theorem LinearIndepOn.congr {w : ι → M} (hli : LinearIndepOn R v s) (h : EqOn v w s) :
+    LinearIndepOn R w s :=
+  (linearIndepOn_congr h).1 hli
+
 theorem LinearIndependent.group_smul {G : Type*} [hG : Group G] [DistribMulAction G R]
     [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : ι → M}
     (hv : LinearIndependent R v) (w : ι → G) : LinearIndependent R (w • v) := by
@@ -453,14 +468,35 @@ theorem LinearIndependent.sum_type {v' : ι' → M} (hv : LinearIndependent R v)
     LinearIndependent R (Sum.elim v v') :=
   linearIndependent_sum.2 ⟨hv, hv', h⟩
 
--- TODO - generalize this to non-identity functions
-theorem LinearIndepOn.id_union {s t : Set M} (hs : LinearIndepOn R id s)
-    (ht : LinearIndepOn R id t) (hst : Disjoint (span R s) (span R t)) :
-    LinearIndepOn R id (s ∪ t) := by
-  have h := hs.linearIndependent.sum_type ht.linearIndependent (by simpa)
-  simpa [id_eq] using h.linearIndepOn_id
-
-@[deprecated (since := "2025-02-14")] alias LinearIndependent.union := LinearIndepOn.id_union
+theorem LinearIndepOn.union {t : Set ι} (hs : LinearIndepOn R v s) (ht : LinearIndepOn R v t)
+    (hdj : Disjoint (span R (v '' s)) (span R (v '' t))) : LinearIndepOn R v (s ∪ t) := by
+  nontriviality R
+  classical
+  have hli := LinearIndependent.sum_type hs ht (by rwa [← image_eq_range, ← image_eq_range])
+  have hdj := (hdj.of_span₀ hs.zero_not_mem_image).of_image
+  rw [LinearIndepOn]
+  convert (hli.comp _ (Equiv.Set.union hdj).injective) with ⟨x, hx | hx⟩
+  · rw [comp_apply, Equiv.Set.union_apply_left _ hx, Sum.elim_inl]
+  rw [comp_apply, Equiv.Set.union_apply_right _ hx, Sum.elim_inr]
+
+theorem LinearIndepOn.id_union {s t : Set M} (hs : LinearIndepOn R id s) (ht : LinearIndepOn R id t)
+    (hdj : Disjoint (span R s) (span R t)) : LinearIndepOn R id (s ∪ t) :=
+  hs.union ht (by simpa)
+
+theorem linearIndepOn_union_iff {t : Set ι} (hdj : Disjoint s t) :
+    LinearIndepOn R v (s ∪ t) ↔
+    LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (span R (v '' s)) (span R (v '' t)) := by
+  refine ⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right, ?_⟩,
+    fun h ↦ h.1.union h.2.1 h.2.2⟩
+  convert h.disjoint_span_image (s := (↑) ⁻¹' s) (t := (↑) ⁻¹' t) (hdj.preimage _) <;>
+  aesop
+
+theorem linearIndepOn_id_union_iff {s t : Set M} (hdj : Disjoint s t) :
+    LinearIndepOn R id (s ∪ t) ↔
+    LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (span R s) (span R t) := by
+  rw [linearIndepOn_union_iff hdj, image_id, image_id]
+
+@[deprecated (since := "2025-02-14")] alias LinearIndependent.union := LinearIndepOn.union
 
 open LinearMap
 
@@ -583,8 +619,12 @@ theorem linearIndependent_unique_iff (v : ι → M) [Unique ι] :
 
 alias ⟨_, linearIndependent_unique⟩ := linearIndependent_unique_iff
 
-theorem LinearIndepOn.singleton {v : ι → M} {i : ι} (hi : v i ≠ 0) : LinearIndepOn R v {i} :=
-  linearIndependent_unique _ hi
+variable (R) in
+@[simp]
+theorem linearIndepOn_singleton_iff {i : ι} {v : ι → M} : LinearIndepOn R v {i} ↔ v i ≠ 0 :=
+  ⟨fun h ↦ h.ne_zero rfl, fun h ↦ linearIndependent_unique _ h⟩
+
+alias ⟨_, LinearIndepOn.singleton⟩ := linearIndepOn_singleton_iff
 
 variable (R) in
 theorem LinearIndepOn.id_singleton {x : M} (hx : x ≠ 0) : LinearIndepOn R id {x} :=

Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

@@ -142,6 +142,9 @@ theorem LinearIndepOn.ne_zero [Nontrivial R] {i : ι} (hv : LinearIndepOn R v s)
     v i ≠ 0 :=
   LinearIndependent.ne_zero ⟨i, hi⟩ hv
 
+theorem LinearIndepOn.zero_not_mem_image [Nontrivial R] (hs : LinearIndepOn R v s) : 0 ∉ v '' s :=
+  fun ⟨_, hi, h0⟩ ↦ hs.ne_zero hi h0
+
 theorem linearIndependent_empty_type [IsEmpty ι] : LinearIndependent R v :=
   injective_of_subsingleton _
 
@@ -150,6 +153,10 @@ theorem linearIndependent_zero_iff [Nontrivial R] : LinearIndependent R (0 : ι
   ⟨fun h ↦ not_nonempty_iff.1 fun ⟨i⟩ ↦ (h.ne_zero i rfl).elim,
     fun _ ↦ linearIndependent_empty_type⟩
 
+@[simp]
+theorem linearIndepOn_zero_iff [Nontrivial R] : LinearIndepOn R (0 : ι → M) s ↔ s = ∅ :=
+  linearIndependent_zero_iff.trans isEmpty_coe_sort
+
 variable (R M) in
 theorem linearIndependent_empty : LinearIndependent R (fun x => x : (∅ : Set M) → M) :=
   linearIndependent_empty_type

Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

@@ -415,7 +415,7 @@ protected theorem LinearIndepOn.insert (hs : LinearIndepOn K id s) (hx : x ∉ s
     LinearIndepOn K id (insert x s) := by
   rw [← union_singleton]
   have x0 : x ≠ 0 := mt (by rintro rfl; apply zero_mem (span K s)) hx
-  apply hs.id_union (LinearIndepOn.singleton x0)
+  apply hs.id_union (LinearIndepOn.id_singleton _ x0)
   rwa [disjoint_span_singleton' x0]
 
 @[deprecated (since := "2025-02-15")] alias LinearIndependent.insert := LinearIndepOn.insert
@@ -458,13 +458,48 @@ theorem linearIndepOn_id_insert (hxs : x ∉ s) :
 
 @[deprecated (since := "2025-02-15")] alias linearIndependent_insert := linearIndepOn_insert
 
+theorem linearIndepOn_insert_iff {s : Set ι} {a : ι} {f : ι → V} :
+    LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s) := by
+  by_cases has : a ∈ s
+  · simp [insert_eq_of_mem has, has]
+  simp [linearIndepOn_insert has, has]
+
+theorem linearIndepOn_id_insert_iff {a : V} {s : Set V} :
+    LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (a ∈ span K s → a ∈ s) := by
+  simpa using linearIndepOn_insert_iff (a := a) (f := id)
+
+theorem LinearIndepOn.mem_span_iff {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
+    f a ∈ Submodule.span K (f '' s) ↔ (LinearIndepOn K f (insert a s) → a ∈ s) := by
+  by_cases has : a ∈ s
+  · exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has
+  simp [linearIndepOn_insert_iff, h, has]
+
+/-- A shortcut to a convenient form for the negation in `LinearIndepOn.mem_span_iff`. -/
+theorem LinearIndepOn.not_mem_span_iff {s : Set ι} {a : ι} {f : ι → V} (h : LinearIndepOn K f s) :
+    f a ∉ Submodule.span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s := by
+  rw [h.mem_span_iff, _root_.not_imp]
+
+theorem LinearIndepOn.mem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn K id s) :
+    a ∈ Submodule.span K s ↔ (LinearIndepOn K id (insert a s) → a ∈ s) := by
+  simpa using h.mem_span_iff (a := a)
+
+theorem LinearIndepOn.not_mem_span_iff_id {s : Set V} {a : V} (h : LinearIndepOn K id s) :
+    a ∉ Submodule.span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s := by
+  rw [h.mem_span_iff_id, _root_.not_imp]
+
 theorem linearIndepOn_id_pair {x y : V} (hx : x ≠ 0) (hy : ∀ a : K, a • x ≠ y) :
     LinearIndepOn K id {x, y} :=
   pair_comm y x ▸ (LinearIndepOn.id_singleton K hx).insert (x := y) <|
     mt mem_span_singleton.1 <| not_exists.2 hy
 
 @[deprecated (since := "2025-02-15")] alias linearIndependent_pair := linearIndepOn_id_pair
 
+theorem linearIndepOn_pair_iff {i j : ι} (v : ι → V) (hij : i ≠ j) (hi : v i ≠ 0):
+    LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j := by
+  rw [pair_comm]
+  convert linearIndepOn_insert (s := {i}) (a := j) hij.symm
+  simp [hi, mem_span_singleton, linearIndependent_unique_iff]
+
 /-- Also see `LinearIndependent.pair_iff` for the version over arbitrary rings. -/
 theorem LinearIndependent.pair_iff' {x y : V} (hx : x ≠ 0) :
     LinearIndependent K ![x, y] ↔ ∀ a : K, a • x ≠ y := by

Mathlib/LinearAlgebra/Span/Defs.lean

@@ -225,6 +225,17 @@ theorem span_int_eq_addSubgroup_closure {M : Type*} [AddCommGroup M] (s : Set M)
 theorem span_int_eq {M : Type*} [AddCommGroup M] (s : AddSubgroup M) :
     (span ℤ (s : Set M)).toAddSubgroup = s := by rw [span_int_eq_addSubgroup_closure, s.closure_eq]
 
+theorem _root_.Disjoint.of_span (hst : Disjoint (span R s) (span R t)) :
+    Disjoint (s \ {0}) t := by
+  rw [disjoint_iff_forall_ne]
+  rintro v ⟨hvs, hv0 : v ≠ 0⟩ _ hvt rfl
+  exact hv0 <| (disjoint_def.1 hst) v (subset_span hvs) (subset_span hvt)
+
+theorem _root_.Disjoint.of_span₀ (hst : Disjoint (span R s) (span R t)) (h0s : 0 ∉ s) :
+    Disjoint s t := by
+  rw [← diff_singleton_eq_self h0s]
+  exact hst.of_span
+
 section
 
 variable (R M)