Finite generation as a quotient of a finite free module (source code)

= Finite generation as a quotient of a finite free module

An <R-module> is finitely generated exactly when it is the image of a <surjection> from a finite <free module> $R^n$. Given generators $m_i$, send $(r_i)$ to $\sum_i r_im_i$; conversely, the images of the standard free generators generate every such image. This criterion does not assert that the <module> is free: a quotient can have nontrivial relations.