First-year graduateCategory TheoryPlanned

Elementary topos theory

Elementary toposes as categories that behave like categories of sets (finite limits, exponentials and a subobject classifier); presheaf and sheaf toposes; internal intuitionistic logic; and Lawvere's ETCS as a categorical axiomatisation of sets.

math.cat.elementary-topoi

Show everything needed to reach this topic

The lesson for this topic has not been written yet. The outline below is part of the curriculum map and has not been reviewed.

Builds on

Categorical logic Limits and colimits The Yoneda lemma

Required prerequisites, all the way down: 33

You will learn to

Verify the topos axioms for Set and for presheaf categories [Cᵒᵖ, Set], computing their subobject classifiers.
Show that the internal logic of a topos is intuitionistic, and give a presheaf topos whose logic is not Boolean.
State the axioms of ETCS and compare them with ZFC.

Definition

An elementary topos is a category with finite limits, exponentials and a subobject classifier.
A subobject classifier is a morphism true : 1 → Ω such that every monomorphism is the pullback of true along a unique morphism to Ω.
A Grothendieck topos is a category equivalent to the category of sheaves on a site.

Theorem

Every presheaf category [Cᵒᵖ, Set] on a small category C is a topos.
The subobjects of any object of a topos form a Heyting algebra.
Set is a Boolean topos, while the topos of presheaves on the poset {0 < 1} is not Boolean.
ETCS without a replacement axiom is strictly weaker than ZFC in consistency strength.

Common misconceptions

Thinking a topos is a kind of topological space; every space gives a topos of sheaves, but many toposes do not arise in this way.
Believing the internal logic of every topos is classical because that of Set is.

Optional discoveries

∞-categories ∞-toposes extend topos theory to homotopy theory, and they model homotopy type theory.
← ZFC: axiomatic set theory
← Representable functors
← Forcing and independence
← Sheaves