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

Question

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?

Answer 1

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).

Answer 2

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.

Answer 3

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.

Answer 4

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.