Topos Theory: Generalized Universes of Sets

When Cohen proved the independence of the continuum hypothesis (1963) via forcing - that was essentially a topos. When Grothendieck proved the Weil conjectures (1974) - he used étale sheaves: toposes. Topos theory unified algebraic geometry, logic, and type theory in one language.

• Grothendieck: étale sheaves and the proof of the Weil conjectures
• Cohen's forcing = construction of the Boolean-valued topos of sets
• HoTT: types = spaces = objects of an ∞-topos (Voevodsky)
• Coq, Agda, Lean: proof assistants on the intuitionistic logic of toposes

The Subobject Classifier Ω: Truth Values of a Category

Haskell has over 250,000 packages on Hackage , each type is an object in the category Hask, with functions as morphisms, and type constructors as functors. In Set, a subset A ⊆ B is given by its characteristic function χ_A: B → {true, false}. The **subobject classifier Ω** generalises {true, false} to an arbitrary category: for every subobject m: A ↪ B there is a unique arrow χ_m: B → Ω making a certain square a pullback.

**Historical note:** The concept of the subobject classifier was introduced by Lawvere and Tierney (1969 - 1972) when they created elementary topos theory. Ω in sheaves corresponds to open sets of a topological space - hence the connection to Grothendieck's algebraic geometry.

A Topos: Cartesian Closed Category with Ω

An **elementary topos** is a category ε satisfying four axioms: 1. finite limits (including a terminal object 1) 2. power objects B^A for all A, B (cartesian closure) 3. a subobject classifier Ω 4. [sometimes added] a natural numbers object. A topos is a generalisation of the category of sets.

**Grothendieck topos vs. elementary topos:** Alexander Grothendieck (1960s) defined toposes via sites and sheaves for algebraic geometry. Lawvere and Tierney (1969) gave the axiomatic definition via CCC + Ω. The second approach is more general and includes the first as a special case.

The Internal Logic of a Topos: Constructive Mathematics

Every topos has an **internal logic**: a language in which one can speak about objects and morphisms of the topos as if they were sets and functions. The internal logic of a topos is intuitionistic (constructive): the law of excluded middle ¬P∨P does not always hold. In Set it holds; in Sh(X) - not in general.

**Applications of topos theory:** 1. Algebraic geometry: Grothendieck's étale sheaves, l-adic cohomology. 2. Synthetic differential geometry (SDG): nilpotent infinitesimals without contradictions. 3. Logic: independence of CH from ZFC via toposes. 4. HoTT: types = spaces = objects of an ∞-topos.

Key Ideas

• Subobject classifier Ω: pullback-universal characterisation of subobjects
• Topos = CCC + finite limits + Ω: generalisation of the category Set
• Examples: Set, Sh(X), Fun(C°,Set) - each gives its own "mathematical universe"
• Internal logic of a topos is intuitionistic: no excluded middle in general
• Applications: algebraic geometry, synthetic differential geometry, HoTT, forcing

Related Topics

Topos theory synthesises categorical algebra, geometry, and logic.

• Adjoint Functors — CCC = adjunction (×A) ⊣ (–)^A; quantifiers = adjoints to substitution
• Limits and Colimits — Finite limits are one of the axioms of a topos
• Higher Categories — ∞-toposes = unification of topos theory and ∞-categories (HoTT)

Вопросы для размышления

• What does the subobject classifier Ω look like in the topos Set? Draw the pullback square for A = even numbers ⊆ B = ℕ.
• Why does synthetic differential geometry (SDG) require a topos rather than ordinary set theory?
• How is Cohen's forcing related to toposes? What is a "model of ZFC via a topos"?

Связанные уроки

• ml-08
• ml-11