feat: add Module.Finite.of_exact (leanprover-community#34243)

Also add two `stacks` tags for https://stacks.math.columbia.edu/tag/0519.

Author: eric-wieser

Mathlib/RingTheory/Finiteness/Basic.lean

@@ -235,6 +235,7 @@ variable {S} {P : Type*} [Semiring S] [AddCommMonoid P] [Module S P]
   {σ : R →+* S} [RingHomSurjective σ]
 
 -- TODO: remove RingHomSurjective
+@[stacks 0519 "(3)"]
 theorem of_surjective [hM : Module.Finite R M] (f : M →ₛₗ[σ] P) (hf : Surjective f) :
     Module.Finite S P :=
   ⟨by

Mathlib/RingTheory/Finiteness/Finsupp.lean

@@ -10,6 +10,7 @@ public import Mathlib.Algebra.MonoidAlgebra.Module
 public import Mathlib.LinearAlgebra.Finsupp.LinearCombination
 public import Mathlib.LinearAlgebra.Quotient.Basic
 public import Mathlib.RingTheory.Finiteness.Basic
+public import Mathlib.Algebra.Exact
 
 /-!
 # Finiteness of (sub)modules and finitely supported functions
@@ -113,11 +114,22 @@ theorem fg_ker_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P)
   · rwa [inf_of_le_right (show (LinearMap.ker f) ≤
       (LinearMap.ker g).comap f from comap_mono bot_le)]
 
+/-- If $M → N → P → 0$ is exact and $M$ and $P$ are finitely generated then so is $N$.
+
+This is the `Module.Finite` version of `Submodule.fg_of_fg_map_of_fg_inf_ker`. -/
+@[stacks 0519 "(1)"]
+lemma _root_.Module.Finite.of_exact {f : M →ₗ[R] N} {g : N →ₗ[R] P}
+    (h_exact : Function.Exact f g) (h_surj : Function.Surjective g)
+    [Module.Finite R M] [Module.Finite R P] : Module.Finite R N := by
+  refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩
+  · rw [← LinearMap.range_eq_top] at h_surj
+    rw [Submodule.map_top, h_surj]
+    exact Module.Finite.fg_top
+  · simp [LinearMap.exact_iff.1 h_exact]
+
 theorem _root_.Module.Finite.of_submodule_quotient (N : Submodule R M) [Module.Finite R N]
-    [Module.Finite R (M ⧸ N)] : Module.Finite R M where
-  fg_top := fg_of_fg_map_of_fg_inf_ker N.mkQ
-    (by simpa only [map_top, range_mkQ] using Module.finite_def.mp ‹_›) <| by
-    simpa only [top_inf_eq, ker_mkQ] using .of_finite
+    [Module.Finite R (M ⧸ N)] : Module.Finite R M :=
+  .of_exact (LinearMap.exact_subtype_mkQ N) (Quotient.mk_surjective _)
 
 end Submodule