Топосы (обзор)

1963 год: Пол Коэн доказывает независимость континуум-гипотезы - она не может быть ни доказана, ни опровергнута в ZFC. Следствие: существуют «параллельные математики» с разными аксиомами. Топосы Гротендика (1960-е) формализуют именно это: каждый топос - полноценная математическая вселенная со своей внутренней логикой, где истина может быть локальным свойством.

• **Доказательство гипотез Вейля**: Делинь (медаль Филдса 1978) использовал l-адические когомологии - конструкцию из теории снопов и топосов - для доказательства глубоких результатов теории чисел
• **Конструктивная математика**: Homotopy Type Theory (HoTT) и Univalent Foundations - программа построения математики в «∞-топосах». Cubical Agda реализует это вычислительно
• **Квантовая механика**: Isham, Döring, Butterfield формулируют квантовую механику через внутреннюю логику топосов - как попытку решить проблему измерения

Предварительные знания

• The Yoneda Lemma

Topos

Топос - это категория, в которой можно делать всю обычную математику, но с другой логикой. Категория Set - топос. Но существуют и другие топосы: категории преснопов, снопы на топологических пространствах, «набры» (sheaves). В каждом топосе своя внутренняя логика. Геометрические топосы (Гротендик) и элементарные (Лоувер-Тирни) - два взгляда на одну идею.

**Элементарный топос** - это категория E с: 1. конечными пределами (в т.ч. терминальный объект 1) 2. экспоненциалами B^A для любых A, B 3. классификатором подобъектов Ω. Эти три свойства достаточны для построения внутренней математики.

Гротендик ввёл топосы геометрически: как «обобщённые топологические пространства». Лоувер и Тирни дали аксиоматическое определение. Оказалось, что это одно и то же: каждый топос Гротендика является элементарным топосом. Это поразительный результат - геометрические и логические интуиции совпадают.

Subobject Classifier

Классификатор подобъектов - сердце топоса. В Set каждое подмножество U ⊆ A задаётся своей характеристической функцией χ_U: A → {0,1}. Классификатор Ω обобщает {0,1}: это специальный объект, такой что подобъекты A «параметризуются» морфизмами A → Ω. В топосах с содержательной логикой Ω может быть больше чем двухточечным.

**Классификатор подобъектов** Ω - это объект с морфизмом true: 1 → Ω, такой что для любого мономорфизма m: U ↪ A существует единственный морфизм χ_m: A → Ω, делающий диаграмму пулбеком: U ↪ A над 1 →^true Ω. Другими словами: Sub(A) ≅ Hom(A, Ω) - подобъекты биективны морфизмам в Ω.

Ключевое открытие: **логика топоса определяется структурой Ω**. В Set Ω = {0,1} - классическая булева логика. В топосе преснопов Ω = Heyting-алгебра - интуиционистская логика (закон исключённого третьего может не выполняться!). В топосе «работающих процессов» - временна́я логика. Топос = математика + логика в едином пакете.

Internal Logic

Каждый топос имеет **внутренний язык** - логику, позволяющую рассуждать «внутри» топоса так, как если бы это было множество. Объекты - типы, морфизмы - функции, Ω - тип булевых значений. Формулы - морфизмы в Ω. Но логика может быть интуиционистской, временно́й, модальной - в зависимости от топоса.

**Внутренний язык** (Mitchell-Bénabou language) топоса E позволяет писать формулы вида {x ∈ A | φ(x)}, ∀x:A.ψ(x), ∃x:A.ψ(x), и интерпретировать их как объекты и морфизмы в E. Верность формулы в топосе = существование морфизма 1 → Ω, задающего «истину» для этой формулы.

**Соответствие Карри-Говарда-Ламбека**: типы ↔ объекты топоса, термы ↔ морфизмы, формулы ↔ подобъекты (морфизмы в Ω), доказательства ↔ элементы типа (морфизмы из 1). Это трёхстороннее соответствие между логикой, теорией типов и теорией категорий - одно из глубочайших открытий математики XX века.

Sheaves

**Снопы** (sheaves) - это преснопы, удовлетворяющие условию «склейки». Интуиция: пресноп задаёт «локальные данные» на каждом открытом U. Сноп добавляет: если на перекрывающихся U и V данные согласованы (совпадают на U ∩ V), то существует единственная «склейка» на U ∪ V. Это глобально-локальный принцип.

**Сноп** F на топологическом пространстве X - это пресноп F: Open(X)^{op} → Set, удовлетворяющий аксиомам: 1. локальность: если две секции s, t ∈ F(U) совпадают на каждом элементе покрытия {Uᵢ}, то s = t 2. склейка: если {sᵢ ∈ F(Uᵢ)} согласованы (sᵢ|_{Uᵢ∩Uⱼ} = sⱼ|_{Uᵢ∩Uⱼ}), то существует s ∈ F(U) с s|_{Uᵢ} = sᵢ.

**Топосы и логика**: категория Sh(X) снопов на топологическом пространстве X - топос. Логика этого топоса - **пространственная интуиционистская логика**. Истинность формулы «в точке x» зависит от окрестности x, а не от всего пространства. Это соответствует «параметрической истинности» - утверждение может быть истинным «локально».

**Топосы как обобщённые вселенные**: каждый топос - это самодостаточная математическая вселенная. В нём есть свои множества, своя логика, своя арифметика (через объект натуральных чисел). Один топос может моделировать математику, где действует принцип исключённого третьего; другой - конструктивную математику; третий - математику с параметрами (пространством).

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

• **Топос** - категория с конечными пределами, экспоненциалами и классификатором подобъектов Ω; обобщает Set как математическую вселенную
• **Классификатор Ω** - объект, параметризующий подобъекты; в Set = {True, False}; в других топосах может быть больше, определяя содержательную логику
• **Внутренняя логика** - соответствие Карри-Говарда-Ламбека: типы=объекты, доказательства=морфизмы 1→A, формулы=подобъекты; логика = интуиционистская в общем случае
• **Снопы** Sh(X) - топос на топол. пространстве X; аксиомы склейки обеспечивают «глобально-локальный» принцип; основа алгебраической геометрии

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

Топосы объединяют большинство продвинутых концепций теории категорий:

• Лемма Ёнеды — Вложение Ёнеды C ↪ Set^{C^{op}} - это вложение в топос преснопов. Топос преснопов - «завершение» C до топоса
• Category Theory в CS — Внутренняя логика топоса = тип-теоретический язык программирования. HoTT, Cubical Agda - топосные языки

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

• Закон исключённого третьего (P ∨ ¬P) не выполняется во внутренней логике произвольного топоса. Придумайте конкретный пример (предикат P и топос), где P ∨ ¬P не является глобальной истиной.
• Соответствие Карри-Говарда-Ламбека: тип `(A × B) → C ≅ A → (B → C)` (curry). Что соответствует этому изоморфизму в логике и теории категорий?
• Сноп непрерывных функций на S¹. Существует ли глобальная непрерывная функция f: S¹ → ℝ без нулей? Как это связано с классификатором Ω снопа?

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

• ml-08
• ml-11