While reading over Alperin's Local Representation Theory and reminding myself how a module is relatively H-projective iff H contains some vertex of the module, I realized I could not prove a basic lemma about relatively H-projective modules using my current favorite definition.
Definition: A G-module U is relatively H-projective if U is a direct summand of $(U_H)^G$.
Lemma: If H ≤ K ≤ G and U is a G-module that is relatively H-projective, then U is relatively K-projective.
Proof: Use Prop 9.1.2 to change definitions of relatively projective back to the good ole relative homological definition I used to like: H-split implies G-split. Clearly K-split implies H-split just by restricting the direct sum, but then relatively H-projectivity (Prop 9.1.2 style) gives G-split, but this suffices to show relative K-projectivity (Prop 9.1.2 style). $\square$
However, when I try to do this with $U|(U_H)^G$ I get confused and can't seem to use Mackey correctly. In Alperin's proof on page 67 he uses a similar but more convenient definition: that U is a direct summand of an induced H-module. Assuming my previous question is right, this is exactly the same as a direct summand of a relatively free module. However, I'm not sure I see how $U|(U_H)^G$ is equivalent to $U|S^G$ for some H-module S. Presumably this is Frobenius reciprocity, but again something is going wrong when I try to do it. At any rate, with the "S" definition it is just transitivity of induction, so I'd like to understand both.