feat(linear_algebra/free_module): add module.free.resolution (#8231)

Any module is a quotient of a free module. This is stated as surjectivity of `finsupp.total M M R id : (M →₀ R) →ₗ[R] M`.

Author: riccardobrasca

src/algebra/module/projective.lean

@@ -51,7 +51,6 @@ https://en.wikipedia.org/wiki/Projective_module
 
 - Direct sum of two projective modules is projective.
 - Arbitrary sum of projective modules is projective.
-- Any module admits a surjection from a projective module.
 
 All of these should be relatively straightforward.
 

src/linear_algebra/finsupp.lean

@@ -433,6 +433,22 @@ theorem total_unique [unique α] (l : α →₀ R) (v) :
   finsupp.total α M R v l = l (default α) • v (default α) :=
 by rw [← total_single, ← unique_single l]
 
+lemma total_surjective (h : function.surjective v) : function.surjective (finsupp.total α M R v) :=
+begin
+  intro x,
+  obtain ⟨y, hy⟩ := h x,
+  exact ⟨finsupp.single y 1, by simp [hy]⟩
+end
+
+theorem total_range (h : function.surjective v) : (finsupp.total α M R v).range = ⊤ :=
+range_eq_top.2 $ total_surjective R h
+
+/-- Any module is a quotient of a free module. This is stated as surjectivity of
+`finsupp.total M M R id : (M →₀ R) →ₗ[R] M`. -/
+lemma total_id_surjective (M) [add_comm_monoid M] [module R M] :
+  function.surjective (finsupp.total M M R id) :=
+total_surjective R function.surjective_id
+
 lemma range_total : (finsupp.total α M R v).range = span R (range v) :=
 begin
   ext x,

src/linear_algebra/free_module.lean

@@ -15,6 +15,8 @@ import logic.small
 We introduce a class `module.free R M`, for `R` a `semiring` and `M` an `R`-module and we provide
 several basic instances for this class.
 
+Use `finsupp.total_id_surjective` to prove that any module is the quotient of a free module.
+
 ## Main definition
 
 * `module.free R M` : the class of free `R`-modules.