# What is the monoidal equivalent of a locally cartesian closed category?

If a closed monoidal category is the monoidal equivalent of a Cartesian closed category, is there an analogous equivalent for locally cartesian closed categories? Is there a standard terminology or reference for such a construction?

• What would you want such a thing to do? The first problem that occurs to me is that I don't see why the slice categories of a monoidal category should even have a monoidal structure. May 6 '15 at 19:46
• Well, if we take "slices" to be part of the data – that is to say, if we start with an indexed (or fibred) category – then we could certainly speak of indexed monoidal categories and indexed monoidal closed categories. May 6 '15 at 20:22
• @Qiaochu - I am coming from a context of categorical logic, where we use pullbacks for everything (substitution, conjunction, weakening). Other operations are usually assumed to be pullback-stable as a matter of course. Now I am running into monoidal categories and I would like to know to what extent those manipulations can translate into a non-Cartesian context. May 6 '15 at 20:44
• @pnips Then you should look into linear logic. May 6 '15 at 22:26
• I think this question is skipping a key intermediate step: "What would be the monoidal equivalent of a category with finite limits" ? Cartesian closed is justs about product so the link with monoidal category is obvious, but locally cartesian closed is about general pullback, so finite limits, and there is no clear analogue of that in the monoidal world. Mar 18 at 14:40

In a certain sense a monoidal version of a slice category is a category of comodules over a cocommutative comonoid object. If $C$ is a cocommutative comonoid object in a monoidal category, then the category of comodules over it $\mathbf{Comod}(C)$ has a monoidal structure with the monoidal product defined in a standard way as a tensor product $\otimes_C$ over $C$. In the Cartesian case a comonoid is just an object, and $\mathbf{Comod}(C)$ coincides with the slice category.

From this point of view a "monoidal equivalent of a locally Cartesian closed category" is a monoidal category for which all $\mathbf{Comod}(C)$ are monoidal closed.

Locally Cartesian closed categories are examples. Another example is the opposite of the category of abelian groups $\mathbf{Ab}^\mathrm{op}$, since the category of modules $\mathbf{Mod}(R)$ over any commutative ring $R$ is a closed monoidal category (it is probably locally coclosed).

• If $C$ is a comonoid in $Ab^{op}$ (= monoid in $Ab$), then the category of comodules over $C$ is the opposite of the category of modules over $C$. The category of modules is closed, but its opposite is not, so $Ab^{op}$ is not an example of a locally monoidal closed category. Jan 13 '17 at 16:19
• So, are there any interesting examples of locally monoidal closed categories besides cartesian? Jan 13 '17 at 16:22

I think there is something intriguing and slightly mysterious going on here.

First, my proposed definition would be slightly different from Dimitri Chikladze's. I agree that the natural generalization of the slice categories $\mathcal V /C$ for $C \in \mathcal V$ should probably be the comodule categories $\mathbf{Comod}(C)$ for $C$ a commutative comonoid in $\mathcal V$. But to me, the fundamental way to characerize local cartesian closedness of $\mathcal V$ is that for $f: C \to D$ in $\mathcal V$, the reindexing functor $f_! : \mathcal V/C \to \mathcal V/D$ (defined by postcomposition) not only has a right adjoint $f^\ast$ (defined by pullback), but $f^\ast$ itself has a right adjoint $f_\ast$ (the local hom functor). So I would say:

Definition: A symmetric monoidal category $\mathcal V$ is locally closed if for every commutative comonoid homomorphism $f: C \to D$ in $\mathcal V$, the reindexing functor $f_!$ fits into an adjoint string $f_! \dashv f^\ast \dashv f_\ast$ satisfying Beck-Chevalley conditions.

The strange thing here is when we look at examples. If $\mathcal V$ has certain nice limits and colimits (e.g. $\mathcal V = \mathsf{Ab}^{\mathrm{op}}$), then we always have an adjoint string $f^! \dashv f_! \dashv f^\ast$ (where $f^\ast$ and $f^!$ are respectively induction and coinduction of modules if $\mathcal V = \mathsf{Ab}^\mathrm{op}$). But the extra adjoint $f^!$ is on the wrong side! In order for $f^\ast$ to have a right adjoint, it must be flat when viewed as a monoid homomorphism in $\mathcal V^\mathrm{op}$.

I can't think of a noncocartesian example of a $\mathcal V^\mathrm{op}$ for which all commutative monoid homomorphisms are flat -- even $\mathsf{Vect}_k$ for $k$ a field doesn't seem to work. So it looks like in noncartesian cases, we're already doing what we do with cartesian categories like $\mathsf{Cat}$ -- exponentiability of a morphism is an important property that one is often interested in, but it's just not reasonable to expect every morphism to be exponentiable.

But perhaps there are natural subcategories of all commutative comonoids which have better exponentiability properties in some cases.

• @HarryGindi That would be really cool if true. I would be careful, though, given that the cartesian product is not exponentiable on Cat or qCat. In that case, you can define a local hom at the level of simplicial sets, but it doesn't play well with Joyal fibrant replacement. So there are issues to consider... Jun 10 '18 at 21:44
• Maybe a reasonable analogue of the triple $(f_{!},f^{*},f_{*})$ for general monoidal categories would be the "change of rings" triple adjunction for bicomodules in $\mathcal{V}$, as in Chapter 3 of Aguiar's thesis.
– Théo
May 24 at 23:36

I think there is another, more logically related way around the problem of defining a "locally monoidal closed category", if your intuition is coming from Type Theory/Logic. Have a look at "Categorical Models of Explicit Substitutions" (with Neil Ghani and Eike Ritter), Proc FOSSACS-99, LNCS 1578, Springer-Verlag, 1999. So there we were modelling categorically a type theory with explicit substitutions, but the expl subs are a bit of a red herring. the point is that you need pullbacks to do your substitutions into terms, but in the fibers you only want to have a symmetric monoidal closed category (as you want a model of LL), not a CCC. so you glue together fibers that are smccs, using a presheaf and this is enough to get a "locally monoidal closed category-look-alike", that did the job for us. maybe it works for you too: if you want to have dependent products, presumably you have to "sew" together the two "fibrations" in a compatible way. We haven't done that for that project, but we vaguely considered it.

The proposed use of comonoid homomorphisms in the other answers is intriguing, but there are more basic things about locally cartesian closed categories that need to be loosened first, although conceivably the homomorphisms generalise what I am about to say.

We have known for decades that substitution is pullback, though I haven't seen a formalisation and proof of this other than the one in Chapter VIII of my book.

Lawvere said that the quantifiers adjoint to substitution, but that is not accurate: they are actually adjoint to weakening.

Also, the two legs of a pullback do not play the same role: one is substitution or weakening and other is the display of a type.

There is a more subtle version of the traditional notion in which the adjoints are only required over a certain pullback-stable class of "display maps".

Plain and local cartesian closure are the extremes in which this class consists of just product projections or all maps, respectively.

In particular, the quantifiers over diagonals ($$X\to X\times X$$) are oddities that I will leave as an exercise.

It would be interesting to see how the other proposals on this page fit together with this.