When is a cartesian closed category also locally cartesian closed

cartesian-closed-categoriescategory-theory

It is well-known that if $\mathcal{C}$ is a locally cartesian closed category with terminal object, then it is also cartesian closed. There are various examples of locally cartesian closed categories that are not cartesian closed and, conversely, there are various examples of cartesian closed categories that are not locally cartesian closed.

Concerning this last point, I tried to find in literature some sufficient condition ensuring that a cartesian closed category is also locally cartesian, but it seems that there is no sufficient condition. Hence, I ask you for some statement of the form:

Let $\mathcal{C}$ be a cartesian closed category. If $\mathcal{C}$ satisfies A, then $\mathcal{C}$ is a locally cartesian closed category.

Best Answer

By definition, a category with products is cartesian closed if and only if pushforwards along projection morphisms exist. It being locally cartesian closed means it has pullbacks and pushforwards along all morphisms. In a category with products, any morphism $f\colon X\to Y$ factors uniquely as $X\to X\times Y\to Y$ through the projection morphism $X\times Y\to Y$, where the "graph morphism" $X\to X\times Y$ is a section of the projection morphism $X\leftarrow X\times Y$. A necessary and sufficient condition for a cartesian closed category to be locally cartesian closed is then that pushforwards along such "graph morphisms" exist.

Given a pullback-stable class $\mathcal M$ of monomorphisms, a sufficient for pushforwards along morphisms in $M$ to exist can be extracted from the proof of the fundamental theorem of topos theory. The sufficient condition is then that every object $Y$ has a partial morphism classifier for partial morphisms with domains given by $\mathcal M$. In the presence of a subobject classifier, the condition is also necessary.

Related Question