CatDat

Implication Details

Assumptions: cofiltered limitsextensiveterminal object

Conclusions: cocartesian cofiltered limits

Proof: Let C\C be an extensive category with cofiltered limits and a terminal object. Then the coproduct functor C×CC/1×C/1C/(1+1)\C \times \C \cong \C/1 \times \C/1 \to \C/(1+1) is an equivalence. The forgetful functor C/AC\C/A \to \C creates connected limits, and hence preserves cofiltered limits. For every XCX \in \C the functor (X,):CC×C(X,-) : \C \to \C \times \C also preserves cofiltered limits. The composition of these functors is X:CCX \sqcup - : \C \to \C and therefore also preserves cofiltered limits.

Show 22 categories using this implication