Bunch of small changes

Algebra: adjointness lemma for Hom and restriction
Descent: add correct reference
Dualizing: add reference
parse.py: add comment on use needs_proof variable