Topos Theory¶
Job: organize elementary toposes as categories of “variable sets” with internal logic; connect sheaf toposes, geometry, and geometric morphisms.
Core¶
A topos is a category with enough structure to interpret higher-order intuitionistic logic and to host sheaf-like geometry. Two historical streams: Grothendieck toposes (sheaves on sites) and elementary toposes (Lawvere–Tierney axioms).
| Layer | Content |
|---|---|
| Elementary axioms | finite limits, exponentials, subobject classifier |
| Subobject classifier | \(\Omega\); characteristic maps; truth values |
| Internal logic | Mitchell–Bénabou language; Kripke–Joyal |
| Sheaf toposes | \(\mathbf{Sh}(C,J)\); étale spaces; geometry |
| Geometric morphisms | \(f^*\dashv f_*\); inverse/direct image |
| Logic links | forcing, independence, synthetic domain theory |
Reading map¶
| Page | Focus |
|---|---|
| Foundations | elementary axioms, \(\Omega\), sheaves, internal logic, geometric morphisms |
| Classifying & Geometric | classifying topos \(\mathbf{B}[T]\), geometric theories, Caramello bridges, Morita |
| Boolean & Forcing | Boolean \(\neg\neg\), Cohen forcing, independence of CH, Solovay, LEM/intuitionistic |
| Cohesive & Higher | cohesive Lawvere, ∞-topos Lurie, Schreiber differential cohomology, shape/flat/sharp |
| Synthetic & Infinitesimal | SDG Kock, \(D=\{d:d^2=0\}\), Kock–Lawvere axiom, Cahiers \(C^\infty\) |
Dependency order¶
- Category theory (limits, adjoints, Yoneda)
- Logic (first-order / intuitionistic connectives)
- Algebraic geometry (sites, étale / Zariski motivations when present)
- This section; then \(\infty\)-toposes \(\leftrightarrow\) HoTT
Where it appears¶
- Foundations of algebraic geometry (Grothendieck topologies; fppf, étale toposes)
- Independence proofs / forcing as sheaves on posets
- Synthetic differential geometry (well-adapted models)
- Semantics of type theory and higher toposes
- Condensed mathematics — condensed sets are sheaves on profinite sets, a Grothendieck topos
See it¶
Sets form a topos. \(\mathbf{Set}\): \(\Omega=\{0,1\}\), exponentials \(B^A\), finite limits — the “constant sets” baseline. Presheaves \(\mathbf{Set}^{C^{\mathrm{op}}}\) are always toposes; sheafification for a topology \(J\) yields \(\mathbf{Sh}(C,J)\), the geometric examples (sheaves on a space \(X\) \(\simeq\) \(\mathbf{Sh}(X)\)).
Check¶
Why is the subobject classifier not just ‘a terminal object for monos’?
It classifies monomorphisms via pullback of a universal mono \(\mathsf{true}:1\to\Omega\). Every mono \(m:A\rightarrowtail B\) is a pullback of \(\mathsf{true}\) along a unique \(\chi_m:B\to\Omega\). Terminal object alone does not provide truth values or power objects.
Name one statement true in all toposes and one that needs classical logic.
True intuitionistically: existence of power objects; \(\Omega\)-logic with \(\land,\Rightarrow,\forall\). Needs Boolean topos / classical logic: \(\forall p:\Omega.\, p\lor\neg p\) (LEM); not valid in e.g. \(\mathbf{Sh}(X)\) for connected \(X\) with nontrivial opens.
Pitfalls¶
- Elementary vs Grothendieck: every Grothendieck topos is elementary; converse fails (need generators / Giraud axioms for sheaf representation).
- Internal equality vs external: two global elements may be internally distinct yet “locally equal.”
- Size: freyd / free toposes and \(\mathbf{Set}\) itself require universe hygiene.
Refs¶
Mac Lane–Moerdijk, Sheaves in Geometry and Logic; Johnstone, Sketches of an Elephant; Borceux Vol. 3; Lawvere–Tierney original notes.
Next¶
Foundations · Category theory · Logic · Algebraic geometry · Homotopy type theory · Classifying & Geometric · Boolean & Forcing · Cohesive & Higher · Synthetic & Infinitesimal