Elementary topos

Template:Short description In mathematics, an elementary topos (plural toposes or topoiTemplate:Sfn) is a category which has properties making it resemble the category of sets. Elementary toposes can be used as models of intuitionistic higher-order logic.

Introduction

An elementary topos (hereafter just topos) can be pictured as an alternate mathematical universe.Template:R It is a category which is sufficiently like the category of sets (the “standard mathematical universe”) that common mathematical constructions can be carried in it, such as subsets, function spaces, etc.

More precisely, a topos supports intuitionistic higher-order logic as an internal languageTemplate:Sfn. As such, toposes are widely used as models of constructive mathematics.

Definition

As originally defined by Lawvere and Tierney, an elementary topos is a category $ℰ$ such that:Template:SfnTemplate:Sfn

• $ℰ$ is finitely complete (it has all finite limits). Equivalently, it has a terminal object, binary products, and binary equalizers.
• $ℰ$ is finitely cocomplete (it has all finite colimits). Equivalently, it has an initial object, binary coproducts and binary coequalizers.
• $ℰ$ has exponential objects (in addition to binary products, which are required for defining exponential objects). Together with having a terminal object and binary products, this means that $ℰ$ is Cartesian closed.
• $ℰ$ has a subobject classifier.

The requirement that $ℰ$ be finitely cocomplete was later observed to be redundant, as it follows from the rest.Template:SfnTemplate:SfnTemplate:Sfn (However, the general construction of finite colimits is relatively complicated; in most examples, one can find a more concrete description, which simplifies the translation of statements from the internal language.)

An even more minimalistic definition is possible: an elementary topos is a finitely complete category with power objects.Template:Sfn (This essentially replaces the requirements to have exponentials $A^B$ and a subobject classifier $\mathrm{\Omega }$ with just the special case of exponentials ${\mathrm{\Omega }}^B$.)

Many other properties follow, such as being regular and moreover exactTemplate:SfnTemplate:Sfn.

Logical functors

A logical functor is a functor between topoi that preserves finite limits and power objects. Logical functors preserve the structures that topoi have. In particular, they preserve finite colimits, subobject classifiers, and exponential objects.

Examples

Having a subobject classifier is a strong requirement, which rules out most categories of algebraic structures such as groups, rings, etc.Template:R

Every Grothendieck topos (a category equivalent to the category of sheaves on a site) is an elementary topos. Important special cases include:

• For any small category $𝒞$, the presheaf category ${\mathrm{Set}}^{{𝒞}^{\mathrm{op}}}$.
• As a further special case of the previous example, for any group $G$, the category of $G$-sets, i.e., sets equipped with an action of $G$, with equivariant maps as morphisms.
• For any topological space $X$, the category of sheaves on $X$.
• The classifying topos for a geometric theory.

The category of finite sets is an elementary toposTemplate:Sfn (however, it lacks a natural numbers object), and similarly for finite $G$-sets.

The effective topos is an important example of an elementary topos with natural numbers object. It is not a Grothendieck topos.Template:R It can be viewed as a universe of computable mathematics. This example is generalized by realizability toposes.

A source of examples is the fundamental theorem of topos theory, which states that for every elementary topos $ℰ$ and every object $\mathrm{\Gamma }\in ℰ$, the slice category $ℰ/\mathrm{\Gamma }$ is an elementary topos.

See also

• History of topos theory
• Intuitionistic type theory

Bibliography

• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite book
• Template:Cite web