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

Topos Theory

Field: Category Theory

The study of topos theory.

Sequence of Expressions

A Grothendieck topos is a category CC which satisfies any one of the following three properties. (A theorem of Jean Giraud states that the properties below are all equivalent.) - There is a small category DD and an inclusion C↪Presh⁡(D)C\hookrightarrow \operatorname {Presh} (D) that admits a finite-limit-preservingleft adjoint. - CC is the category of sheaves on a Grothendieck site. - CC satisfies Giraud's axioms, below. Here Presh⁡(D)\operatorname {Presh} (D) denotes the category of contravariant functors from DD to the category of sets; such a contravariant functor is frequently called a presheaf. Giraud's axioms for a category CC are: - CC has a small set of generators, and admits all small colimits. Furthermore, fiber products distribute over coproducts; that is, given a set II , an II -indexed coproduct mapping to AA , and a morphism A′→AA'\to A , the pullback is an II -indexed coproduct of the pullbacks: (∐i∈IBi)×AA′≅∐i∈I(Bi×AA′).\left(\coprod _{i\in I}B_{i}\right)\times _{A}A'\cong \coprod _{i\in I}(B_{i}\times _{A}A'). - Sums in CC are disjoint. In other words, the fiber product of XX and YY over their sum is the initial object in CC . - All equivalence relations in CC are effective. The last axiom needs the most explanation. If X is an object of C, an "equivalence relation" R on X is a map R → X × X in C such that for any object Y in C, the induced map Hom(Y, R) → Hom(Y, X) × Hom(Y, X) gives an ordinary equivalence relation on the set Hom(Y, X). Since C has colimits we may form the coequalizer of the two maps R → X; call this X/R. The equivalence relation is "effective" if the canonical map R→X×X/RX  ⁣R\to X\times _{X/R}X\,\! is an isomorphism.
Giraud's axioms for a category CC are: - CC has a small set of generators, and admits all small colimits. Furthermore, fiber products distribute over coproducts; that is, given a set II , an II -indexed coproduct mapping to AA , and a morphism A′→AA'\to A , the pullback is an II -indexed coproduct of the pullbacks: (∐i∈IBi)×AA′≅∐i∈I(Bi×AA′).\left(\coprod _{i\in I}B_{i}\right)\times _{A}A'\cong \coprod _{i\in I}(B_{i}\times _{A}A'). - Sums in CC are disjoint. In other words, the fiber product of XX and YY over their sum is the initial object in CC . - All equivalence relations in CC are effective. The last axiom needs the most explanation. If X is an object of C, an "equivalence relation" R on X is a map R → X × X in C such that for any object Y in C, the induced map Hom(Y, R) → Hom(Y, X) × Hom(Y, X) gives an ordinary equivalence relation on the set Hom(Y, X). Since C has colimits we may form the coequalizer of the two maps R → X; call this X/R. The equivalence relation is "effective" if the canonical map R→X×X/RX  ⁣R\to X\times _{X/R}X\,\! is an isomorphism.
Since the early 20th century, the predominant axiomatic foundation of mathematics has been set theory, in which all mathematical objects are ultimately represented by sets (including functions, which map between sets). More recent work in category theory allows this foundation to be generalized using topoi; each topos completely defines its own mathematical framework. The category of sets forms a familiar topos, and working within this topos is equivalent to using traditional set-theoretic mathematics. But one could instead choose to work with many alternative topoi. A standard formulation of the axiom of choice makes sense in any topos, and there are topoi in which it is invalid. Constructivists will be interested to work in a topos without the law of excluded middle. If symmetry under a particular groupG is of importance, one can use the topos consisting of all G-sets. It is also possible to encode an algebraic theory, such as the theory of groups, as a topos, in the form of a classifying topos. The individual models of the theory, i.e. the groups in our example, then correspond to functors from the encoding topos to the category of sets that respect the topos structure.
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.