feat: characterize when projections are almost 0 or almost id (leanprover-community#41038)

in the sense of `LinearMap.FiniteRangeSetoid`.

Author: ADedecker

Mathlib/Algebra/Module/LinearMap/FiniteRange.lean

@@ -235,6 +235,13 @@ lemma equiv_iff_hasFiniteRange [IsNoetherianRing K] {u v : V →ₗ[K] V₂} :
     u ≈ v ↔ (u - v).HasFiniteRange := by
   rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_hasFiniteRange]
 
+lemma equiv_zero_iff_hasNoetherianRange {u : V →ₗ[K] V₂} : u ≈ 0 ↔ u.HasNoetherianRange := by
+  simp [equiv_iff_hasNoetherianRange]
+
+lemma equiv_zero_iff_hasFiniteRange [IsNoetherianRing K] {u : V →ₗ[K] V₂} :
+    u ≈ 0 ↔ u.HasFiniteRange := by
+  simp [equiv_iff_hasFiniteRange]
+
 lemma equiv_iff_isNoetherian_quotient_eqLocus {u v : V →ₗ[K] V₂} :
     u ≈ v ↔ IsNoetherian K (V ⧸ eqLocus u v) := by
   rw [equiv_iff_hasNoetherianRange, hasNoetherianRange_iff_quotient_ker, eqLocus_eq_ker_sub]
@@ -269,6 +276,23 @@ lemma equiv_comp {u v : V →ₗ[K] V₂} {u' v' : V₂ →ₗ[K] V₃} (h : u 
     u' ∘ₗ u ≈ v' ∘ₗ v := by
   grw [equiv_comp_right h', equiv_comp_left h]
 
+lemma projection_equiv_zero_iff_isNoetherian {S T : Submodule K V} (hST : IsCompl S T) :
+    S.projection T hST ≈ 0 ↔ IsNoetherian K S := by
+  rw [equiv_zero_iff_hasNoetherianRange, hasNoetherianRange_iff_range, range_projection]
+
+lemma projection_equiv_zero {S T : Submodule K V} [IsNoetherian K S] (hST : IsCompl S T) :
+    S.projection T hST ≈ 0 :=
+  projection_equiv_zero_iff_isNoetherian hST |>.mpr inferInstance
+
+lemma projection_equiv_id_iff_isNoetherian {S T : Submodule K V} (hST : IsCompl S T) :
+    S.projection T hST ≈ id ↔ IsNoetherian K T := by
+  rw [Setoid.comm, equiv_iff_hasNoetherianRange, ← projection_eq_id_sub_projection,
+    hasNoetherianRange_iff_range, range_projection]
+
+lemma projection_equiv_id {S T : Submodule K V} [IsNoetherian K T] (hST : IsCompl S T) :
+    S.projection T hST ≈ id :=
+  projection_equiv_id_iff_isNoetherian hST |>.mpr inferInstance
+
 end FiniteRangeSetoid
 
 end Setoid
@@ -432,6 +456,13 @@ lemma IsQuasiInverse.of_comp_right {u : V →ₗ[K] V₂} {v : V₂ →ₗ[K] V
     (w ∘ₗ v).IsQuasiInverse u :=
   ⟨hw.1, IsRightQuasiInverse.of_comp_right hv.1 hw.2⟩
 
+lemma isQuasiInverse_subtype_projectionOnto {S T : Submodule K V} [IsNoetherian K T]
+    (hST : IsCompl S T) :
+    IsQuasiInverse S.subtype (S.projectionOnto T hST) := by
+  constructor
+  · grw [IsLeftQuasiInverse, ← FiniteRangeSetoid.projection_equiv_id hST, projection]
+  · simp [IsRightQuasiInverse, projectionOnto_comp_subtype]
+
 end QuasiInverse
 
 end LinearMap

Mathlib/Data/Setoid/Basic.lean

@@ -69,6 +69,9 @@ theorem trans' (r : Setoid α) : ∀ {x y z}, r x y → r y z → r x z := r.ise
 theorem comm' (s : Setoid α) {x y} : s x y ↔ s y x :=
   ⟨s.symm', s.symm'⟩
 
+theorem comm [Setoid α] {x y : α} : x ≈ y ↔ y ≈ x :=
+  ⟨Setoid.symm, Setoid.symm⟩
+
 open scoped Function -- required for scoped `on` notation
 
 /-- The kernel of a function is an equivalence relation. -/