Green mackey intersections force proper vertices

If $U$ is relatively $P$-projective, F6 gives $\alpha \in {\mathrm{End}}_{kP}(U)$ of relative trace $1_U$. In the tensor model the map $u\mapsto {\sum }_{t\in H\mathrm{/}P}t\otimes \alpha (t^{-1}u)$ splits $h\otimes u\mapsto hu$: reindexing the finite cosets proves $H$-linearity, and their composite is the relative trace. Thus with $W={\mathrm{Res}}_P^{H}U$ we have ${\mathrm{Ind}}_P^{H}W\cong U\oplus U^{\mathrm{\prime }}$ for a finite-dimensional $U^{\mathrm{\prime }}$.

Finite indecomposable decomposition and uniqueness make the family predicate closed under finite direct sums and direct summands: decompose each summand, and compare the resulting multisets. In particular, if a module is induced from a subgroup contained in a member of a family, transitivity makes each indecomposable summand relatively projective for that member. These uses of finite-length decomposition inherit AC.

Mackey for ${\mathrm{Res}}_H^G{\mathrm{Ind}}_P^{G}W$ splits the identity double coset from the others. The identity term is ${\mathrm{Ind}}_P^{H}W$; every remaining term is induced from $H\cap {}^{g}P$ with $g\mathrm{\notin }H$, so their sum $E_0$ is $\mathcal{Y}$-projective by 1.2. Separately, Mackey for induction from $H$ gives ${\mathrm{Res}}_H^G{\mathrm{Ind}}_H^{G}U\cong U\oplus E$ and the analogous $U^{\mathrm{\prime }}\oplus E^{\mathrm{\prime }}$ decomposition, since the identity double coset contributes exactly the original module. Transitivity and 1.1 now give $U\oplus U^{\mathrm{\prime }}\oplus E\oplus E^{\mathrm{\prime }}\cong U\oplus U^{\mathrm{\prime }}\oplus E_0$. Cancellation by uniqueness in F4 gives $E\oplus E^{\mathrm{\prime }}\cong E_0$. Hence $E$ is $\mathcal{Y}$-projective. This proves (a), including its complement assertion rather than just containment of $U$.

For (b), first take a module relatively projective for $D=P\cap {}^{s}P$ with $s\mathrm{\notin }H$. Use the finite inducing witness supplied in F3 and apply Mackey on restriction. Its terms are induced from subgroups $H\cap {}^{t}D=H\cap {}^{t}P\cap {}^{ts}P$. At least one of $t,ts$ lies outside $H$, since otherwise $s=t^{-1}(ts)\in H$. Thus each such subgroup is contained in a member of $\mathcal{Y}$. Step 1.2 proves the required family-projectivity for the restriction and for its summands. Decompose a general $\mathcal{X}$-projective module and apply this argument to each indecomposable; this proves (b).

For (c), decompose the given $H$-module into indecomposables $V$. Each is relatively $P$-projective, so F3 and F5 let us choose its vertex $Q$ inside $P$. Since $V$ is also $\mathcal{Y}$-projective, vertex containment gives $Q{\le }_H\mathcal{Y}$. By F2, $Q{\le }_G\mathcal{X}$. Transitivity makes ${\mathrm{Ind}}_H^{G}V$ relatively $Q$-projective and hence relatively projective for a member of $\mathcal{X}$: conjugating the inducing subgroup does not change the induced summand property, as follows also by multiplying its tensor representatives by the conjugator. Step 1.2 and finite additivity prove (c).

The last assertion follows from F2; no order bound on $\mathcal{Y}$ was used. When $H=G$, Mackey has only the identity coset, so $E=0$ in (a). The empty-family predicate holds only for the zero finite-dimensional module, by existence of finite decompositions; hence (b) and (c) also hold. When $P=1$, the normalizer condition forces $H=G$. Zero input modules give zero errors in all three assertions. This finishes the proof under the inherited AC assumption. [F2, F4, step 2.1, step 2.2, step 2.3] QED