 Finite projective module

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.