∞-категории: морфизмы между морфизмами

Программисты работают с типами каждый день. Математики - с пространствами. HoTT говорит: это одно и то же! данная функция f: A → B - это непрерывное отображение топологических пространств. Ошибки типизации = разрывы непрерывности. ∞-категории - это язык, в котором это утверждение точно.

• HoTT и унивалентность: новое фундирование математики (Воеводский, IAS)
• Cubical Agda: реализация кубического HoTT для формальной математики
• Производная алгебраическая геометрия: ∞-стеки и спектральные схемы (Лурие)
• Теория струн: ∞-категории кобордизмов и TQFT

2-категории: морфизмы между морфизмами

Программа HoTT (Homotopy Type Theory, 2013, Институт перспективных исследований Принстон) формализует 2-категории через Coq: 50 000+ строк формальных доказательств. **2-категория** содержит три уровня: объекты (0-клетки), морфизмы (1-клетки) и **2-морфизмы** между морфизмами (2-клетки). Классический пример: Cat (категория малых категорий), где объекты = категории, морфизмы = функторы, 2-морфизмы = естественные преобразования.

**Физика струн и 2-категории:** В теории конформных полей (CFT) и теории струн появляются 2-категории естественным образом. Категория Кобордизмов (Bord_2) - 2-категория, где объекты = 0-многообразия, 1-клетки = 1-многообразия (кобордизмы), 2-клетки = 2-многообразия (диффеоморфизмы кобордизмов).

n-Категории и ∞-категории

**n-категория** добавляет k-морфизмы для каждого k от 0 до n. **∞-категория (ω-категория)** имеет k-морфизмы для всех k ≥ 0. Строгие ∞-категории определить просто, но они слишком ограничены. **Слабые ∞-категории** (∞-категории Жур ана - Тьерни, квазикатегории Джойала) - правильная концепция, где равенства заменяются когерентными гомотопиями.

**Производные алгебраической геометрии:** Жакоб Лурие в «Higher Topos Theory» (2009) и «Spectral Algebraic Geometry» формализовал ∞-категории через квазикатегории. Это открыло эру производной алгебраической геометрии: схемы заменяются ∞-стеками, а когомологии - спектральными последовательностями в ∞-категориях.

∞-Группоиды, HoTT и гипотеза Гротендика

**∞-Группоид** - ∞-категория, в которой каждый k-морфизм обратим. **Гипотеза Гротендика** (доказана): гомотопические типы топологических пространств взаимно однозначно соответствуют ∞-группоидам. **Теория гомотопических типов (HoTT)** Воеводского делает это основой математики: типы = пространства = ∞-группоиды.

**Владимир Воеводский и унивалентность:** Владимир Воеводский (Fields Medal 2002, IAS Princeton) разработал Теорию Гомотопических Типов (HoTT) как новое фундирование математики. Он был убеждён, что обычная математика содержит неисправленные ошибки, и HoTT + пруф-ассистенты - единственный способ получить полностью проверенные доказательства. Проект UniMath продолжает его работу.

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

• 2-категории: объекты, морфизмы, 2-морфизмы (нат. преобразования в Cat)
• ∞-категории: бесконечная иерархия k-морфизмов; слабые ≠ строгие при n≥3
• ∞-группоид = ∞-категория с обратимыми морфизмами; гипотеза Гротендика доказана
• HoTT: тип = пространство = ∞-группоид; принцип унивалентности
• Производная алгебраическая геометрия: ∞-топосы, спектральные схемы (Лурие)

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

∞-категории синтезируют всю теорию категорий на высшем уровне.

• Теория топосов — ∞-топосы = обобщение топосов Гротендика на ∞-категории
• Когомологии — Производные категории - 1-категориальное приближение ∞-категорий; ∞-топосы дают полную теорию
• Монады — Монады в ∞-категориях = монадичность Барра–Бека в ∞-контексте

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

• Почему тип пути (a =_A b) в HoTT является более богатой структурой, чем простое булевое равенство?
• Как гипотеза Гротендика связывает алгебраическую топологию (гомотопические типы) с теорией категорий (∞-группоиды)?
• Что значит «производная алгебраическая геометрия» - в чём принципиальное улучшение по сравнению с классической алгебраической геометрией?

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

• ml-16
• aa-26-derived-categories