¿Cuál es el equivalente monoidal de una categoría cerrada localmente cartesiana?

Question

Si una categoría cerrada monoidal es el equivalente monoidal de una categoría cerrada cartesiana, ¿existe un equivalente análogo para las categorías cerradas localmente cartesianas? ¿Existe una terminología estándar o una referencia para tal construcción?

Answer 1

En cierto sentido, una versión monoidal de una categoría de cortes es una categoría de códulos sobre un objeto comonoide cocomutativo. Si $C$ es un objeto comonoide conmutativo en una categoría monoidal, entonces la categoría de códulos sobre ella $\mathbf{Comod}(C)$ tiene una estructura monoidal con el producto monoidal definido de forma estándar como un producto tensorial $\otimes_C$ en $C$ . En el caso cartesiano un comonoide es sólo un objeto, y $\mathbf{Comod}(C)$ coincide con la categoría de las rodajas.

Desde este punto de vista, un "equivalente monoidal de una categoría cerrada localmente cartesiana" es una categoría monoidal para la que todas $\mathbf{Comod}(C)$ son monoidales cerrados.

Las categorías cerradas localmente cartesianas son ejemplos. Otro ejemplo es el opuesto de la categoría de grupos abelianos $\mathbf{Ab}^\mathrm{op}$ ya que la categoría de módulos $\mathbf{Mod}(R)$ sobre cualquier anillo conmutativo $R$ es una categoría monoidal cerrada (probablemente esté localmente cohesionada).

Answer 2

Creo que aquí hay algo intrigante y ligeramente misterioso.

En primer lugar, mi propuesta de definición sería ligeramente diferente a la de Dimitri Chikladze. Estoy de acuerdo en que la generalización natural de las categorías de rodajas $\mathcal V /C$ para $C \in \mathcal V$ probablemente deberían ser las categorías del comodín $\mathbf{Comod}(C)$ para $C$ un comonoide conmutativo en $\mathcal V$ . Pero para mí, la forma fundamental de caracterizar la cerrazón cartesiana local de $\mathcal V$ es que para $f: C \to D$ en $\mathcal V$ el functor de reindexación $f_! : \mathcal V/C \to \mathcal V/D$ (definida por postcomposición) no sólo tiene un adjunto derecho $f^\ast$ (definido por el pullback), pero $f^\ast$ tiene un adjunto derecho $f_\ast$ (el functor hom local). Así que yo diría:

Definición: Una categoría monoidal simétrica $\mathcal V$ es cerrado localmente si para cada homomorfismo comonoide conmutativo $f: C \to D$ en $\mathcal V$ el functor de reindexación $f_!$ encaja en una cadena adyacente $f_! \dashv f^\ast \dashv f_\ast$ satisfaciendo las condiciones de Beck-Chevalley.

Lo extraño aquí es cuando miramos los ejemplos. Si $\mathcal V$ tiene ciertos límites y colímites agradables (por ejemplo $\mathcal V = \mathsf{Ab}^{\mathrm{op}}$ ), entonces siempre tenemos una cadena adyacente $f^! \dashv f_! \dashv f^\ast$ (donde $f^\ast$ y $f^!$ son respectivamente inducción y coinducción de módulos si $\mathcal V = \mathsf{Ab}^\mathrm{op}$ ). Pero el adjunto extra $f^!$ ¡está en el lado equivocado! Para que $f^\ast$ para tener un adjunto derecho, debe ser plano cuando se ve como un homomorfismo monoide en $\mathcal V^\mathrm{op}$ .

No se me ocurre un ejemplo no cocartesiano de un $\mathcal V^\mathrm{op}$ para los que todos los homomorfismos monoides conmutativos son planos -- incluso $\mathsf{Vect}_k$ para $k$ un campo no parece funcionar. Así que parece que en los casos no cartesianos, ya estamos haciendo lo que hacemos con las categorías cartesianas como $\mathsf{Cat}$ -- La exponenciabilidad de un morfismo es una propiedad importante que a menudo interesa, pero no es razonable esperar que todos los morfismos sean exponenciables.

Pero quizás haya subcategorías naturales de todos los comonoides conmutativos que tengan mejores propiedades de exponenciabilidad en algunos casos.

Answer 3

Creo que hay otra forma, más relacionada con la lógica, de evitar el problema de definir una "categoría cerrada localmente monoidal", si tu intuición proviene de la Teoría de Tipos/Lógica. Echa un vistazo a "Categorical Models of Explicit Substitutions" (con Neil Ghani y Eike Ritter), Proc FOSSACS-99, LNCS 1578, Springer-Verlag, 1999. Así que ahí estábamos modelando categóricamente una teoría de tipos con sustituciones explícitas, pero los subs explícitos son un poco una pista falsa. la cuestión es que necesitas pullbacks para hacer tus sustituciones en términos, pero en las fibras sólo quieres tener una categoría cerrada simétrica monoidal (como quieres un modelo de LL), no una CCC. Así que pegas las fibras que son smccs, usando un presheaf y esto es suficiente para obtener una "categoría cerrada localmente monoidal-parecida", que hizo el trabajo para nosotros. tal vez funciona para ti también: si quieres tener productos dependientes, presumiblemente tienes que "coser" las dos "fibraciones" de una manera compatible. No lo hemos hecho para ese proyecto, pero lo hemos considerado vagamente.

Answer 4

El uso propuesto de los homomorfismos comonoides en las otras respuestas es intrigante, pero hay cosas más básicas sobre las categorías cerradas localmente cartesianas que necesitan ser aflojadas primero, aunque concebiblemente los homomorfismos generalizan lo que voy a decir.

Hace décadas que sabemos que la sustitución es un retroceso, aunque no he visto una formalización y prueba de esto más que la de Capítulo VIII de mi libro .

Lawvere dijo que los cuantificadores se unen a sustitución pero eso no es exacto: en realidad son adyacentes a debilitamiento .

Además, las dos patas de un pullback no juegan el mismo papel: una es la sustitución o debilitamiento y la otra es la visualización de un tipo .

Existe una versión más sutil de la noción tradicional en la que los adyacentes sólo se requieren sobre una determinada clase de "mapas de visualización" estables al retroceso.

El cierre cartesiano simple y el local son los extremos en los que esta clase está formada sólo por proyecciones del producto o por todos los mapas, respectivamente.

En particular, los cuantificadores sobre diagonales ( $X\to X\times X$ ) son rarezas que dejaré como ejercicio.

Sería interesante ver cómo encajan las otras propuestas de esta página con esto.