feat: a submodule disjoint from a coFG module is FG (#41008)

... over a noetherian ring.

Also, over an arbitrary ring, a submodule codisjoint from a fg module is cofg.

This is a prerequisite for Fredholm operators.

Author: ADedecker

Mathlib/RingTheory/Finiteness/Cofinite.lean

@@ -49,10 +49,20 @@ theorem _root_.Module.Finite.iff_cofg_bot : (⊥ : Submodule R M).CoFG ↔ Modul
 theorem CoFG.fg_of_isCompl {S T : Submodule R M} (hST : IsCompl S T) (hS : S.CoFG) : T.FG :=
   Module.Finite.iff_fg.mp <| Module.Finite.equiv <| quotientEquivOfIsCompl S T hST
 
+/-- Over a noetherian ring, if `S` and `T` are disjoint and `T` is CoFG, then `S` is FG. -/
+theorem CoFG.fg_of_disjoint [IsNoetherianRing R] {S T : Submodule R M} (hST : Disjoint S T)
+    (hT : T.CoFG) : S.FG :=
+  .of_disjoint_of_isNoetherian_quotient hST
+
+/-- If `S` and `T` are co-disjoint and `S` is FG, then `T` is CoFG. -/
+theorem FG.cofg_of_codisjoint {S T : Submodule R M} (hST : Codisjoint S T) (hS : S.FG) :
+    T.CoFG :=
+  have := Module.Finite.iff_fg.mpr hS
+  .of_surjective (T.mkQ.domRestrict S) (by simp [← LinearMap.range_eq_top, hST.symm.eq_top])
+
 /-- A complement of an FG submodule is CoFG. -/
-theorem FG.cofg_of_isCompl {S T : Submodule R M} (hST : IsCompl S T) (hS : S.FG) : T.CoFG := by
-  haveI := Module.Finite.iff_fg.mpr hS
-  exact Module.Finite.equiv (quotientEquivOfIsCompl T S hST.symm).symm
+theorem FG.cofg_of_isCompl {S T : Submodule R M} (hST : IsCompl S T) (hS : S.FG) : T.CoFG :=
+  hS.cofg_of_codisjoint hST.codisjoint
 
 /-- A submodule that contains a CoFG submodule is CoFG. -/
 theorem CoFG.of_le {S T : Submodule R M} (hT : S ≤ T) (hS : S.CoFG) : T.CoFG := by

Mathlib/RingTheory/Noetherian/Basic.lean

@@ -382,6 +382,12 @@ lemma FG.of_le [IsNoetherianRing R] {S T : Submodule R M} (hT : T.FG) (hST : S 
   rw [← Module.Finite.iff_fg] at hT
   exact FG.of_le_of_isNoetherian hST
 
+/-- If `S` is disjoint from `T` and `M ⧸ T` is a noetherian module, then `S` is FG.
+See also `Submodule.CoFG.fg_of_disjoint`. -/
+theorem FG.of_disjoint_of_isNoetherian_quotient {S T : Submodule R M} [IsNoetherian R (M ⧸ T)]
+    (hST : Disjoint S T) : S.FG :=
+  Module.Finite.iff_fg.mp <| .of_injective (T.mkQ.domRestrict S) (by simp [hST.eq_bot])
+
 end Submodule
 
 universe w v u