Pushforward of module sheaves

Action identifies the top-section scalar action for every scheme morphism, without an affine or quasi-coherence hypothesis. BaseChange compares pushforward and restriction around any independent open square.