Equational criterion for flatness (source code)

= Equational criterion for flatness
{title2=$\sum_i a_im_i=0\Longrightarrow m_i=\sum_jb_{ij}n_j,\quad\sum_i a_ib_{ij}=0$}

For a <flat module> $M$ over a <commutative ring>, every finite relation among elements of $M$ is a finite combination of relations among elements of the <ring> itself, in the displayed sense. To obtain this, tensor the kernel of the linear map $A^r\to A$, $(u_i)\mapsto\sum_i a_iu_i$, with $M$. Flatness says that this tensor maps onto the kernel in $M^r$. Writing an element of that tensor as a finite sum gives the columns $b_{ij}$ and the elements $n_j$. The converse follows by applying this condition to relations in a <tensor product> to prove that tensoring preserves injections.