La condición de Beck-Chevalley

Ya hemos demostrado una versión de Beck-Chevalley, pero en esta versión empezamos con un mono \(k\colon B\to A\). Ahora quitaremos esa hipótesis adicional y obtendremos el mismo resultado.

Empezamos recordando que si \(f\colon B\to A\) es una flecha en \(\mathcal{E}\), entonces la imagen inversa \(f^{-1}\colon Sub(A)\to Sub (B)\) tiene adjunto izquierdo \(\exists_f\colon Sub(B)\to Sub(A)\). Este adjunto izquierdo se evalúa en un subobjeto \(U\rightarrowtail B\) componiendo con \(f\), obteniendo \(U\rightarrowtail B\to A\) y luego calculando la imagen de esa composición (la factorización epi-mono) \(\exists_f U\rightarrowtail A\).

Si usamos las adjunciones \(\exists_f \dashv f^{-1}\) y \(a\land - \dashv (a\Rightarrow -)\) podemos obtener \[\exists_f W\land U = \exists_f(W\land f^{-1}U)\]

para cualesquiera \(U\in Sub(A)\) y \(W\in Sub(B)\).

Además, es posible demostrar una versión externa de la condición de Beck-Chevalley. El objetivo principal de esta sección es demostrar una versión interna de Beck-Chevalley, así que tenemos que hacer un trabajo de internalización de resultados externos. Es suficiente internalizar-externalizar objetos parcialmente ordenados, morfismos entre ellos y adjunciones entre los morfismos.

Con lo que ya tenemos del proceso de internalizar resultados externos y la condición de Beck-Chevalley externa podemos obtener la versión interna que Beck-Chevalley que nos interesa. Más explícitamente, para cualquier \(f\colon B\to A\) la flecha \(Pf\colon PA\to PB\) tiene adjunto izquierdo interno \(\exists f\colon PB\to PA\) y se satisface \[\exists q\, Pp=Pg\, \exists f\]

Para encontrar al adjunto izquierdo interno de \(Pf\) usamos que \(f^{-1}\colon Sub(A)\to Sub(B)\) tiene adjunto izquierdo \(\exists_f\colon Sub(B)\to Sub(A)\), inducido por el adjunto izquierdo del funtor cambio de base \(f^*\colon\mathcal{E}/A\to\mathcal{E}/B\). Así, podemos repetir el proceso con el adjunto derecho del cambio de base para obtener un adjunto derecho interno de \(Pf\), denotado \(\forall f\colon PB\to PA\), que satisface una condición de Beck-Chevalley para el universal, \[\forall p\, Pq = Pf\, \forall g\]