Lifting property of a free module (source code)

= Lifting property of a free module
{title2=$\phi q=\psi$}

For a <free module> $F$, a <surjective> <module homomorphism> $\phi:P\to M$, and a <module homomorphism> $\psi:F\to M$, there is a <module homomorphism> $q:F\to P$ satisfying $\phi q=\psi$. Choose a preimage under $\phi$ of the image of each element of a <basis of a module> of $F$, and extend by linearity. Thus every <free module> is a <projective module>.