Comprender la enfermedad de Beck-Chevalley

Question

Una vez abierta la caja negra del teorema de la monadicidad de Beck, me gustaría hacer lo mismo con el descenso monádico. Mientras indago, sigo encontrándome con la condición de Beck-Chevalley.

Desgraciadamente, el entrada nlab está muy por encima de mi cabeza. Quiero entender la idea intuitiva detrás de esta condición en algunos casos concretos, pero ni siquiera sé cómo empezar.

¿Cuál es el significado intuitivo de la condición Beck-Chevalley, ya sea desde una perspectiva geométrica o lógica? (No conozco la teoría de tipos).

Answer 1

$\require{AMScd}$ Cuando haces geometría algebraica, puedes considerar diagramas como $$ \begin{CD} X @>f>> A\\ @VgVV \\ B \end{CD} $$ donde $X,A,B$ son espacios y $g,f$ sus mapas. Es bastante natural pensar que se trata de "funciones generalizadas" entre $A$ y $B$ . De hecho, se denominan "correspondencias" entre $A$ y $B$ y se organizan en una categoría que contiene su categoría de espacios de (en realidad dos) manera(s) canónica(s).

Moralmente, estos tipos corresponden a functores "pull-push" como $g_*f^* : D(A)\to D(B)$ . Pero hay una sutileza: para que sea una (bi)categoría bien definida, hay que especificar condiciones de coherencia en una ley de composición: lo más natural, dado un diagrama $$ \begin{CD} @. X @>f>> A\\ @. @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD} $$ es completarlo a un pullback $$ \begin{CD} P @>q>> X @>f>> A\\ @VpVV @VgVV \\ Y @>h>> B\\ @VkVV\\ C \end{CD} $$ Observe que tiene dos aparentemente diferentes maneras de leer su composición, ahora: la primera, como $(kp)_*(fq)^* = k_* p_* q^* f^*$ y el segundo como $k_* h^* g_* f^*$ . ¿Cuándo serán estos dos iguales (o mejor dicho, canónicamente isomorfos)?

Answer 2

La página de nLab tiene una discusión decente sobre la perspectiva lógica. El comienzo del artículo de Dusko Pavlovic de 1996 Mapas II: Diagramas de persecución en la teoría de las pruebas categóricas tiene también una descripción bastante legible de la situación. Lo que sigue es una forma significativamente elaborada del ejemplo de ese documento.

Antes de eso, quiero señalar una perspectiva diferente que se analiza en la sección 3 y, en particular, en la proposición 3.4 de la obra de Bart Jacobs Categorías de comprensión y semántica de la dependencia de tipos . Tenemos una 2-categoría de fibraciones sobre una categoría base (que es a su vez una fibra en fibración de fibraciones). Por tanto, podemos instanciar en ella la definición 2-categórica de adjunción. El resultado es una adjunción fibrada que es una adjunción (normal) de funtores cartesianos entre las categorías totales cuya unidad (o equivalentemente counit) es vertical que induce una adjunción en cada fibra que se preserva por reindexación. La pregunta obvia es: ¿cuándo una colección de adjuntos izquierda/derecha fibrados a fibras de un functor cartesiano da lugar a un adjunto izquierda/derecha fibrado? La respuesta es: exactamente cuando se cumple la condición (generalizada) de Beck-Chevalley.

Sea $\pi_! \dashv \pi^*$ donde $\pi^*$ es la imagen inversa de la proyección, llamada functor de debilitamiento, y $\pi_!$ es la imagen directa y corresponde a la cuantificación existencial, es decir $\pi_{!,B}(x:A,y:B\vdash P(x,y))$ corresponde a $x:A\vdash\exists y:B.P(x,y)$ . La imagen inversa $\pi_B^*(x:A\vdash P(x))$ corresponde a $x:A,y:B\vdash P(x)$ de ahí "debilitamiento". Ahora el problema es que hay dos maneras de conseguir $x:A\vdash \exists y:B.R(\sigma(x),y)$ a partir de $x:A,y:B\vdash R(x,y)$ . Primero podrías cuantificar existencialmente conseguir $x:A\vdash\exists y:B.R(x,y)$ y luego sustituir, o puede sustituir primero $x:A,y:B\vdash R(\sigma(x),y)$ y luego cuantificar existencialmente. El cuadrado de retroceso en la base es $$\require{AMScd} \begin{CD} A\stackrel{\times}{{}_{\pi_B,\sigma}} B @>\hat\pi_B>> A\\ @V\hat\sigma VV @VV\sigma V \\ A\times B @>\pi_B>> A \end{CD}$$ y obtenemos $\hat\pi_{!,B}\circ\hat\sigma^* \to \sigma^*\circ\pi_{!,B}$ . La transformación natural surge como se describe aquí y en este caso se parece a $$\cfrac{\cfrac{ x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}R(x,y)} {x:A\vdash\exists y:B.[\sigma(x)/x,y/y]_{x,y}[x/x]_{x,y}\exists w:B.R(x,w)}}{ \cfrac{x:A\vdash \exists y:B.[x/x]_{x,y}[\sigma(x)/x]_{x}\exists w:B.R(x,w)}{ x:A\vdash[\sigma(x)/x]_{x}\exists w:B.R(x,w)}}$$ donde estoy usando, por ejemplo $[\sigma(x)/x]_{x,y}$ como sustitución de $x$ con $\sigma(x)$ en función de las variables $x$ y $y$ . Que la implicación anterior sea una equivalencia es la condición de Beck-Chevalley.