Let $V$ be a complete and cocomplete cartesian closed category. Feel free to assume more about $V$ if necessary; in my application $V$ is simplicial sets, so it is a presheaf topos and hence has all sorts of nice properties you might want (except that its underlying-set functor $V(1,-) : V \to \rm Set$ is not faithful or conservative).

Let $C$ be a complete and cocomplete $V$-enriched category with powers and copowers (a.k.a. cotensors and tensors), hence all $V$-enriched weighted limits. And suppose that the underlying ordinary category $C_0$ is cartesian closed, i.e. we have natural isomorphisms of hom-sets

$$ C_0(X\times Y, Z) \cong C_0(X, Z^Y). $$

Is it necessarily the case that $C$ is also cartesian closed in the $V$-enriched sense, i.e. we have $V$-natural isomorphisms of $V$-valued hom-objects

$$ C(X\times Y, Z) \cong C(X, Z^Y)? $$

I can't decide whether I think this is likely to be true or not. I used to believe that it was true, and I believe I have implicitly used it (or more precisely its generalization to the locally cartesian closed case, which should follow from the simple one applied to enriched slice categories) in a published paper or two. However, right now I can't see how to prove it, and when stated clearly it sounds unlikely, since usually it is an extra condition on an adjunction between enriched categories to be an enriched adjunction (even when one of the functors is known to be an enriched functor, as is the case here for the cartesian product). On the other hand, it is true when $C=V$ itself: a cartesian closed category, defined by an isomorphism of hom-sets, automatically enhances to an isomorphism of hom-objects $Z^{X\times Y} \cong (Z^X)^Y$.

  • $\begingroup$ My spidey sense says that the only way this could fail would be for stupid set theoretic reasons, if your categories are too far from being locally presentable. (I don't make a wager about that case --- perhaps there are no set theoretic obstructions.) But I agree I cannot answer the question. $\endgroup$ Commented Jan 31, 2019 at 0:59
  • 2
    $\begingroup$ It is not hard to reduce to the case $X=1$. Your question is equivalent to asking whether $C(Y,Z) \overset?= C(1,Z^Y)$. $\endgroup$ Commented Jan 31, 2019 at 1:00
  • 4
    $\begingroup$ Which is in turn equivalent to asking whether $(A\otimes 1) \times Y \overset?= A\otimes Y$, for $A \in V$ and $Y \in C$. $\endgroup$ Commented Jan 31, 2019 at 1:02
  • $\begingroup$ @TheoJohnson-Freyd Good point about $X=1$. $\endgroup$ Commented Jan 31, 2019 at 6:06
  • 1
    $\begingroup$ Hmm, actually maybe that isn't quite enough: the large category we embed it in will still have $(A\otimes 1)\times Y \ncong A\otimes Y$, but it may not be cartesian closed. However, I've now constructed such a $D$, which seems to me to be a big step towards a negative answer, so I'll post it below. $\endgroup$ Commented Jan 31, 2019 at 9:31

3 Answers 3


I believe I managed to cook up an actual counterexample where both $C$ and $V$ are presheaf toposes. I'm going to leave my original attempt below since I still think it is instructive.

Let $V$ be presheaves over the category of finite sets $\mathsf{Fin}$ and let $C$ be preasheaves over the poset $\mathbb{N}$ (i.e., towers of sets). Then $C$ carries a $V$-enrichment given as $C(X, Y)_A = C_0(X, m \mapsto Y_{m |A|})$ for $A \in \mathsf{Fin}$ and $X, Y \in C$. This makes $C$ into a (co)tensored $V$-category, but internal homs in $C$ are not enriched.

This does look quite criptic. Let me explain this as an instance of a general construction.

Let's take two small categories $P$ and $J$ with $P$ symmetric monoidal and acting on $J$. Then we set $V$ to be presheaves on $P$ with Day convolution and $C$ presheaves on $J$. We construct a $V$-enrichment as follows. Let $F_p \colon J \to J$ be the action of $p \in P$ on $J$. This extends via a left Kan extension to a functor $L_p \colon C \to C$ which has a right adjoint $R_p \colon C \to C$. We set $C(X, Y)_p = C_0(X, R_p Y)$. This makes $C(X, Y)$ into a $P$-presheaf and the composition operations are induced by the $P$-action of $J$. We also have (co)tensors. The tensor of $X \in C$ by a representable presheaf $P(-,p)$ is $L_p X$ and the cotensor is $R_p X$ (and they extend by (co)limits to all presheaves).

$C$ is clearly cartesian closed and I believe there are many cases when the internal homs are not $V$-enriched. My old example below has a variant with $P = \mathbb{Z}/2$ (as a discrete monoidal category) and $J = \Delta$ with action by opposites.

In order to make $V$ cartesian, we can just take $P$ cartesian, e.g., $P = \mathsf{Fin}$. Then a natural candidate for $J$ is some category with finite coproducts so that $P$ acts by tensors. I took $J = \mathbb{N}$ to keep things easy, but I don't know if this is really the simplest choice. If we compute the functors $R_A$ for $A \in \mathsf{Fin}$, we indeed get $(R_A X)_m = X_{m |A|}$.

Now, let $A = \mathbf{2}$ be a two element set. Then $C(X \times Y, Z)_\mathbf{2} = C_0(X \times Y, R_\mathbf{2} Z) = C_0(X, (R_\mathbf{2} Z)^Y)$ and $C(X, Z^Y)_\mathbf{2} = C_0(X, R_\mathbf{2} (Z^Y))$, but $(R_\mathbf{2} Z)^Y$ and $R_\mathbf{2} (Z^Y)$ are clearly different in general.

Original answer

This is not an answer, but it is a bit too long for a comment. And perhaps it provides some hint towards an actual solution. Basically, I have a counterexample where the monoidal structure of $V$ is not cartesian, but I don't see if it can be modified to make it cartesian.

Let $V$ be the category of $\mathbb{Z}/2$-graded sets. The category $C = \mathsf{Cat}$ has a nice $V$-enrichment where even morphisms are covariant functors and odd morphisms are contravariant functors. It also has (co)tensors, the tensor of a category $X$ by a graded set $A$ is $X \times A_0 \sqcup X^{\mathrm{op}} \times A_1$ and the cotensor is $X^{A_0} \times (X^{\mathrm{op}})^{A_1}$. However, the internal homs in $C$ (with respect to the cartesian monoidal structure) are not enriched. Indeed, the odd elements of $C(X \times Y, Z)$ are functors that are contravariant in both $X$ and $Y$, but the odd elements of $C(X, Z^Y)$ are functors that are contravariant only in $X$.

  • 2
    $\begingroup$ Very nice! I feel like I should have thought of that myself. $\endgroup$ Commented Feb 6, 2019 at 12:21
  • $\begingroup$ FWIW, I think it would have been better to leave your old answer here (e.g. my previous comment only refers to the old answer, now it doesn't make much sense any more) and post a new answer with your updated construction. But the updated version is very nice! Am I right that the action of $V$ on $C$ is really just the same Day convolution formula applied to the action $P\times J\to J$ instead of a monoidal structure? $\endgroup$ Commented Feb 10, 2019 at 16:35
  • $\begingroup$ I agree about the old answer, but it didn't occur to me at first and I guess it's too late to change it now. And yes, I believe that you are right about the action. $\endgroup$ Commented Feb 10, 2019 at 20:11
  • $\begingroup$ It seems that more generally, instead of $P$ acting directly on $J$ and extending to $[J^{\rm op},\rm Set]$ by convolution, we could let $P$ act directly on any locally presentable category through cocontinuous functors. Reid's answer is an instance of this generalization, for the even simpler choice of $P = \mathbf{2}$. Right? $\endgroup$ Commented Feb 10, 2019 at 23:41

Here is an interesting construction that may be relevant, though it doesn't quite answer the question.

Firstly, note that as Theo says, it suffices to assume $X=1$, i.e. to ask whether $C(1,Z^Y) \cong C(Y,Z)$. For if this is true, then for any $X$ we have

$$ C(X\times Y,Z) \cong C(1, Z^{X\times Y}) \cong C(1,(Z^Y)^X) \cong C(X,Z^Y). $$

Secondly, as Theo also says, note that by adjointness and the Yoneda lemma, it suffices to ask whether $(A\odot 1)\times Y\cong A\odot Y$ for all $A\in V$, where $\odot$ denotes the copower of $C$ over $V$. For we have isomorphisms

$$ V_0(A,C(1,Z^Y)) \cong C_0(A\odot 1, Z^Y) \cong C_0((A\odot 1)\times Y,Z) $$

$$ V_0(A,C(Y,Z)) \cong C_0(A\odot Y,Z).$$

Now this question $(A\odot 1)\times Y\cong A\odot Y$ does not refer to cartesian closedness of $C$. And if we drop the hypothesis that $C$ is cartesian closed, then this isomorphism can fail, even when $C$ is complete and cocomplete and otherwise nice (even locally presentable, if $V$ is). To show this, it suffices to exhibit a small $V$-category $D$ containing an object $Y$, a terminal object $1$, copowers $A\odot 1$ and $A\odot Y$, and a product $(A\odot 1)\times Y$, for some $A\in V$, such that $(A\odot 1)\times Y\ncong A\odot Y$. For if we have such a $D$, let $C$ be the full subcategory of the functor $V$-category $[D^{\rm op},V]$ spanned by those functors $F$ that preserve the two copowers $A\odot 1$ and $A\odot Y$. Then $C$ is reflective in $[D^{\rm op},V]$, hence complete and cocomplete (and locally presentable, if $V$ is), and the embedding $D\hookrightarrow C$ preserves the two copowers, as well as the terminal object and the product, and is fully faithful so it also preserves the non-isomorphism. (But, there seems no reason in general why $C$ should be cartesian closed.)

Finally, to produce such a $D$ we can use the time-honored technique of looking at a universal example. Consider the $V$-category $D$ with exactly those five objects, which is "freely generated" by the requirement that the two copowers, the terminal object, and the product have their appropriate universal properties. The hom-objects of this category are given in the following table ($D(x,y)$ is in the $x$-row and the $y$-column).

$$ \begin{array}{c|ccccc} \nearrow & A\odot 1 & A\odot Y & Y & (A\odot 1)\times Y & 1 \\\hline A\odot 1 & A^A & \emptyset & \emptyset & \emptyset & 1 \\ A\odot Y & A^A & A^A & 1 & A^A & 1 \\ Y & A & A & 1 & A & 1 \\ (A\odot 1)\times Y & A^A & A & 1 & A^A & 1 \\ 1 & A & \emptyset & \emptyset & \emptyset & 1 \\ \end{array} $$

(This is assuming there are no morphisms $A\to \emptyset$ in $V$, as is the case whenever $A$ is not initial since $V$ is cartesian closed.) I will leave it as an exercise for the reader to define all 125 composition maps, check the 50 identity equations and 625 associativity equations to be sure we have a category, and check that 20 induced maps are isomorphisms to be sure we have the right universal properties (we don't need to check "freeness" of $D$; all that matters is that it exists, although we used the idea of freeness to construct it). And before you ask, yes, I actually did that exercise myself, although Coq helped a lot. (-:

In particular, the composition map

$$D((A\odot 1)\times Y, A\odot Y) \times D(A\odot Y, (A\odot 1)\times Y) \to D(A\odot Y,A\odot Y)$$

is the morphism $A \times A^A \to A^A$ whose adjunct $A\times A^A \times A\to A$ is projection onto the first copy of $A$. In other words, $A \times A^A \to A^A$ factors through the "inclusion of constant functions" $A\to A^A$, and thus as long as $A$ is nontrivial it can never yield the identity. Hence $(A\odot 1)\times Y\ncong A\odot Y$ in $D$.

So to summarize: the question can be stated in an equivalent form about copowers, and if we drop the assumption of cartesian closedness then the answer to that related question becomes false. So if the statement is true, it would have to be some kind of exactness property following from cartesian closedness, not due to any general fact about copowers.

  • 1
    $\begingroup$ Tip of the hat for the formal proof check that your category is what you claim it is! $\endgroup$
    – David Roberts
    Commented Jan 31, 2019 at 21:09
  • $\begingroup$ Is the exercise about doing the computation without Coq, or rather about coding the proof in Coq? $\endgroup$
    – fosco
    Commented Jan 31, 2019 at 21:46
  • 1
    $\begingroup$ @FoscoLoregian The exercise is to do the proof. I found it helpful to use a proof assistant to assist me in doing the proof, and others might likewise. In particular, a 5-line tactic script in Coq was able to prove all 625 associativity equations automatically without any thought on my part, saving me a lot of work. (Do that in Agda! (-: ) In fact, when I first defined composition I made a couple of mistakes, so the proof of associativity failed and showed me where the mistakes were. But, if you'd rather write them all out by hand, be my guest. (-: $\endgroup$ Commented Feb 1, 2019 at 0:04
  • $\begingroup$ Is it obvious that having powers (that is, cotensors) will not require additional restrictions that would damage the counterexample? $\endgroup$ Commented Feb 3, 2019 at 22:44
  • 1
    $\begingroup$ @მამუკაჯიბლაძე Passing to the presheaf category $[D^{\rm op},V]$ introduces all cotensors and the subcategory $C$ is closed under them, just like all other $V$-limits. $\endgroup$ Commented Feb 3, 2019 at 23:47

$\require{AMScd}$As Theo noted, the question amounts to whether the action $A \odot Y$ is given by the formula $(A \odot 1) \times Y$. The algebraic analogue would be to ask whether a module $C$ over a ring $V$ which also happens to have a ring structure is automatically a $V$-algebra. Of course there is no reason that this should be true, and if not for the condition in the question that $V$ and $C$ be cartesian monoidal categories, it ought to be easy to pick a simple counterexample in algebra and cook up a corresponding enriched category. However, I don't know how to extend the analogy to incorporate the cartesian condition, so instead let's just try simple cartesian closed categories $V$ and see what happens.

Obviously $V = \mathrm{Set}$ is too simple. Perhaps the next simplest example is $V = \mathcal{P}(\cdot \to \cdot) = \mathrm{Set}^{\cdot \leftarrow \cdot}$, where $\mathcal{P}(A)$ denotes the category of presheaves on $A$. Let's label the morphism of $\cdot \to \cdot$ as $e : u \to i$ and write $\mathbf{y}$ for the Yoneda embedding. Then the category $V$ is freely generated under colimits by the morphism $\mathbf{y}e : \mathbf{y}u \to \mathbf{y}i$. The object $\mathbf{y}i$ is also the terminal object of $V$ so let's denote it by $1_V$. We also see that the diagonal map $\mathbf{y}u \to \mathbf{y}u \times \mathbf{y}u$ is an isomorphism. Then, informally, it appears that $V$ with its cartesian closed structure as an "algebra" (~ closed symmetric monoidal locally presentable category) is generated by the object $\mathbf{y}u$ together with a morphism $\mathbf{y}e : \mathbf{y}u \to 1_V$ and an isomorphism $\mathbf{y}u \times \mathbf{y}u \to \mathbf{y}u$ inverting the diagonal map of $\mathbf{y}u$.

Now suppose $C$ is a category enriched, tensored and cotensored over $V$. Then the tensor $- \odot - : V \times C \to C$ is an adjunction of two variables, so it is determined by specifying the left adjoints $U(-) = \mathbf{y}u \odot - : C \to C$ and $1_V \odot - : C \to C$, which we can identify with $\mathrm{id}_C$, together with a natural transformation $\varepsilon : U \to \mathrm{id}_C$. Furthermore the diagonal map $\mathbf{y}u \to \mathbf{y}u \times \mathbf{y}u$ induces a natural transformation $$ \delta : U = \mathbf{y}u \odot - \to (\mathbf{y}u \times \mathbf{y}u) \odot - \cong \mathbf{y}u \odot (\mathbf{y}u \odot -) = U \circ U $$ which is easily seen to (together with $\varepsilon$) make $U$ into a comonad on $C$. Moreover, it is an idempotent comonad because the diagonal map of $\mathbf{y}u$ is an isomorphism.

To construct an example we need the converse direction, so suppose that $C$ is a complete and cocomplete category equipped with an idempotent comonad $U$ which is also a left adjoint. I claim that $C$ then has the structure of a category enriched, tensored and cotensored over $V$ for which $\mathbf{y}u \odot - = U(-)$. We could write down the enrichment (the Hom-objects are given by $C(X, Y) = (\varepsilon_X^* : \mathrm{Hom}(UX, Y) \leftarrow \mathrm{Hom}(X, Y))$) and cotensor and check a lot of conditions but I'll instead assume that $C$ is a locally presentable category and equip it with the structure of a (pseudo)module over $V$. The construction is just the above argument in reverse. A functor $\alpha : V \otimes C \to C$ (recall $V = \mathcal{P}(\cdot \to \cdot)$) is specified by a functor from $\cdot \to \cdot$ to the category of left adjoints $C \to C$, that is, a natural transformation between left adjoints, for which we take $\varepsilon : U \to \mathrm{id}_C$. We must give an associator which is a natural transformation between the two functors $V \otimes V \otimes C \to C$ built from $\alpha$ and the multiplication $\times$ on $V$; since $\times$ factors through the construction $\mathcal{P}$, this amounts to giving a natural isomorphism between two squares

\begin{CD} U @>1>> U\\ @V 1 V V @VV \varepsilon V\\ U @>>\varepsilon> \mathrm{id}_C \end{CD} and \begin{CD} U \circ U @>U\varepsilon>> U\\ @V \varepsilon U V V @VV \varepsilon V\\ U @>>\varepsilon> \mathrm{id}_C \end{CD} for which we take the comultiplication of $U$ (which is an isomorphism) in the top-left corner and the identity elsewhere. The unitor between $C \to V \otimes C \to C$ and the identity $C \to C$ is an equality. Finally, we have to check two commutative diagrams. The pentagon identity is an equality between two natural transformations between left adjoints $V \otimes V \otimes V \otimes C \to C$. We may check it object-wise on the generators $\mathbf{y}u$ and $\mathbf{y}i$ of $V$. When all the $V$ generators are $\mathbf{y}u$, this is the coassociativity of $U$. In the remaining cases it should be a formal identity (though I haven't checked). Similarly the relation between the unitor and the associator should reduce to the counitality of $U$. Thus the action $\alpha : V \otimes C \to C$ amounts to giving $C$ the desired structure. (There may well be a more high-brow way of describing this whole construction, but this way is just about manageable.)

Now, for a counterexample to the original question, it suffices to find a locally presentable cartesian closed category $C$ together with an idempotent comonad $U$ which is a left adjoint but for which the natural transformation $UY \to U1_C \times Y$ is not an isomorphism. For example, we could take $C$ to be simplicial sets and $U$ to be the 0-skeleton functor, sending a simplicial set $Y$ to $Y_0$ viewed as a discrete simplicial set. Then $UY$ is 0-skeletal, but $U1 \times Y = Y$ is not.

  • $\begingroup$ Unfortunately I can only accept one answer, but this one adds some extra to Karol's: you can choose an even simpler cartesian monoidal $P = (\cdot \to\cdot)$ than his, and rather than acting on a small $J$ and extending to presheaves by convolution, you can have it act directly on a locally presentable category by cocontinuous functors. $\endgroup$ Commented Feb 10, 2019 at 23:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.