Projective modules are direct summands of free modules (source code)

= Projective modules are direct summands of free modules
{title2=$P\text{ projective}\iff P\text{ is a direct summand of a free module}$}

Every <module> $P$ is a quotient of a <free module> $F=\bigoplus_{p\in P}Ae_p$, via $e_p\mapsto p$. If $P$ is a <projective module>, lift $1_P$ through this <surjection> to obtain a section $s:P\to F$. The resulting <split short exact sequence> identifies $F$ with $\ker\pi\oplus P$. Conversely, if $P$ is a summand of a <free module>, extend a prescribed map out of $P$ to the <free module> using the summand projection, lift each <basis> image through the given <surjection>, and restrict the lift to $P$. This proves the equivalence with the lifting definition of a <projective module>, for arbitrary ranks.