En matemáticas , el teorema fundamental de la teoría topos establece que la rebanada de un topos sobre cualquiera de sus objetos es en sí mismo un topos. Además, si hay un morfismo en entonces hay un functor que conserva exponenciales y el clasificador de subobjetos .
El functor de retroceso
Para cualquier morfismo f en hay un "functor de retroceso" asociado que es clave en la demostración del teorema. Para cualquier otro morfismo g enque comparte el mismo codominio que f , su producto es la diagonal de su cuadrado de retroceso, y el morfismo que va desde el dominio de al dominio de f es opuesto ag en el cuadrado de retroceso, por lo que es el retroceso de g a lo largo de f , que se puede denotar como.
Tenga en cuenta que un topos es isomorfo al corte sobre su propio objeto terminal, es decir , por lo que para cualquier objeto A en hay un morfismo y por lo tanto un functor de retroceso , por eso cualquier rebanada también es un topos.
Por un trozo dado dejar denotar un objeto de la misma, donde X es un objeto de la categoría base. Luego es un functor que mapea: . Ahora aplica a . Esto produce
así es como el functor de retroceso mapas de objetos de a . Además, tenga en cuenta que cualquier elemento C del topos base es isomorfo a, por lo tanto si luego y así que eso es de hecho un funtor del topos base a su rebanada .
Interpretación lógica
Considere un par de fórmulas de suelo y cuyas extensiones y (donde el subrayado aquí denota el contexto nulo) son objetos del topos base. Luego implica si y solo si hay un monic de a . Si este es el caso, entonces, por teorema, la fórmula es cierto en la rebanada , porque el objeto terminal de los factores de corte a través de su extensión . En términos lógicos, esto podría expresarse como
para que rebanar por la extensión de correspondería a asumir como hipótesis. Entonces el teorema diría que hacer una suposición lógica no cambia las reglas de la lógica topos.
Referencias
- Colin McLarty, Categorías elementales, Topos elementales , Oxford University Press (1995), pág. 158