¿Cuándo satisface un topos el axioma de regularidad?
En la teoría de conjuntos categórica, observamos que ciertos topoi satisfacen (versiones adecuadas de) ciertos axiomas de la teoría de conjuntos. Por ejemplo, Lawvere$\mathsf{ETCS}$ afirma que $\mathbf{Set}$ es un topos bien puntiagudo con un objeto de números naturales, que satisface el axioma (interno) de elección. $\mathsf{ETCS}$ se sabe que es equivalente a $\mathsf{BZC}$, un fragmento de $\mathsf{ZFC}$que no incluye regularidad.
Mi pregunta es: ¿qué se necesita para que un topos satisfaga (una versión adecuadamente redactada de) el axioma de regularidad? O tal vez alguna afirmación que sea equivalente (en presencia de la otra$\mathsf{ZFC}$ axiomas), según tengo entendido, la regularidad no es intuicionistamente aceptable.
Respuestas
La relación entre tópicos y teorías de conjuntos se estudió de forma exhaustiva en
Steve Awodey, Carsten Butz, Alex Simpson, Thomas Streicher: relacionar teorías de conjuntos de primer orden, tópicos y categorías de clases . Annals of Pure and Applied Logic, volumen 165, número 2, febrero de 2014, páginas 428-502
La regularidad se discute bajo el nombre de "fundamento". Puede encontrar muchos detalles en el documento, solo voy a revisar rápidamente la configuración.
Trabajamos en un topos elemental $\mathcal{E}$.
El primer paso es cocinar una noción de $\in$-afiliación. Definir un gráfico de membresía para que sea un triple$G = (|G|, A_G, r_G)$ dónde $|G|$ un $A_G$ son objetos y $r_G : |G| \to A_G + P|G|$un morfismo. Pensamos en$|G|$ como un conjunto de vértices con cada vértice $x \in |G|$ siendo un átomo $a$ (en caso $r(x) = \mathrm{inl}(a)$ por $a : A_G$) o un vértice de ramificación con conjunto de adyacencia $d \subseteq |G|$ (en caso $r(x) = \mathrm{inr}(d)$ por $d : P|G|$). Podemos definir una relación de bisimilitud$\sim_{G,H}$ entre dos gráficos de pertenencia que expresan el hecho de que, hasta el reordenamiento y la repetición, $G$ y $H$ representar lo mismo $\in$-estructura de membresía. En otras palabras,$\sim_{G,H}$ expresa la igualdad extensional de conjuntos representados por $G$ y $H$. En particular,$\sim_{G,G}$ es una relación de equivalencia que coienta el gráfico de pertenencia para dar una relación de pertenencia que es extensional.
A continuación, definimos un nuevo topos. $\mathcal{E}_\mathrm{nwf}$ cuyos objetos son triples $(D, m, G)$ dónde $G$ es un gráfico de membresía en $\mathcal{E}$, $D$ un objeto de $\mathcal{E}$, y $m : D \to |G|$ un mono en $\mathcal{E}$. Se concibe una noción adecuada de morfismo que tiene en cuenta las relaciones de bisimilitud$\sim_{G,H}$. Entonces tenemos:
Teorema 11.7: $\mathcal{E}_\mathrm{nwf}$ es equivalente a $\mathcal{E}$.
Podemos entender que el teorema dice que enriquecimos el topos $\mathcal{E}$ con relaciones de membresía para obtener $\mathcal{E}_\mathrm{nwf}$, que cambió el topos solo hasta la equivalencia (por lo que no de ninguna manera esencial desde el punto de vista de la teoría del topos).
Hasta ahora permitimos tanto los átomos como la relación de pertenencia no bien fundada. El siguiente paso es definir lo que significa para un gráfico de membresía.$G = (|G|, A_G, r_G)$estar bien fundado. Aquí no hay sorpresas, ya que podemos utilizar el lenguaje interno del topos para indicar cuándo$X : P|G|$ satisface la propiedad "$X$ contiene todos los átomos $A_G$ y está hereditariamente cerrado bajo la relación de membresía $r_G$"(ver la fórmula después del Corolario 11.2).
Definimos un tercer topos $\mathcal{E}_\mathrm{wf}$ como la subcategoría completa de $\mathcal{E}_\mathrm{nwf}$ de aquellos objetos cuyos gráficos de pertenencia están bien fundamentados.
Proposición 11.3: La equivalencia entre$\mathcal{E}$ y $\mathcal{E}_\mathrm{nwf}$ reduce a una equivalencia entre $\mathcal{E}$ y $\mathcal{E}_\mathrm{wf}$.
La moraleja de la historia es que, en primer lugar, podemos definir una noción de relación de pertenencia extensional en objetos en un topos, y en segundo lugar, que restringir a la parte bien fundada del topos no cambia el topos de una manera que sea relevante. a la teoría de topos.
En cierto sentido, la respuesta a la pregunta "cuándo un topos satisface el axioma de regularidad" es "no importa". Esto se analiza con más detalle en el artículo de la Sección 11.4, donde los autores concluyen con
... se deduce que cualquier topos puede interpretarse como un modelo de BIZFA− y como un modelo de BINWFA−.
Aquí BIZFA- es su formulación de teoría de conjuntos similar a ZF con fundamento (regularidad) y BIZWFA- una formulación de teoría de conjuntos similar a ZF con anti-fundamento.
Descargo de responsabilidad: no tome el resumen anterior como una descripción satisfactoria. El documento contiene muchos más detalles y explicaciones, y debe ser consultado para comprender en profundidad el tema.