= Finite projective module
= Finitely generated projective module
{synonym}
A finite projective module is a <finitely generated module> that is a <projective module>. Equivalently it is a direct summand of a finite <free module>: a finite free surjection splits by projectivity. Its <dual module> is finite projective and its evaluation map to its <double dual module> is an <isomorphism>, since both properties hold for finite free modules and pass to direct summands. Finite generation is needed for this elementary duality argument.
Back to article page
