Topos theory [tt-004U]
Topos theory [tt-004U]
definition 1. topos [kostecki2011introduction, 7.1] [tt-004O]
definition 1. topos [kostecki2011introduction, 7.1] [tt-004O]
A topos or elementary topos is a category satisfying one of these equivalent conditions:
- it is a complete category with exponentials and subobject classifier
- it is a complete category with subobject classifier and its power object
- it is a cartesian closed category with equalizers and subobject classifier
Since the completeness of a category with subobject classifier implies its cocompleteness. Thus a topos not only has all finite limits, but also has all finite colimits.
This means that topos is such category which has, in particular,
- terminal object
- equalizers
- pullbacks
- all other limits
- exponential objects
- subobject classifier
remark 2. topoi, toposes [kostecki2011introduction, 7.1] [tt-004P]
remark 2. topoi, toposes [kostecki2011introduction, 7.1] [tt-004P]
The name "topos" originates from the Greek word "τoπoς", meaning a place, as topos could mean a place of geometry, and at the same time as a place of logic.
Following the ancient Greek naming convention, the plural of topos is topoi, but people also use toposes. We use them interchangeably.
example 3. topos [tt-004R]
example 3. topos [tt-004R]
Topos theory unifies, in an extraordinary way, important aspects of geometry and logic.
Grothendieck topos was first introduced by Grothendieck to generalize topological space [kostecki2011introduction, 7.2]:
every space gives rise to a topos (namely, the category of sheaves on it).
Topological properties of the space can be reinterpreted in a useful way as categorical properties of its associated topos.
Elementary topos was introduced by Lawvere and Tierney, to generalize Set. A topos can be regarded as a 'universe of sets' [leinster2016basic, 6.3.20]. \(\mathbf {Set}\) is the most basic example of a topos, and every topos shares enough features with Set that [⧉]
anything you really really needed to do in the category of sets can be done in any topos.
Every presheaf category, is a topos. [leinster2016basic, 6.3.27]
A topos can allow the interpretation of a higher-order logic. In particular, objects can be seen as collections of elements of a given type, subobjects are viewed as propositions. Products and coproducts are interpreted as conjunction and disjunction respectively. For an introduction, see [pitts2001categorical].
definition 4. geometric morphism, Topoi [kostecki2011introduction, 7.2] [tt-004Q]
definition 4. geometric morphism, Topoi [kostecki2011introduction, 7.2] [tt-004Q]
If \({\cal E}_1\) and \({\cal E}_2\) are toposes, then a geometric morphism \(\mathscr {G}: {\cal E}_1 \to {\cal E}_2\) is defined as a pair of adjoint functors \(\mathscr {G}^* \dashv \mathscr {G}_*\) between \({\cal E}_1\) and \({\cal E}_2\), such that \(\mathscr {G}^*\) preserves finite limits (i.e. is left exact), which implies \(\mathscr {G}_*\) preserves colimits (i.e. is right exact).
The category of toposes and their geometric morphisms is denoted \(\mathbf {Topoi}\).