refactor(algebra/inj_surj): more lemmas, move to files, rename (#3290)
* use names `function.?jective.monoid` etc;
* move definitions to different files;
* add versions for `semimodules` and various `*_with_zero`;
* add `funciton.surjective.forall` etc.