Пример из практики: что нужно, чтобы сформулировать и доказать аргумент Квиллена о малых объектах в ZFC?
Я немного запутался в интересном вопросе Питера Шольце об устранении зависимости от вселенных из теорем теории категорий. В частности, я вынужден признать, что на самом деле я не знаю, когда вызывается замена, не говоря уже о том, когда она вызывается «по существу». Итак, я хотел бы проработать достаточно конкретный пример этого явления. Я понимаю, что замену «действительно» следует рассматривать как аксиому, допускающую трансфинитную рекурсию. Я считаю, что теория категорий не склонна использовать рекурсию в чрезмерных количествах (хотя, в большей степени, чем другие разделы математики, в ней есть множество определений, которые, по крайней мере, на первый взгляд, имеют нетривиальную сложность Леви. Например, я думаю, что формула$\phi(x,y,z,p,q)$ говоря, что набор $z$ и функции $p: z \to x$ а также $q: z \to y$ являются категориальным произведением множеств $x,y$ синтаксически $\Pi_1$, а утверждение, что бинарные продукты существуют в категории наборов, синтаксически $\Pi_3$ (конечно, игнорируя ограниченные кванторы)).
Следующая теорема, я думаю, является одним из заметных исключений из теоретико-категориальной неприменения рекурсии:
Теорема [Квиллен] "Аргумент малого объекта": Пусть$\mathcal C$ - местная презентабельная категория, и пусть $I \subseteq Mor \mathcal C$- небольшой набор морфизмов. Позволять$\mathcal L \subseteq Mor \mathcal C$ быть классом ретрактов трансфинитных композитов кобазо-замен копродуктов морфизмов в $I$, и разреши $\mathcal R \subseteq Mor \mathcal C$ составляют те морфизмы, слабо ортогональные вправо к морфсимам $I$. потом$(\mathcal L, \mathcal R)$является слабой системой факторизации на$\mathcal C$.
Для доказательства см. Nlab . В основном факторизации строятся трансфинитной рекурсией. Рекурсия кажется мне «необходимой», потому что новые данные вводятся на каждом этапе построения.
Формализация:
Я думаю, что эту теорему и ее доказательство можно прямо формализовать в МК, где теоретико-категориальное различие «малое / большое» интерпретируется как различие МК «множество / класс». Я не считаю себя вправе комментировать, работает ли доказательство в NBG, но утверждение, по крайней мере, имеет прямой смысл.
Когда дело доходит до формализации в ZFC, у нас есть выбор относительно различий между малым и большим:
Один из вариантов - ввести «вселенную» $V_\kappa$(который, если мы действительно пытаемся работать в ZFC, будет более слабой вселенной, чем обычно). Мы будем интерпретировать "маленький" как "в"$V_\kappa$". Мы не будем рассматривать" действительно большие объекты "- все, о чем мы говорим, будет набором - в частности, каждая категория, о которой мы говорим, будет иметь размер набора, даже если не" маленькие "как таковые. интерпретировать "местную презентабельную категорию" как "$\kappa$-полный, локально $\kappa$-маленькая категория с сильным $\kappa$-небольшой, $\lambda$-представленный генератор на какой-то штатный $\lambda < \kappa$"(Я не знаю, имеет ли смысл говорить это $V_\kappa$ думает $\lambda$ - обычный кардинал).
Другой вариант - не вводить какую-либо вселенную, а просто интерпретировать «маленький» как «размер множества». В этом случае любой «большой» объект, о котором мы говорим, должен определяться по малым параметрам. Итак, мы определяем категорию, которая включает в себя определяемый параметром класс объектов, определяемый параметром класс морфизмов и т. Д. Это может показаться ограничительным, но это будет хорошо работать в локально представимом случае, поскольку мы можем определить локально представимую категорию.$\mathcal C$ подлежит определению относительно параметров $(\lambda, \mathcal C_\lambda)$ (где $\lambda$ обычный кардинал и $\mathcal C_\lambda$ маленький $\lambda$-полная категория), как категория $\lambda$-Индовать объекты в $\mathcal C_\lambda$.
Теперь, применительно к рассматриваемой теореме, подход (2) кажется более чистым, поскольку необходимая «трансляция» проста, и как только она будет выполнена, исходное доказательство должно работать без изменений. Я думаю, что основные недостатки (2) заключаются в другом. Например, формулировка теорем о категории локально представимых категорий, вероятно, будет деликатным делом. В общем, будут различные теоремы о категориях, которые имеют чистые, концептуальные формулировки и доказательства, когда задействованные категории малы, но которые требуют раздражающих технических модификаций, когда задействованные категории большие. Именно по этим причинам подходы типа (1), как правило, предпочтительнее для крупномасштабных теоретико-категорийных проектов.
Итак, предположим, что мы следуем подходу (1). Тогда возникает вопрос:
Вопрос 1. Какая именно вселенная нам нужна, чтобы сформулировать и доказать вышеприведенную теорему, следуя подходу (1)?
Вопрос 2: Сколько таких вселенных гарантированно существует ZFC?
Предположительно, ответ на вопрос 2 будет заключаться в том, что таких вселенных очень много - достаточно, чтобы мы могли делать такие вещи, как, учитывая категорию, переходить во вселенную, достаточно большую, чтобы сделать эту категорию маленькой, и применять теорему для этой вселенной. .
Вопрос 3: Как далеко мы должны зайти в сорняки, чтобы ответить на вопросы 1 и 2?
Нужно ли нам глубоко анализировать доказательство теоремы? Есть ли простая рубрика критериев, которая позволяет нам взглянуть на доказательство и для 99% подобных теорем легко сказать, что оно «проходит», не вдаваясь в подробности? Или есть хоть какая-то формальная метатеорема, к которой мы можем обратиться, чтобы даже компьютер мог проверить, что все в порядке?
Ответы
Комментарий Якоба Лурье дает ответ на вопрос 1. А именно, предполагая, что оценки, которые я дал в своем комментарии , верны, для формулировки и доказательства теоремы достаточно предположить, что
- $\kappa$ регулярно
и это
- для каждого $\mu < \kappa$, Существует $\rho < \kappa$ такой, что $\mu \ll \rho$ (означающий, что $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Возможно это свойство $\kappa$можно рассматривать как «форму» замены. Но на самом деле у нас есть два условия на$\kappa$ которые являются чисто теоретико-множественными, а не метаматематическими, так что ответ на вопрос 1 гораздо более ясен, чем я предполагал.
Это позволяет нам ответить на вопрос 2. Предположительно, результат таков, что ZFC доказывает, что существует много-много $\kappa$ удовлетворяющий двум вышеуказанным условиям.
Когда дело доходит до вопроса 3, может показаться, что при таком подходе нам действительно нужно довольно глубоко вникнуть в доказательство. Фактически, кажется, что для того, чтобы реализовать этот подход, мы должны добавить некоторое истинное математическое содержание к доказательству и фактически доказать более сильное утверждение. Дальнейшие вопросы становятся
Будет ли вообще возможно «конструктивизировать» «большинство» теоретико-категорийных теорем таким образом, или в ходе проекта «Теория категорий ZFC-ify» обнаружатся другие проблемы?
Если ответ на (1) - «да» (или если это обычно «нет», и мы ограничиваем наше внимание случаями, когда это «да»), то «сколько дополнительной работы» было бы в действительности для такого проекта?
Я предполагаю, что ответ на (1) заключается в том, что, когда дело доходит до использования трансфинитной рекурсии в теории категорий, действительно обычно бывает так, что использование замены может быть исключено аналогичным образом, но это более важно. что важно, я упустил суть: как утверждает Джейкоб Лурье в ответ на вопрос Питера Шольце, самые острые проблемы с теорией категорий ZFC связаны не с трансфинитной рекурсией, а с возможностью свободно перемещаться между «большими категориями». "и" маленькие категории "по-разному.
Я предполагаю, что ответ на (2) состоит в том, что для "большинства" теоретико-категориальных применений трансфинитной рекурсии на самом деле должно быть довольно просто "конструктивизировать" их так, чтобы они вписывались в "детскую вселенную" со свойствами выше или что-то подобное, и это с небольшой практикой, можно развить способность почти с первого взгляда проверить, что это возможно, хотя все еще на основе теоремы за теоремой. Но я бы хотел, чтобы меня доказали, что он неправ, и я бы показал теорему теории категорий, в которой такой подход не работает!
Наконец, остается открытым вопрос, существует ли «более автоматический» способ сделать все это - возможно, с более слабым выводом, чем «наша Вселенная вообще не нуждается в какой-либо форме замены».