Теория топосов: обобщённые вселенные множеств

Когда Коэн доказал независимость гипотезы континуума (1963) через форсинг - это был, по сути, топос. Когда Гротендик доказал теорему Вейля (1974) - он использовал этальные пучки: топосы. Теория топосов объединила алгебраическую геометрию, логику и теорию типов в одном языке.

• Гротендик: этальные пучки и доказательство гипотез Вейля
• Форсинг Коэна = конструкция топоса булевозначных множеств
• HoTT: типы = пространства = объекты ∞-топоса (Voevodsky)
• Coq, Agda, Lean: пруф-ассистенты на интуиционистской логике топосов

Классификатор подобъектов Ω: истинностные значения категории

Haskell содержит более 250 тысяч пакетов на Hackage - каждый тип является объектом категории Hask, где функции - морфизмы. В категории Set подмножество A ⊆ B задаётся характеристической функцией χ_A: B → {true, false}. **Классификатор подобъектов Ω** - объект, обобщающий {true, false} на произвольную категорию: для каждого подобъекта m: A ↪ B существует единственная стрелка χ_m: B → Ω, делающая квадрат pullback-ом.

**Историческая заметка:** Концепция классификатора подобъектов появилась у Лоувера и Тирни (1969 - 1972) при создании элементарной теории топосов. Ω в пучках соответствует открытым множествам топологического пространства - отсюда связь с алгебраической геометрией Гротендика.

Топос: картезиански замкнутая категория с Ω

**Топос (элементарный)** - категория ε, удовлетворяющая четырём аксиомам: 1. конечные пределы (включая терминальный объект 1) 2. степенные объекты B^A для всех A, B (декартово замкнутость) 3. классификатор подобъектов Ω 4. [иногда добавляют] нётерово условие. Топос - обобщение категории множеств.

**Топос Гротендика vs элементарный топос:** Александр Гротендик (1960-е) определил топос через сайты и пучки для алгебраической геометрии. Лоувер и Тирни (1969) дали аксиоматическое определение через CCC + Ω. Второй подход более общий и охватывает первый как частный случай.

Внутренняя логика топоса: конструктивная математика

Каждый топос имеет **внутреннюю логику**: язык, в котором можно говорить об объектах и морфизмах топоса как о множествах и функциях. Внутренняя логика топоса - интуиционистская (конструктивная): закон исключённого третьего ¬P∨P не всегда выполняется. В топосе Set он выполняется, в Sh(X) - нет.

**Приложения теории топосов:** 1. Алгебраическая геометрия: этальные пучки Гротендика, l-адические когомологии. 2. Синтетическая дифференциальная геометрия (SDG): нильпотентные бесконечно малые без противоречий. 3. Логика: доказательство независимости CH от ZFC через топосы. 4. HoTT: типы = пространства = объекты ∞-топоса.

Ключевые идеи

• Классификатор подобъектов Ω: pullback-универсальная характеристика подобъектов
• Топос = CCC + конечные пределы + Ω: обобщение категории Set
• Примеры: Set, Sh(X), Fun(C°,Set) - каждый задаёт свою «математическую вселенную»
• Внутренняя логика топоса - интуиционистская: нет исключённого третьего в общем случае
• Приложения: алг. геометрия, синтетическая дифгеометрия, HoTT, форсинг

Связанные темы

Теория топосов синтезирует категорную алгебру, геометрию и логику.

• Сопряжённые функторы — CCC = сопряжение (×A) ⊣ (–)^A; кванторы = сопряжения к подстановке
• Пределы и копределы — Конечные пределы - одна из аксиом топоса
• Высшие категории — ∞-топосы = объединение теории топосов и ∞-категорий (HoTT)

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

• Как в топосе Set выглядит классификатор подобъектов Ω? Нарисуйте pullback-квадрат для A = чётные числа ⊆ B = ℕ.
• Почему синтетическая дифференциальная геометрия (SDG) требует топоса, а не обычной теории множеств?
• Как форсинг Коэна связан с топосами? Что такое «модель ZFC через топос»?

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

• ml-08
• ml-11