El formalismo de los seis funtores en una teoría de cohomología dada consiste en que para cada espacio hay una categoría derivada de láminas y seis formas diferentes de construir funtores entre esas categorías (cuatro que implican un morfismo y dos sólo un espacio). Consiste entonces en muchas coherencias - son isomorfismos entre ciertas composiciones de estos functores y, en formulaciones modernas, homotopías entre ciertas combinaciones de estos isomorfismos, 2-homotopías entre ciertas composiciones de estas homotopías, etcétera.
En Notas de Peter Scholze sobre seis formalismos de funtores da una definición precisa, atribuida a Lukas Mann, y la cierra diciendo:
Observamos que aquí no son necesarias más coherencias: Los colindantes adquieren automáticamente todas coherencias pertinentes.
Qué matemáticas ¿se está reclamando aquí? ¿Cómo sabemos que las coherencias adquiridas son todas las pertinentes? ¿Nos da ese conocimiento una algoritmo para demostrar que se obtiene una coherencia deseada?
En el caso de un formalismo de tres funtores, incluyendo sólo $\otimes, f^*, f_!$ (es decir, ignorando los colindantes mencionados en el pasaje citado), sé básicamente cómo responder a todas estas preguntas. El formalismo de los tres funtores es un funtor que va de una cierta categoría infinita de correspondencias a la categoría infinita de todas las categorías infinitas. Cada functor surge de una correspondencia, por lo que una composición de functores surge de una composición de correspondencias. Comprobar que dos funtores son isomorfos significa calcular las correspondencias pertinentes y comprobar que son isomorfos, y esto funciona para todos los isomorfismos clásicos del formalismo de los seis funtores que implican sólo a esos funtores (secuencia espectral de Leray con soportes compactos, simetría y asociatividad del producto tensorial, functorialidad del pullback, fórmula de Künneth, cambio de base propio, fórmula de proyección, los productos tensoriales son compatibles con los pullbacks). Comprobar que dos isomorfismos de este tipo son iguales significa evaluar dos isomorfismos de correspondencias, que en última instancia dan isomorfismos de esquemas, y comprobar que son iguales.
Pero cuando aparecen colindantes ya no sé cómo hacerlo. ¿Debo dibujar algún diagrama en el que las correspondencias estén conectadas con cadenas?