= Frobenius reciprocity for subobjects
{c}
{title2=$\exists_f(A\cap f^*B)=\exists_f(A)\cap B$}
In a <category> with <pullback in a category> constructions and <image factorizations>, direct image $\exists_f(A')=\operatorname{im}(A'\hookrightarrow A\xrightarrow{f}B)$ is a <left adjoint> to inverse image on <subobjects>. Frobenius reciprocity is $\exists_f(A'\cap f^*B')=\exists_f(A')\cap B'$. It holds for all such subobjects exactly when <strong epimorphisms> are stable under pullback along <monomorphisms>. For sufficiency pull the strong part of the image factorization back along the mono into its intersection with $B'$; for necessity take $A'=A$ and $f$ strong, whose image is the whole codomain.
Back to article page
