feat: miscellaneous linear algebra lemmas (#8157)

Mathlib/Algebra/Algebra/Basic.lean

@@ -361,6 +361,12 @@ theorem commutes (r : R) (x : A) : algebraMap R A r * x = x * algebraMap R A r :
   Algebra.commutes' r x
 #align algebra.commutes Algebra.commutes
 
+lemma commute_algebraMap_left (r : R) (x : A) : Commute (algebraMap R A r) x :=
+  Algebra.commutes r x
+
+lemma commute_algebraMap_right (r : R) (x : A) : Commute x (algebraMap R A r) :=
+  (Algebra.commutes r x).symm
+
 /-- `mul_left_comm` for `Algebra`s when one element is from the base ring. -/
 theorem left_comm (x : A) (r : R) (y : A) :
     x * (algebraMap R A r * y) = algebraMap R A r * (x * y) := by

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -130,12 +130,18 @@ def botEquivPUnit : (⊥ : Submodule R M) ≃ₗ[R] PUnit.{v+1} where
   right_inv _ := rfl
 #align submodule.bot_equiv_punit Submodule.botEquivPUnit
 
-theorem eq_bot_of_subsingleton (p : Submodule R M) [Subsingleton p] : p = ⊥ := by
-  rw [eq_bot_iff]
-  intro v hv
-  exact congr_arg Subtype.val (Subsingleton.elim (⟨v, hv⟩ : p) 0)
+theorem subsingleton_iff_eq_bot : Subsingleton p ↔ p = ⊥ := by
+  rw [subsingleton_iff, Submodule.eq_bot_iff]
+  refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
+    fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩
+
+theorem eq_bot_of_subsingleton [Subsingleton p] : p = ⊥ :=
+  subsingleton_iff_eq_bot.mp inferInstance
 #align submodule.eq_bot_of_subsingleton Submodule.eq_bot_of_subsingleton
 
+theorem nontrivial_iff_ne_bot : Nontrivial p ↔ p ≠ ⊥ := by
+  rw [iff_not_comm, not_nontrivial_iff_subsingleton, subsingleton_iff_eq_bot]
+
 /-!
 ## Top element of a submodule
 -/

Mathlib/Analysis/InnerProductSpace/Spectrum.lean

@@ -129,7 +129,7 @@ theorem orthogonalComplement_iSup_eigenspaces_eq_bot : (⨆ μ, eigenspace T μ)
   -- a self-adjoint operator on a nontrivial inner product space has an eigenvalue
   haveI :=
     hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_eigenspaces
-  exact Submodule.eq_bot_of_subsingleton _
+  exact Submodule.eq_bot_of_subsingleton
 #align linear_map.is_symmetric.orthogonal_supr_eigenspaces_eq_bot LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot
 
 theorem orthogonalComplement_iSup_eigenspaces_eq_bot' :

Mathlib/Data/Set/Function.lean

@@ -876,6 +876,17 @@ theorem surjOn_iff_surjective : SurjOn f s univ ↔ Surjective (s.restrict f) :=
     ⟨a, as, e⟩⟩
 #align set.surj_on_iff_surjective Set.surjOn_iff_surjective
 
+@[simp]
+theorem MapsTo.restrict_surjective_iff (h : MapsTo f s t) :
+    Surjective (MapsTo.restrict _ _ _ h) ↔ SurjOn f s t := by
+  refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
+  · obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩
+    replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
+    rw [← ha']
+    exact mem_image_of_mem f ha
+  · obtain ⟨a, ha, rfl⟩ := h' hb
+    exact ⟨⟨a, ha⟩, rfl⟩
+
 theorem SurjOn.image_eq_of_mapsTo (h₁ : SurjOn f s t) (h₂ : MapsTo f s t) : f '' s = t :=
   eq_of_subset_of_subset h₂.image_subset h₁
 #align set.surj_on.image_eq_of_maps_to Set.SurjOn.image_eq_of_mapsTo

Mathlib/LinearAlgebra/Basic.lean

@@ -837,6 +837,17 @@ theorem ker_le_ker_comp (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ
     ker f ≤ ker (g.comp f : M →ₛₗ[τ₁₃] M₃) := by rw [ker_comp]; exact comap_mono bot_le
 #align linear_map.ker_le_ker_comp LinearMap.ker_le_ker_comp
 
+theorem ker_sup_ker_le_ker_comp_of_commute {f g : M →ₗ[R] M} (h : Commute f g) :
+    ker f ⊔ ker g ≤ ker (f ∘ₗ g) := by
+  refine sup_le_iff.mpr ⟨?_, ker_le_ker_comp g f⟩
+  rw [← mul_eq_comp, h.eq, mul_eq_comp]
+  exact ker_le_ker_comp f g
+
+@[simp]
+theorem ker_le_comap {p : Submodule R₂ M₂} (f : M →ₛₗ[τ₁₂] M₂) :
+    ker f ≤ p.comap f :=
+  fun x hx ↦ by simp [mem_ker.mp hx]
+
 theorem disjoint_ker {f : F} {p : Submodule R M} : Disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 :=
   by simp [disjoint_def]
 #align linear_map.disjoint_ker LinearMap.disjoint_ker
@@ -1035,6 +1046,11 @@ theorem ker_le_iff [RingHomSurjective τ₁₂] {p : Submodule R M} :
     rw [h] at this
     simpa using this
 
+@[simp] theorem injective_restrict_iff_disjoint {p : Submodule R M} {f : M →ₗ[R] M}
+    (hf : ∀ x ∈ p, f x ∈ p) :
+    Injective (f.restrict hf) ↔ Disjoint p (ker f) := by
+  rw [← ker_eq_bot, ker_restrict hf, ker_eq_bot, injective_domRestrict_iff, disjoint_iff]
+
 end Ring
 
 section Semifield

Mathlib/LinearAlgebra/DFinsupp.lean

@@ -337,20 +337,35 @@ theorem biSup_eq_range_dfinsupp_lsum (p : ι → Prop) [DecidablePred p] (S : ι
     · simp [hp]
 #align submodule.bsupr_eq_range_dfinsupp_lsum Submodule.biSup_eq_range_dfinsupp_lsum
 
+/-- A characterisation of the span of a family of submodules.
+
+See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
 theorem mem_iSup_iff_exists_dfinsupp (p : ι → Submodule R N) (x : N) :
     x ∈ iSup p ↔
       ∃ f : Π₀ i, p i, DFinsupp.lsum ℕ (M := fun i ↦ ↥(p i)) (fun i => (p i).subtype) f = x :=
   SetLike.ext_iff.mp (iSup_eq_range_dfinsupp_lsum p) x
 #align submodule.mem_supr_iff_exists_dfinsupp Submodule.mem_iSup_iff_exists_dfinsupp
 
-/-- A variant of `Submodule.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded. -/
+/-- A variant of `Submodule.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded.
+
+See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
 theorem mem_iSup_iff_exists_dfinsupp' (p : ι → Submodule R N) [∀ (i) (x : p i), Decidable (x ≠ 0)]
     (x : N) : x ∈ iSup p ↔ ∃ f : Π₀ i, p i, (f.sum fun i xi => ↑xi) = x := by
   rw [mem_iSup_iff_exists_dfinsupp]
   simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
     LinearMap.toAddMonoidHom_coe, coeSubtype]
 #align submodule.mem_supr_iff_exists_dfinsupp' Submodule.mem_iSup_iff_exists_dfinsupp'
 
+lemma mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
+    x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x := by
+  classical
+  rw [mem_iSup_iff_exists_dfinsupp']
+  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
+  rintro ⟨f, hf, rfl⟩
+  refine ⟨DFinsupp.mk f.support <| fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
+  · ext; simp
+  · simp [Finsupp.mem_support_iff.mp hi]
+
 theorem mem_biSup_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N)
     (x : N) :
     (x ∈ ⨆ (i) (_ : p i), S i) ↔

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -922,6 +922,13 @@ theorem injective_iff_surjective [FiniteDimensional K V] {f : V →ₗ[K] V} :
         this).injective⟩
 #align linear_map.injective_iff_surjective LinearMap.injective_iff_surjective
 
+lemma injOn_iff_surjOn {p : Submodule K V} [FiniteDimensional K p]
+    {f : V →ₗ[K] V} (h : ∀ x ∈ p, f x ∈ p) :
+    Set.InjOn f p ↔ Set.SurjOn f p p := by
+  rw [Set.injOn_iff_injective, ← Set.MapsTo.restrict_surjective_iff h]
+  change Injective (f.domRestrict p) ↔ Surjective (f.restrict h)
+  simp [disjoint_iff, ← injective_iff_surjective]
+
 theorem ker_eq_bot_iff_range_eq_top [FiniteDimensional K V] {f : V →ₗ[K] V} :
     LinearMap.ker f = ⊥ ↔ LinearMap.range f = ⊤ := by
   rw [range_eq_top, ker_eq_bot, injective_iff_surjective]
@@ -959,6 +966,37 @@ theorem finrank_range_add_finrank_ker [FiniteDimensional K V] (f : V →ₗ[K] V
   exact Submodule.finrank_quotient_add_finrank _
 #align linear_map.finrank_range_add_finrank_ker LinearMap.finrank_range_add_finrank_ker
 
+theorem comap_eq_sup_ker_of_disjoint {p : Submodule K V} [FiniteDimensional K p] {f : V →ₗ[K] V}
+    (h : ∀ x ∈ p, f x ∈ p) (h' : Disjoint p (ker f)) :
+    p.comap f = p ⊔ ker f := by
+  refine le_antisymm (fun x hx ↦ ?_) (sup_le_iff.mpr ⟨h, ker_le_comap _⟩)
+  obtain ⟨⟨y, hy⟩, hxy⟩ :=
+    surjective_of_injective ((injective_restrict_iff_disjoint h).mpr h') ⟨f x, hx⟩
+  replace hxy : f y = f x := by simpa [Subtype.ext_iff] using hxy
+  exact Submodule.mem_sup.mpr ⟨y, hy, x - y, by simp [hxy], add_sub_cancel'_right y x⟩
+
+theorem ker_comp_eq_of_commute_of_disjoint_ker [FiniteDimensional K V] {f g : V →ₗ[K] V}
+    (h : Commute f g) (h' : Disjoint (ker f) (ker g)) :
+    ker (f ∘ₗ g) = ker f ⊔ ker g := by
+  suffices ∀ x, f x = 0 → f (g x) = 0 by rw [ker_comp, comap_eq_sup_ker_of_disjoint _ h']; simpa
+  intro x hx
+  rw [← comp_apply, ← mul_eq_comp, h.eq, mul_apply, hx, _root_.map_zero]
+
+theorem ker_noncommProd_eq_of_supIndep_ker [FiniteDimensional K V] {ι : Type*} {f : ι → V →ₗ[K] V}
+    (s : Finset ι) (comm) (h : s.SupIndep fun i ↦ ker (f i)) :
+    ker (s.noncommProd f comm) = ⨆ i ∈ s, ker (f i) := by
+  classical
+  induction' s using Finset.induction_on with i s hi ih; simpa using LinearMap.ker_id
+  replace ih : ker (Finset.noncommProd s f <| Set.Pairwise.mono (s.subset_insert i) comm) =
+      ⨆ x ∈ s, ker (f x) := ih _ (h.subset (s.subset_insert i))
+  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hi, mul_eq_comp,
+    ker_comp_eq_of_commute_of_disjoint_ker]
+  · simp_rw [Finset.mem_insert_coe, iSup_insert, Finset.mem_coe, ih]
+  · exact s.noncommProd_commute _ _ _ fun j hj ↦
+      comm (s.mem_insert_self i) (Finset.mem_insert_of_mem hj) (by aesop)
+  · replace h := Finset.supIndep_iff_disjoint_erase.mp h i (s.mem_insert_self i)
+    simpa [ih, hi, Finset.sup_eq_iSup] using h
+
 end DivisionRing
 
 end LinearMap

Mathlib/LinearAlgebra/Matrix/Gershgorin.lean

@@ -29,7 +29,7 @@ theorem eigenvalue_mem_ball {μ : K} (hμ : Module.End.HasEigenvalue (Matrix.toL
     ∃ k, μ ∈ Metric.closedBall (A k k) (∑ j in Finset.univ.erase k, ‖A k j‖) := by
   cases isEmpty_or_nonempty n
   · exfalso
-    exact hμ (Submodule.eq_bot_of_subsingleton _)
+    exact hμ Submodule.eq_bot_of_subsingleton
   · obtain ⟨v, h_eg, h_nz⟩ := hμ.exists_hasEigenvector
     obtain ⟨i, -, h_i⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty (fun i => ‖v i‖)
     have h_nz : v i ≠ 0 := by