Beta Phase: Square45 is currently in beta testing. Expect some features or content to be incomplete or missing.
45

Formal definition

📜

The statement of the theorem

When used for foundational work a topos will be defined axiomatically; set theory is then treated as a special case of topos theory. Building from category theory, there are multiple equivalent definitions of a topos. The following has the virtue of being concise: A topos is a category that has the following two properties: - All limits taken over finite index categories exist. - Every object has a power object. This plays the role of the powerset in set theory. Formally, a power object of an object XX is a pair (PX,∋X)(PX,\ni _{X}) with ∋X⊆PX×X{\ni _{X}}\subseteq PX\times X , which classifies relations, in the following sense. First note that for every object II , a morphism r ⁣:I→PXr\colon I\to PX ("a family of subsets") induces a subobject {(i,x) ∣ x∈r(i)}⊆I×X\{(i,x)~|~x\in r(i)\}\subseteq I\times X . Formally, this is defined by pulling back ∋X\ni _{X} along r×X:I×X→PX×Xr\times X:I\times X\to PX\times X . The universal property of a power object is that every relation arises in this way, giving a bijective correspondence between relations R⊆I×XR\subseteq I\times X and morphisms r ⁣:I→PXr\colon I\to PX . From finite limits and power objects one can derive that - All colimits taken over finite index categories exist. - The category has a subobject classifier. - The category is Cartesian closed. In some applications, the role of the subobject classifier is pivotal, whereas power objects are not. Thus some definitions reverse the roles of what is defined and what is derived.