Existenzquantifikator in einem Topos

Question

Nehme an, dass $E$ist ein elementarer Topos. Also für jedes Objekt$X\in E$ man hat den entsprechenden existenziellen Quantifizierer $\exists_X:PX\rightarrow \Omega$. Meine Frage ist:

Was ist das Unterobjekt der Macht $PX$ klassifiziert durch $\exists_X$?

Ich vermute, dass dieses Unterobjekt nichts anderes als die Singleton-Map ist $\{\cdot\}_X:X\rightarrow PX$. Ist das richtig?

Answer 1

Es ist nicht nur die Singleton-Karte, sondern das Bild von $\pi_2\circ\epsilon:\in\;\hookrightarrow X\times PX\to PX$. Immerhin eine Formel gegeben$\varphi(x)$möchten Sie weiterhin, dass die existenzielle Quantifiziererkarte zurückkehrt $\top$ wenn $\{x:\varphi(x)\}$ hat mehr als ein Element - Sie möchten, dass es zurückkehrt $\top$ auf jeder nicht leeren "Teilmenge" von $X$.