Minimal supported subobject (source code)

= Minimal supported subobject

For a limit-preserving <functor> $U$ and an arrow $d:D\to UC$, a supported <subobject> is $m:M\hookrightarrow C$ through which $d$ factors after applying $U$. In a complete well-powered domain, their intersection remains supported. At the resulting pair $(C_0,d_0)$, every supported <subobject> of $C_0$ is invertible. This minimality makes $q\mapsto U(q)d_0$ injective on morphisms to each cogenerator.