Принцип отражения против вселенных
В теоретико-категориальных дискуссиях часто возникает соблазн взглянуть на категорию всех абелевых групп или всех категорий и т. Д., Что быстро приводит к обычным теоретико-множественным проблемам. Их часто избегают, используя вселенные Гротендика. На теоретико-множественном языке фиксируется сильно недоступный кардинальный$\kappa$ -- это значит, что $\kappa$ какой-то несчетный кардинал такой, что для всех $\lambda<\kappa$, также $2^\lambda<\kappa$, и для любого набора $<\kappa$ много наборов $S_i$ размера $<\kappa$, также их объединение имеет размер $<\kappa$. Это означает, что этап$V_\kappa\subset V$ "наборов размеров $<\kappa$"сам по себе является моделью ZFC - применив любую из операций над наборами, например, взяв наборы мощности или союзы, вы никогда не сможете покинуть $V_\kappa$. Эти множества тогда называются «малыми», и тогда категория малых абелевых групп определенно корректно определена.
Исторически этот подход был впервые использован Гротендиком; более поздний основополагающий текст - это работа Лурье над$\infty$-категории. Однако их использование всегда вызывало некоторую обратную реакцию, поскольку некоторые люди не хотели позволять аксиомам, выходящим за рамки ZFC, ускользать в устоявшейся литературе. Например, я думаю, что в какой-то момент велась долгая дискуссия о том, была ли доказана Великая теорема Ферма в ZFC, теперь решенная Макларти. Совсем недавно я видел похожие аргументы в пользу теорем, доказательства которых относятся к работе Лурье. (Лично я не испытываю сильных эмоций по этому поводу и все равно понимаю аргументы.)
С другой стороны, также всегда было так, что более тщательное изучение обнаруживало, что любое использование вселенных на самом деле было ненужным. Например, проект Stacks не использует юниверсы. Вместо этого (см. Тег 000H ) он эффективно ослабляет гипотезу о том, что$\kappa$ сильно недоступен, к чему-то вроде сильного предельного кардинала несчетной конфинальности, то есть: для всех $\lambda<\kappa$, надо $2^\lambda<\kappa$, и всякий раз, когда у вас есть счетная коллекция наборов$S_i$ размера $<\kappa$, а также объединение $S_i$ имеет размер $<\kappa$. ZFC легко доказывает существование таких$\kappa$, и почти каждый аргумент, который можно себе представить в категории абелевых групп, на самом деле также работает в категории $\kappa$-малые абелевы группы для таких $\kappa$. Если делать более сложные рассуждения, можно соответственно усилить исходную гипотезу о$\kappa$. Мне довелось сам играть в эту игру, результат см. В разделе 4 на сайте www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf . Исходя из этого опыта, я почти уверен, что можно аналогичным образом переписать «Теорию высших топосов» Лурье или любую другую аналогичную теоретико-категориальную работу таким образом, чтобы удалить всех строго недоступных кардиналов, заменив их тщательно подобранными$\kappa$ с такими свойствами, как указанные выше.
Фактически, похоже, существует теорема ZFC, принцип отражения (который кратко обсуждается, например, в Tag 000F проекта Stacks), который, кажется, гарантирует, что это всегда возможно. А именно, для любого данного конечного набора формул теории множеств существует достаточно большой$\kappa$ такие, что, грубо говоря, эти формулы справедливы в $V_\kappa$ если и только если они держатся $V$. Похоже, это говорит о том, что для любого заданного конечного набора формул можно найти некоторые$\kappa$ такой, что $V_\kappa$ведет себя как вселенная по отношению к этим формулам, но, пожалуйста, поправьте меня в моем очень наивном понимании принципа отражения! (С этим связан тот факт, что ZFC доказывает непротиворечивость любого заданного конечного фрагмента аксиом ZFC.)
С другой стороны, любой данный математический текст содержит только конечное число формул (если только в нем не указана «схема теоремы», что, как мне кажется, обычно не происходит). Таким образом, вопрос сформулирован несколько провокационно:
Подразумевает ли принцип отражения, что должна быть возможность переписать теорию высших топосов таким образом, чтобы избежать использования вселенных?
Изменить (28.01.2021): Большое спасибо за все очень полезные ответы! Я думаю, что теперь у меня гораздо более четкое представление о ситуации, но я все еще не совсем уверен, каков ответ на вопрос.
Насколько я понимаю, (примерно) лучшая мета-теорема в этом направлении - это следующая (специализированная для HTT). Напомним, что HTT исправляет двух сильно недоступных кардиналов.$\kappa_0$ а также $\kappa_1$, освобождая место для небольших (в $V_{\kappa_0}$), большой (в $V_{\kappa_1}$), и очень большие (в $V$) объекты. Затем можно попытаться прочитать HTT в следующей системе аксиом (по сути, это одна из статей Фефермана «Теоретико-множественные основы теории категорий», которая также была предложена в ответе Родриго Фрейре ниже).
(i) Обычные аксиомы ZFC
(ii) Два других символа $\kappa_0$ а также $\kappa_1$, с аксиомами, что они кардиналы, что конфинальность $\kappa_0$ несчетное количество, и что cofinality $\kappa_1$ больше чем $\kappa_0$.
(iii) Схема аксиом, гласящая, что для каждой формулы $\phi$ теории множеств, $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ а также $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
Затем можно использовать принцип отражения, чтобы показать (см. Ответ Родриго Фрейре ниже для наброска доказательства):
Теорема. Эта система аксиом консервативна по отношению к ZFC. Другими словами, любая теорема в этой формальной системе, не относящаяся к$\kappa_0$ а также $\kappa_1$ также является теоремой ZFC.
Именно к такому выводу я хотел бы прийти.
Обратите внимание, что $V_{\kappa_0}$ а также $V_{\kappa_1}$ являются моделями ZFC, но (критически!) это не может быть доказано внутри формальной системы, поскольку ZFC не является конечно аксиоматизируемым, и только каждая отдельная аксиома ZFC постулируется согласно (iii).
Одна хорошая вещь в этой системе аксиом состоит в том, что она явно допускает случайные аргументы вида «мы доказали эту теорему для малых категорий, но затем мы можем применить ее и к большим категориям».
Тогда возникает более точный вопрос:
Работают ли аргументы HTT в этой формальной системе?
Майк Шульман в Разделе 11 https://arxiv.org/abs/0810.1279дает очень четкое описание возможных проблем. А именно, если у вас есть набор$I\in V_{\kappa_0}$ и устанавливает $S_i\in V_{\kappa_0}$ для $i\in I$, вы не можете заключить, что объединение $S_i$ в $V_{\kappa_0}$. Этот вывод гарантирован только в том случае, если функция$i\mapsto S_i$ также определено в $V_{\kappa_0}$ (или если $I$счетна в силу дополнительного предположения о несчетной конфинальности). На практике это означает, что когда кто-то хочет утверждать, что что-то «маленькое» (т.е.$V_{\kappa_0}$), это суждение относится не только к объектам, но также и к морфизмам и т. д. Мне сейчас не ясно, насколько это действительно проблема, мне нужно было бы больше подумать об этом; На самом деле я могу представить, что читать HTT довольно легко, чтобы соответствовать этой формальной системе. Шульман говорит, что с этим предостережением можно доказать теорему о присоединенном функторе, и, как говорит Лурье в своих ответах, аргументы в HTT имеют аналогичную теоретико-множественную сложность. Тем не менее, меня все еще интересовало бы суждение о том, будет ли ответ на вопрос «Да, как написано» или, скорее, «Возможно, да, но вам нужно приложить некоторые усилия», или фактически «Не совсем». (Я искренне надеюсь, что эксперты сумеют примерно договориться о том, где находится ответ в этом спектре.)
Последнее замечание: предположение о "несчетности" выше может показаться несколько произвольным; почему бы не разрешить несколько более крупных союзов? Один из способов решить эту проблему - добавить символ$\kappa_{-1}$ с теми же свойствами, и вместо этого спросите, что cofinality $\kappa_0$ больше чем $\kappa_{-1}$. Точно так же можно заменить границу$\mathrm{cf} \kappa_1>\kappa_0$ чуть более сильной связью вроде $\mathrm{cf} \kappa_1>2^{\kappa_0}$сказать. Опять же, если это упростит ситуацию, тогда можно было бы просто сжать другую$\kappa_{1/2}$ между ними, так что $\mathrm{cf} \kappa_{1/2}>\kappa_0$ а также $\mathrm{cf} \kappa_1>\kappa_{1/2}$. Таким образом, не нужно беспокоиться о том, останутся ли какие-либо из «стандартных» объектов, которые появляются в некоторых доказательствах, счетного размера, или все еще можно брать копределы в$V_{\kappa_1}$ когда наборы индексов точно не имеют размера, ограниченного $\kappa_0$ но были немного изменены.
PS: Я только сейчас нахожу все соответствующие предыдущие вопросы и ответы МО. Некоторые очень важные из них - это ответы Джоэла Хэмкинса здесь и здесь .
Ответы
Я собираюсь рискнуть и предположить, что книга HTT никогда не использует ничего более сильного, чем замена для $\Sigma_{15}$-формулы теории множеств. (Здесь$15$ - произвольно выбранное большое число, а HTT - случайно выбранная книга по математике, которая конкретно не посвящена теории множеств.)
Размышляя над комментарием Гейба к моему первоначальному ответу, я теперь думаю, что то, что я написал, вводит в заблуждение, потому что оно объединяет два отдельных (но связанных) утверждения:
Существование сильно недоступных кардиналов на самом деле не требуется в теории категорий.
Вся мощь ZFC не нужна в теории категорий.
Я согласен с обоими этими утверждениями, но думаю, что лучший способ убедить кого-то в 1) не будет сочетать 2) с принципом отражения: то есть не следует пытаться заменить использование сильно недоступного кардинала $\kappa$ по одному, для которого $V_{\kappa}$ моделирует большую часть ZFC.
На мой взгляд, «проблема», которую решают вселенные, состоит в том, чтобы оправдать комбинацию двух типов рассуждений:
А) Иногда бывает полезно доказать теоремы о малых категориях. $\mathcal{C}$ путем встраивания их в «большие» категории (например, с помощью встраивания Yoneda), которые имеют приятные дополнительные функции: например, наличие ограничений и копределов.
Б) Большие категории также являются категориями, поэтому любая теорема, относящаяся к категориям в целом, должна также применяться к большим категориям.
Если бы вы беспокоились только о B), тогда может быть актуален принцип отражения. Выбор кардинала$\kappa$ такой, что $V_{\kappa}$ удовлетворяет большую часть ZFC, вы можете переопределить «небольшую категорию», чтобы обозначить «категорию, принадлежащую к $V_{\kappa}$"и" большая категория "означает" категория, не обязательно принадлежащая $V_{\kappa}$", и вы можете быть уверены, что все основные теоремы, которые вам могут понадобиться, верны в обоих случаях.
Но если вас беспокоит еще и пункт A), это не обязательно поможет. Скажем, вы начинаете с категории$\mathcal{C}$ принадлежащий $V_{\kappa}$, и вам нужна какая-то версия вложения Йонеды. Естественным предположением было бы вложить в категорию функторов из$\mathcal{C}^{\mathrm{op}}$ в категорию наборов размеров $<\tau$ (или его эквивалентную модель), для некоторого кардинального $\tau$. Первое предположение - вам следует взять$\tau = \kappa$, но я думаю, что это имеет смысл $\kappa$сильно недоступен (иначе некоторые множества Hom будут слишком большими). В любом случае гарантируйте, что эта конструкция имеет хорошие свойства, вам захочется потребовать разные свойства кардинала.$\tau$. Например, если вы хотите, чтобы у этой категории предварительных пучков было много копределов, тогда вам понадобится$\tau$иметь большую кофинальность. И если вы начнете думать о том, какие дополнительные предположения вам могут потребоваться, вы вернетесь туда, откуда начали: подумайте о том, какие оценки мощности гарантируют, что «предварительные пучки наборов размера$< \tau$"являются хорошим приближением к категории всех предпучков множеств. Таким образом, принцип отражения не помогает избежать этих проблем.
(Изменить: после написания я понял, что текст ниже в основном повторяет исходный пост Питера. Но я оставлю его здесь на случай, если кто-то сочтет его полезным.)
Если вам нужна строгая формализация в чем-то вроде ZFC, вероятно, лучше всего вообще отказаться от больших категорий. Значит, B) не проблема. Чтобы разобраться с A), позвольте мне заметить, что многие из «больших» категорий, о которых хотелось бы поговорить, возникают особым образом: каждый начинается с небольшой категории.$\mathcal{C}$ который уже имеет определенные виды копределов и формально увеличивает $\mathcal{C}$ сделать категорию побольше $\mathcal{C}^{+}$который имеет произвольные копределы (без изменения тех, с которых вы начали). Категории, которые возникают таким образом, называются локально презентабельными , и есть простая формула для$\mathcal{C}^{+}$: это категория функторов $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ которые сохраняют пределы, с которых вы начали (то есть копределы, с которых вы начали в $\mathcal{C}$).
Теперь, если вы хотите имитировать это в мире небольших категорий, вы можете вместо этого выбрать какой-нибудь кардинальный $\kappa$ и вместо этого рассмотрим функторы $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\каппа$} \}$, что эквивалентно небольшой категории $\mathcal{C}^{+}_{\kappa}$. Вы задаетесь вопросом, достаточно ли это хорошая замена для большой категории?$\mathcal{C}^{+}$выше. Например, есть ли у него много ограничений и коллимитов? Неразумно просить, чтобы у него были все копределы, но вместо этого вы можете спросить следующее:
Q) Категория $\mathcal{C}^{+}_{\kappa}$ иметь копределы, проиндексированные диаграммами размеров $< \kappa$?
Ответ на вопрос: «в целом нет, но да, если $\kappa$ красиво выбрано ". Например, если у вас есть бесконечный кардинал $\lambda$ ограничивая размер $\mathcal{C}$ и количество диаграмм копределов, с которых вы начинаете, тогда я считаю, что вы можете гарантировать (i), взяв $\kappa = (2^{\lambda})^{+}$ (и категория $\mathcal{C}^{+}_{\kappa}$можно охарактеризовать ожидаемым универсальным свойством). Более того, чтобы доказать это, вам не потребуется никакая замена.
Теперь вы также можете спросить следующее:
Q ') Категория $\mathcal{C}^{+}_{\kappa}$ иметь пределы, обозначенные диаграммами размеров $< \kappa$?
Здесь обычно ответ будет «нет», если только $\kappa$сильно недоступен. Но если вас интересуют только пределы определенного типа (например, если вы изучаете топои Гротендика, вас могут особенно интересовать конечные пределы), то ответ снова будет «да для$\kappa$ хорошо выбран ». И это то, что вы можете доказать, используя очень мало ZFC.
Я утверждаю, что, основываясь на моем опыте, приведенное выше обсуждение является репрезентативным для вопросов, с которыми вы столкнетесь, пытаясь сориентироваться в различии между «маленькими» и «большими» категориями (безусловно, это типичное представление того, в моей книге, о которой был задан первоначальный вопрос). На практике вам никогда не придется говорить о большой категории в целом, например о$\mathcal{C}^{+}$; достаточно, чтобы построить из него достаточно большой кусок (например,$\mathcal{C}^{+}_{\kappa}$) с функциями, которые вы хотите видеть, которые вы можете упорядочить, выбрав $\kappa$ осторожно.
Я считаю, что концептуально более ясно игнорировать вопрос о том, как вещи формализованы в ZFC, и формулировать вещи в терминах «большой» категории. $\mathcal{C}^{+}$, возвращаясь к его "маленьким" приближениям $\mathcal{C}^{+}_{\kappa}$только в качестве вспомогательных средств в доказательстве (которое неизбежно все равно где-нибудь появится!). Вызов «вселенных» - это просто способ написать так, но при этом на словах придерживаться аксиоматической структуры ZFC, и это определенно несущественно.
Я хотел бы упомянуть кое-что, на что я еще не обращал внимания. Первоначальный вопрос начинался с
На теоретико-множественном языке фиксируется сильно недоступный кардинальный $\kappa$... Это означает, что этап $𝑉_\kappa\subset 𝑉$ "наборов размеров $<\kappa$"Сама по себе модель ZFC.
Однако утверждение, что $V_\kappa$ модель ZFC значительно слабее, чем сказать, что $\kappa$недоступен. Фактически, если$\kappa$ недоступен, то $\{ \lambda\mid V_\lambda$ это модель ZFC $\}$ неподвижен в $\kappa$. Следовательно, самый маленький недоступный (если он есть) намного больше самого маленького.$\kappa$ такой, что $V_\kappa$ модели ZFC.
Поскольку принцип отражения полезен (что, как указывали некоторые другие ответы, можно, по крайней мере, задавать вопросом), он напрямую полезен только для аргументов, в которых соответствующее свойство вселенной Гротендика состоит в том, что это модель ZFC. Однако, по крайней мере, в наивной формулировке, есть много мест, где теория категорий использует нечто большее. В частности, мы используем тот факт, что вселенная Гротендика удовлетворяет замене второго порядка , что означает, что любая функция$f:A\to V_\kappa$, где $A \in V_\kappa$, есть изображение. Говоря это$V_\kappa$модели ZFC только подразумевает, что он удовлетворяет замене первого порядка , что позволяет нам только заключить, что такая$f$ есть изображение, если $f$ определяется из $V_\kappa$ по логической формуле.
Я считаю, что замена второго порядка повсеместна в теории категорий, основанной на вселенной, как это обычно формулируется. Например, если${\rm Set}_\kappa$ обозначает категорию множеств в $V_\kappa$, а затем доказать, что ${\rm Set}_\kappa$ является «полным и соколным» в том наивном смысле, что он допускает предел и копредел для любого функтора, область определения которого мала, нам нужна замена второго порядка, чтобы собрать образы такого функтора в единый набор.
Теперь есть способы переформулировать теорию категорий, чтобы избежать этого. В статье Макларти это делается некоторыми теоретико-множественными способами. Категорически последовательный подход заключается в замене наивных «больших категорий» (то есть категорий, наборы объектов и морфизмов которых могут не принадлежать$V_\kappa$) с большим ${\rm Set}_\kappa$- проиндексированные категории . Но это гораздо более существенный вид переформулирования, выполняемый вручную.
Если я правильно понял, вам нужно заявление в форме:
"Если что-то было доказано в HTT с использованием вселенных, это можно доказать и без них, ограничившись некоторыми $V_\kappa$ для $\kappa$ достаточно большой"
Если у нас нет дополнительной информации о HTT, строгий ответ на этот вопрос заключается в том, что такого утверждения быть не может, если ZFC согласован.
В самом деле, возможно, что существование вселенных несовместимо (на самом деле невозможно доказать, что оно непротиворечиво), и в этой ситуации с помощью вселенных можно доказать что угодно, и поэтому такое утверждение будет означать, что все можно доказать. , т.е. ZFC несовместим.
Я немного небрежно отношусь к тому, что можно доказать, в чем и т. Д., Но основная идея здесь
Конечно, мы кое-что знаем о HTT, и если мы внимательно его прочитаем, мы сможем проанализировать, где он использует вселенные, и увидеть, что они фактически могут быть заменены транзитивными моделями замены ZC + вплоть до $\Sigma_{15}$-формулы, как указывает Джейкоб. В этом случае, поскольку существуют такие модели с хорошим поведением (вида$V_\kappa$, для $\kappa$удачно подобранный), это не проблема; и HTT можно переписать без юниверсов - но это не может быть доказано без знания того, что находится в HTT.
«Мораль» этого состоит в том, что в большинстве теоретических вопросов основной категории вселенные - это средство экономии времени, а не фактическая часть математики.
Любая теорема $T$ из $\mathsf{ZFC}$ следует из конечного подмножества аксиом $\mathsf{ZFC}$ или, чтобы не усложнять, от $\mathsf{ZFC}$ где аксиомная схема замены ограничена $\Sigma_n$ предикаты¹, назовите это $\mathsf{ZFC}_n$. Сейчас$\mathsf{ZFC}$, а точнее $\mathsf{ZFC}_{n+1}$, доказывает существование сколь угодно больших кардиналов $\kappa$, сильные пределы несчетной конфинальности, такие что $V_\kappa$ это модель $\mathsf{ZFC}_n$, и, в частности, теоремы $T$, и такие, что, кроме того, истинное значение любого $\Sigma_n$ заявление, с параметрами в $V_\kappa$ то же самое в $V_\kappa$как в (истинной) вселенной. Мы можем назвать это$V_\kappa$ «Ограниченные вселенные» в том смысле, что они закрываются при большинстве теоретико-множественных операций, таких как взятие наборов степеней, за исключением того, что замена должна быть либо счетной (включена для удобства), либо ограничена $\Sigma_n$предикат; и, в частности, они закрываются при любых заявлениях о существовании$T$ делает.
Идея состоит в том, чтобы применить вышеизложенное к соединению $T$ всех теорем, которые вы считаете частью теории высших топосов (и любых других теорий, используемых в качестве предварительных условий), и найдите подходящую $n$. (Я действительно подозреваю, что$n=1$ должно быть достаточно: я был бы очень удивлен, если бы нашел в обычной математике пример замены, который не следует из $\Sigma_1$-замена.) Тогда $\mathsf{ZFC}_n$ докажет $T$ (все теоремы теории) и $\mathsf{ZFC}_{n+1}$ докажет существование бесконечного количества ограниченных вселенных, в которых можно использовать эту теорию.
Конечно, чтобы избежать бесконечного цикла, вы не можете рассматривать эту теорему (утверждающую существование бесконечного запаса$V_\kappa$), чтобы быть частью теории, или вам нужно перейти к более крупному $n$.
Чтобы объяснить то, что может показаться логическим противоречием, здесь необходимо пояснить, что утверждение о том, что существование многих моделей $\mathsf{ZFC}_n$ можно доказать в $\mathsf{ZFC}$ для каждого $n$, но неравномерно (доказательство становится все длиннее и длиннее по мере того, как $n$ растет), поэтому $n$должно быть конкретным натуральным числом, универсально определенным количественно (более $n$) утверждение не доказуемо в$\mathsf{ZFC}$. Но это не проблема, пока ваша теория зафиксирована и сформулирована в$\mathsf{ZFC}$ (который требует, чтобы он сам по себе не содержал таких метатеорем, как «для любого конкретного $n$ мы можем доказать следующее в $\mathsf{ZFC}$»). Так что вы должны убедиться, что это так для HTT (и, если вы достаточно смелы, найдите подходящий$n$).
(Просто чтобы дать представление о том, как в этом участвуют кардиналы, кардиналы $\kappa$ такой, что $V_\kappa$ это модель $\mathsf{ZFC}_1$ неподвижные точки $\gamma \mapsto \beth_\gamma$функция. Я не думаю, что есть какая-то надежда на разумное описание$\kappa$ такой, что $V_\kappa$ это модель $\mathsf{ZFC}_n$ для любого бетона $n\geq 2$. См. Также этот вопрос .)
- Значение предикатов с не более чем $n$ чередующиеся наборы неограниченных кванторов, начиная с кванторов существования, за которыми следует формула с ограниченными кванторами (значение формы $\forall x\in y$ или же $\exists x\in y$).
Хорошо, я потратил большую часть сегодняшнего дня, пытаясь понять это, фактически рассматривая некоторые детали HTT. Это была настоящая поездка; Я определенно несколько раз менял свою точку зрения. В настоящее время мне кажется, что ответ заключается в том, что HTT, как написано, может быть прочитан в этой формальной системе. (Это похоже на шутку, где в нерабочее время кто-то говорит: «Да, это очевидно». Определенно есть моменты, в которых нужно выбрать правильную интерпретацию, но, как и в любом математическом тексте, это уже так.) этим ответом я хочу выдвинуть аргумент, что HTT можно прочитать в этой формальной системе, пытаясь немного объяснить, как интерпретировать определенные вещи в случае возникновения двусмысленности, и почему я думаю, что, читая его таким образом, все должно работать. Но вполне вероятно, что я упустил из виду что-то важное, поэтому, пожалуйста, поправьте меня!
Как отмечает Тим Кэмпион, большинство ранних вещей работает без проблем - на самом деле, вселенные здесь даже не упоминаются. Пока этого не происходит, все работает в$V_{\kappa_0}$, в $V_{\kappa_1}$, И в $V$, а данная схема аксиом даже гарантирует, что любые сделанные конструкции будут совместимы.
При переходе к главам 5 и 6 необходимо уделять больше внимания. Позвольте мне попытаться представить некоторые определения и предложения из этих глав с трех разных точек зрения.
Классическая точка зрения ZFC или (равносогласованная) точка зрения теории фон Неймана - Бернейса - Гёделя (NBG), которая допускает классы в дополнение к множествам, поэтому мы можем говорить о категории (размера класса) всех множеств $\mathrm{Set}$.
Точка зрения HTT, то есть вселенных ZFC + Гротендика.
Точка зрения теории множеств Фефермана в том виде, в каком она изложена в вопросе. (На самом деле, я больше не уверен, действительно ли мне нужны эти границы софинальности. Но приятно знать, что их можно предполагать.)
Обратите внимание, что заданный вопрос предполагает, что один действительно интересуется первой точкой зрения, а другие - лишь постольку, поскольку они позволяют что-то доказать о первой точке зрения. Это согласуется с содержанием глав 5 и 6: вся теория презентабельных категорий хорошо вписывается в первую установку, в том числе и с философской точки зрения.
Хорошо, напомним, что это презентабельная категория - позвольте мне просто придерживаться категорий вместо $\infty$-категории, разница несущественна для нас - это категория (размер класса) $C$ который допускает все малые копределы и такой, что для некоторого регулярного кардинального $\kappa$, есть небольшая категория $C_0$ и эквивалентность $C\cong \mathrm{Ind}_{\kappa}(C_0)$,
т.е. $C$ получается путем свободного присоединения $\kappa$-фильтрованные копределы до $C_0$. (В частности,$C_0$ обязательно эквивалентна полной подкатегории $\kappa$-компактные объекты $C$.) В частности, презентабельные категории определяются небольшим объемом данных. Кроме того, идея состоит в том, что$C$это действительно категория всех объектов (наборов, групп, чего угодно). Эта точка зрения наиболее четко сформулирована в 1), в то время как в 2) и 3) понятие представимости внезапно снова зависит от вселенной, и внезапно они снова содержат только небольшие множества / группы / ...; позвольте мне соответственно называть их маленькими-презентабельными. Обратите внимание, что это понятие имеет смысл как в 2), так и в 3) и зависит только от$V_{\kappa_0}$. Тогда, в частности, небольшая презентабельная категория может быть определена в малой степени, поэтому живет в$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$, где это включение является равенством в п. 2) (но не в п. 3)).
В 2) обычно определяется категория с малым представлением как особый вид большой категории, что и является подходом HTT. Но здесь я на самом деле уже немного запутался: похоже, есть два понятия функторов$F: C\to D$: Те, которые можно определить в $V_{\kappa_0}$, что эквивалентно $F\in V_{\kappa_0+1}$ (а именно, $V_{\kappa_0+1}$ это именно классы $V_{\kappa_0}$) или все функторы в $V_{\kappa_1}$. Мне не кажется очевидным, что любой функтор$F: C\to D$ в $V_{\kappa_1}$ заключается в $V_{\kappa_0+1}$, в виде $C$ а также $D$ сами живут только в $V_{\kappa_0+1}$. Разница между этими двумя понятиями исчезает, если ограничиться доступными функторами, все из которых определимы. Обратите внимание, что пункт 1) говорит, что это действительно первое понятие, о котором мы должны заботиться! (До написания этого поста я не осознавал разницы.)
В 3) правильным способом продолжения является использование перспективы, продиктованной 1), которая заключается в том, что "$V_{\kappa_0}$-определяемые категории ", поэтому они живут в $\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$. Их снова можно рассматривать как$\kappa_1$-малые категории. Сначала я подумал, что здесь будет существенная разница между подходами 2) и 3), но на самом деле кажется, что в обоих случаях мы приходим к двум различным понятиям функторов, которые согласовываются, если ограничиваться доступными функторами.
Одна из основных теорем - теорема о присоединенном функторе: если $F: C\to D$является функтором представительных категорий, сохраняющим все малые копределы, то он допускает правый сопряженный элемент. Что на самом деле означает эта теорема?
В 1) это означает, что существует функтор $G: D\to C$ - что, в частности, означает, что это должно быть определено формулами, поскольку это то, чем являются функторы между категориями размера класса - вместе с (определимыми!) преобразованиями единиц и счетчиков, удовлетворяющими обычным условиям.
В 2) просто говорится о $C$ а также $D$ как маленький, если рассматривать в $V_{\kappa_1}$а затем утверждает существование правого сопряженного там. Без дополнительной информации это фактически не дает того, что мы хотели в 1), поскольку априори$G$(а также преобразования единиц и счетчиков) все лежат в большей вселенной. Но эту информацию можно получить, вспомнив, что$G$ действительно доступен (часть теоремы о присоединенном функторе, которую я пропустил, чтобы указать выше, но должен быть включен), и поэтому все определяется на множестве.
В 3) хотелось бы снова получить результат 1), но можно попробовать сделать это, как в 2), предварительно доказав существование таких данных в $V_{\kappa_1}$ а затем доказывая доступность, таким образом доказывая, что все находится в $\mathrm{Def}(V_{\kappa_0})$.
Давайте посмотрим, как это проявляется в нескольких первых местах главы 5, где используются вселенные.
Определение 5.1.6.2. Пусть $C$- категория, допускающая все малые копределы. Объект$X\in C$является вполне компактным , если функтор$j_X: C\to \widehat{\mathrm{Set}}$ сопредставлено $X$ сохраняет мелкие копределы.
Здесь $\widehat{\mathrm{Set}}$ является (очень большой) категорией множеств в $V_{\kappa_1}$. Давайте интерпретируем, что означает это определение в вышеупомянутых системах.
Здесь $C$- любая категория (возможно, размером с класс). Обратите внимание, что, особенно в HTT, «локально маленький» не является стандартной гипотезой, поэтому это позволяет даже морфизму между двумя объектами быть правильными множествами. По этой причине функтор действительно должен перейти в$\widehat{\mathrm{Set}}$, и это то, о чем мы не можем говорить в этой обстановке. Итак, чтобы ответить на это возражение, нужно было бы переформулировать условие; это не должно быть сложно, но может быть немного неприятно.
Я думаю, в определении подразумевается, что $C$ любая категория, лежащая в $V_{\kappa_1}$. Это строго отражает настройку 1) в том смысле, что если$C$ является малоопределимой как исходящая из 1), то любая маленькая диаграмма копределов в $C$ автоматически определяется с малым числом.
Здесь у нас есть два варианта: один из 1) или один из 2), и они дают разные понятия. В случае конфликта перспектива из 1) является правильной, поэтому$C$является малоопределимой, и требуется коммутация с копределами малоопределимых диаграмм. Но в то время как в 1) у нас возникли проблемы с формулировкой условия, вселенные в 3) означают, что теперь условие может быть сформулировано: мы можем спросить, что оно принимает малоопределимые копределы в$C$ к пределам в $\widehat{\mathrm{Set}}$. Здесь$\widehat{\mathrm{Set}}$ наборы в $V_{\kappa_1}$.
Таким образом, в этом случае результат состоит в том, что нужно быть немного осторожным в 3) интерпретации, но руководствуясь тем, 1) можно дать правильное определение; и тогда система действительно помогает.
Предложение 5.2.6.2. Пусть $C$ а также $D$быть категориями. Тогда категории$\mathrm{Fun}^L(C,D)$ сопряженных слева функторов из $C$ к $D$, а также $\mathrm{Fun}^R(D,C)$ правых сопряженных функторов из $D$ к $C$ (канонически) эквивалентны друг другу.
С этой точки зрения это предложение действительно имеет смысл только тогда, когда $C$ а также $D$ маленькие, иначе $\mathrm{Fun}(C,D)$слишком большой. (Хочется рассмотреть такие категории функторов, когда$C$ а также $D$презентабельны (или доступны), но только при ограничении доступными функторами. Это обсуждение, которое появится позже в главе 5.) Тогда утверждение достаточно ясно, и приведенное доказательство применимо.
С этой точки зрения, я думаю, это то же самое, что и в пункте 1), за исключением того, что можно сформулировать тот же результат в другой вселенной.
То же самое.
Заметим, однако, что в существующем виде в 1) это предложение (пока) не может быть применено в случае $C$ а также $D$презентабельны. Во 2) и 3) (маленькие) презентабельные - это особые большие категории, к которым относится результат. Однако обратите внимание, что категории функторов и их эквивалентность все живут в большей вселенной, и мы не получаем информации о том, что они лежат ни в одной из них.$V_{\kappa_0+1}$ или же $\mathrm{Def}(V_{\kappa_0})$.
Следующее предложение рассматривает предпучковую категорию $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, и доказательство - типичный аргумент, связанный с переходом в большую вселенную для решения проблем гомотопической когерентности.
Предложение 5.2.6.3. Пусть $f: C\to C'$ быть функтором между малыми категориями и пусть $G: \mathcal P(C')\to \mathcal P(C)$ - индуцированный функтор предпучковых категорий, индуцированный композицией с $f$. потом$G$ прямо примыкает к $\mathcal P(f)$.
Здесь $\mathcal P(f)$ определяется как единственное малое, сохраняющее копредел, расширение $f$ (под вложением Йонеды).
Здесь у нас есть две категории размера класса и функторы между ними, все определяемые (как и должно быть). Предложение требует от нас найти (определимые!) Преобразования единиц и чисел, заставляющие коммутировать некоторые диаграммы. Это кажется не слишком сложным. Но в$\infty$-категории, как известно, сложно определить функторы вручную, так что на самом деле это не то, как поступает Лурье!
Здесь $\mathcal P(C)$ а также $\mathcal P(C')$особые большие категории. Лурье фактически применяет в доказательстве большое вложение Йонеды. Так что на самом деле это производит присоединения единиц и счетчиков только в какой-то более обширной вселенной. Как обсуждалось выше, я думаю, что это доказательство на самом деле не дает того, что мы хотели в 1)!
Мы можем спорить, как это делает Лурье, о создании данных в какой-то более крупной «вселенной». (Изменить: на самом деле, как указывает Тим Кэмпион, нужно сделать минимальный обходной путь, чтобы оправдать написанное. См. Комментарии к его ответу.)
Поэтому при чтении этого предложения в системе 2) или 3) следует сделать мысленный маркер, что пока доказанное утверждение слабее, чем можно было бы наивно надеяться. Но позже это исправят, заметив, что все определяется небольшим объемом данных.
Итог: хотя сначала я думал, что между 2) и 3) будет существенная разница, на самом деле я думаю, что (почти) ее нет. Одно отличие в том, что$\mathrm{Def}(V_{\kappa_0})\subset V_{\kappa_0+1}$ правильное включение, но на практике способ гарантировать сдерживание $V_{\kappa_0+1}$ кажется, чтобы доказать определимость в $V_{\kappa_0}$ (например, доказав, что определенные функторы доступны).
Хорошо, а теперь скажи мне, почему это не работает! :-)
Ответ на этот вопрос сильно зависит от того, что именно вы хотите от теории высших топосов, потому что выражение высокой логической силы - это цель, отличная от выражения удачно объединенной логической основы для алгебраической геометрии и теории чисел. Единые прочные основы для общей категориальной математики - одна прекрасная цель, и, кажется, цель многих авторов здесь. Для этой цели актуально все сказанное в комментариях и ответах на этот вопрос. Но для хорошей работы в области геометрии и теории чисел не требуется огромной логической силы.
Хотя HTT более тесно связан с вселенными, чем SGA, ни HTT, ни SGA не используют (очень сильную) схему аксиом замены. Таким образом, они могут использовать «вселенные» радикально более слабые, чем у Гротендика. В качестве типичного и уместного примера Гротендик сделал всего одно обращение к аксиомной схеме замены. Это в его весьма важном доказательстве, что каждая категория AB5 с порождающим множеством имеет достаточно инъективных объектов. И это использование замены оказывается устранимым. Это сработало, но на самом деле Гротендику это не понадобилось для получения результата.
Чтобы расширить использование замены Гротендиком: Райнхольд Бэр в 1940-х годах использовал трансфинитную индукцию (которая требует схемы замены аксиом), чтобы доказать, что модули (над любым данным кольцом) имеют достаточно инъективных элементов. Он сознательно исследовал новые методы доказательства и получил хороший результат. Тохоку Гротендика привел это доказательство в форму, показывающую, что каждая категория AB5 с небольшим набором образующих имеет достаточно инъективных - и несколько лет спустя Гротендик обнаружил, что это именно та теорема, которая ему нужна для топос-когомологий. Баер и Гротендик преследовали практические цели, не связанные с проблемами фонда, но оба тоже хотели создать правильные фонды. И они это сделали. Но оказывается, что они могли получить те же теоремы, правильно, без замены, почти такими же доказательствами, задав для начала достаточно большие наборы функций (используя набор степеней, но не замену). Есть результаты, которые действительно требуют схемы аксиом замены. Но такие результаты редко бывают вне фундаментальных исследований.
Многие люди, идущие с самых разных точек зрения (некоторые логики, некоторые не любят логику) с 1960-х годов, отметили, что в контексте алгебраической геометрии и теории чисел высокая логическая сила аксиомы вселенной Гротендика является фактически неиспользуемым побочным продуктом Стремление Гротендика к единой структуре когомологий. Теперь это можно сделать довольно точным: весь аппарат Гротендика, включая не только производные функциональные когомологии топосов, но и 2-категорию топосов, и производные категории, можно формализовать почти точно так же, как это было формализовано Гротендиком, но логическая сила намного ниже теории множеств Цермело-Френкеля или даже теории множеств Цермело. То же самое и с HTT. Вы можете получить его без недоступных вселенных или отражения, пока вам не понадобится обширная (и редко используемая) сила замены. Доказательства для HTT фактически не приводились. Это было для использования вселенных Гротендиком . Кажется очевидным, что то же самое будет работать и для HTT.
Необходимая логическая сила выражалась различными способами: теория простых типов (с арифметикой), арифметика конечного порядка, элементарная теория категорий множеств, теория множеств с ограниченным квантором Цермело. Грубо говоря, вы постулируете набор натуральных чисел и постулируете, что каждый набор имеет набор степеней, но вы не постулируете неограниченную итерацию множеств степеней. Достаточно наивная теория вселенных может быть консервативной по отношению к любой из них (как теория множеств Гёделя-Бернейса консервативна по отношению к ZFC) и адекватной всему аппарату большой структуры школы Гротендика.
Я бы рассмотрел консервативное расширение ZFC, полученное из ZFC добавлением константы $\alpha$ и следующие аксиомы:
$\alpha$ порядковый номер ($Ord(\alpha)$).
Предложение $\phi\leftrightarrow\phi^{V_\alpha}$, для каждого предложения на языке оригинала $\phi$ (схема аксиом).
$V_{\alpha}$ ведет себя как $V$(для всех предложений на языке теории множеств). Если нужны две (или более) юниверсы, можно добавить еще одну константу$\beta$ с соответствующими аксиомами, а аксиома $\alpha<\beta$.
Доказательство консервативности полученной теории над ZFC несложно.
Предположить, что $\phi$ доказуемо с помощью новых аксиом (аксиом, использующих $\alpha$), в котором $\phi$на языке оригинала. Поскольку любое доказательство конечно, имеется конечное число предложений$\phi_1$, ..., $\phi_n$ такой, что
$Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}})\rightarrow \phi$
доказуемо без каких-либо новых аксиом. Следовательно, можно думать о$\alpha$как свободная переменная, и приведенное выше предложение доказуемо в ZFC (теорема о константах). С$\alpha$ не встречается в $\phi$, в ZFC ($\exists$-вступление):
$\exists\alpha(Ord(\alpha)\wedge(\phi_1\leftrightarrow\phi_1^{V_{\alpha}})\wedge...\wedge(\phi_n\leftrightarrow\phi_n^{V_{\alpha}}))\rightarrow \phi$
Принцип отражения для ZFC гласит, что антецедент - это ZFC-теорема. ZFC доказывает, что modus ponens$\phi$.
Так что вы можете работать с новыми аксиомами и $V_{\alpha}$ ведет себя как вселенная, и все, что доказано, не упоминает $\alpha$ можно доказать уже в ZFC.
В комментариях возник вопрос о мотивации задать вопрос. Позвольте мне попытаться обратиться к этому здесь.
Прежде всего, это обучение! Как я уже упоминал в исходном вопросе, я сам играл с некоторыми "глупыми" кардинальными ограничениями и только позже узнал о принципе отражения, поэтому я хотел понять, что он может (и чего не может), и могу ли я может каким-то образом автоматически перенести в эту машину любые дальнейшие сложные версии таких оценок. Так что это обычное дело, когда вы просто спотыкаетесь в темной комнате и очень хотели бы, чтобы комната была освещена! Итак, спасибо вам всем за разъясняющие ответы!
Другая причина в том, что недавно я был немного разочарован решением вселенных Гротендика для рассматриваемой проблемы. Позволь мне объяснить.
Я очень хочу поговорить о категории всех множеств или всех групп и т. Д. И хочу доказать теоремы об этом. И, по крайней мере, в версии теории ZFC фон Неймана-Бернайса-Гёделя (NBG), которая допускает классы, это совершенно верное понятие. Так что я нахожу онтологически очень приятным работать в этой обстановке, и мне бы очень хотелось, чтобы теорема о присоединенном функторе была теоремой о (представимых) категориях в этом смысле.
Теперь презентабельные категории определяются небольшим объемом данных, поэтому всегда можно работать с этим небольшим объемом данных и внимательно следить за относительными размерами. Фактически, многие доказательства в HTT явно отслеживают такие относительные размеры, но все же есть несколько мест, где было бы неплохо сначала взглянуть «шире» и взглянуть на эти большие категории, как если бы они были маленькими.
Действительно, теорема о сопряженных функторах касается функторов между большими категориями, и быстро становится неприятным говорить об этом изнутри NBG / ZFC. Обратите внимание, что утверждение теоремы о присоединенном функторе имеет смысл - оно просто требует, чтобы все данные присоединения были определимы. Но немного противно говорить об этом «изнутри». Так что определенно было бы неплохо иметь какую-то мета-теорию, с помощью которой можно было бы спорить об этих больших категориях и делать вид, что они маленькие. Тонкий вопрос «определяемости изнутри» может быть априори утерян в этой метатеории, но я считаю этот вопрос «определяемости изнутри» центральным, потому что, в конце концов, я хотел получить теорему обо всех множествах, поэтому я Меня устраивает то, что мне приходится уделять этому немного внимания - и, если отвлечься, оказывается, что именно в этом разница между работой с вселенными Гротендика и работой с «вселенными» Фефермана.
Вот почему вселенные Гротендика предназначены: они всегда дают вам большую вселенную для любой вселенной, в которой вы в настоящее время работаете. Я считаю, что существование вселенных Гротендика полностью интуитивно понятно, и на самом деле постулирование их существования кажется полностью равным постулированию бесконечное множество: вы просто позволяете собрать все, что у вас уже есть, в более крупную отдельную сущность.
Но теперь внезапно то, что я раньше думал, так как все наборы стали называть маленькими наборами, есть также много более крупных наборов. Таким образом, даже если я докажу теорему о присоединенном функторе в этой ситуации, это уже не теорема о функторах между категориями всех множеств / групп / ..., а только один из функторов между небольшими наборами / группами / .... Итак, если вы подумайте об этом, даже во вселенных ZFC + Grothendieck вы никогда не докажете ту теорему, которую вы действительно хотели, о категории всех множеств. (На самом деле, до недавнего времени я предполагал, что теорема о присоединенном функторе (для$\infty$-categories) - это утверждение ZFC, которое было доказано в «ZFC + Universes», но это не совсем верно: доказанное утверждение может быть сформулировано даже только в ZFC + Universes.)
Доказано, что справедливость теоремы о сопряженных функторах непротиворечива . А именно, предполагая согласованность вселенных ZFC +, теперь вы создали модель ZFC - модель небольших наборов в вашей модели вселенных ZFC + - в которой теорема верна. Итак, теперь вы можете работать с теорией «ZFC + теорема о присоединенном функторе», в которой теорема о присоединенном функторе может быть применена к категории всех множеств / групп / ..., но это определенно кажется мне обманом. Вы даже не доказали, что «ZFC + Вселенные + теорема о присоединенном функторе» непротиворечива! (Вы получите это, если начнете с согласованности чуть больше, чем ZFC + Universes, попросив$\kappa$ такой, что $V_\kappa$удовлетворяет ZFC + Universes. Опять же, это кажется мне совершенно справедливым предположением - просто продолжайте.) Но теперь вы можете увидеть опасность того, что вы непреднамеренно подниметесь по лестнице согласованности, поскольку вы неявно начнете использовать все больше и больше теорем, доказанных также для небольших множеств. для всех комплектов.
Было бы намного лучше, если бы вы знали, что во вселенных ZFC + Grothendieck все, что вы доказали относительно малых множеств, также является теоремой для всей внешней категории всех множеств. Это не происходит автоматически, но вы можете добавить это как схему аксиомы. Майк Шульман в разделе 12 теории множеств для теории категорий (arXiv: 0810.1279) обсуждает эту идею (что он обозначает ZMC): я нахожу это онтологически довольно приятным, он также, кажется, имеет очень простую аксиоматизацию (даже проще, чем ZFC!), но
а) эта дополнительная схема аксиом не является для меня полностью самоочевидной: почему все, что истинно в малых наборах, также должно выполняться для всех наборов? (Особенно, если у нас возникли проблемы с доказательством желаемого результата в первую очередь. Также обратите внимание, что это определенно не верно для любого понятия малых множеств: скорее, схема аксиомы гарантирует, что существует некоторое понятие малых множеств, для которых этот вид рефлексии. Теперь это кажется мне немного сомнительным, так как вначале я никогда не хотел маленьких наборов, поэтому теперь я постулирую их, а также прошу, чтобы они по-прежнему отражали поведение всех наборов в целом. Вероятно, хорошо, но не для меня самоочевидно.)
б) прочность последовательности этой схемы аксиом значительно выше: она такая же, как последовательность кардинала Мало. Это все еще невысокий уровень для крупных кардиналов, но он намного выше, чем простые вселенные Гротендика (которые действительно находятся внизу иерархии).
Что касается пункта а), тот факт, что мы смогли доказать непротиворечивость теоремы о присоединенном функторе из согласованности вселенных Гротендика, указывает в правильном направлении, но это само по себе не гарантирует, что они вместе согласованы. Я могу представить, что смогу убедить себя в разумности схемы аксиом, но я определенно думаю, что она требует гораздо большего обоснования, чем простые вселенные Гротендика. (Дополнительный вопрос: насколько велики большие кардиналы, можно оправдать использование идеи «позволить собрать воедино все, что у нас уже было»? Я не уверен, что это полностью четко сформулированный вопрос ... но для меня это измеримый кардинал определенно не относится к тому типу (но я рад, что поправлюсь), поскольку он, кажется, предполагает появление новых комбинаторных свойств.)
Еще одна причина, по которой я недавно был немного недоволен вселенными Гротендика, заключается в том, что, хотя в некотором смысле мы хотели бы использовать их, чтобы иметь возможность игнорировать теоретико-множественные тонкости, в некотором смысле они возвращаются, чтобы укусить вас, поскольку теперь вы должны указать в в какой вселенной живут определенные вещи. Иногда вам даже может потребоваться указать несколько разных вселенных для разных типов объектов (подумайте о связках на бесконечных множествах), и я обнаружил, что это быстро становится довольно уродливым. Я бы предпочел, чтобы все объекты жили вместе в одной вселенной.
Итак, размышляя о пучках на проконечных множествах, я пришел к выводу, что решение только с одной вселенной намного более эстетично и онтологически приятным, и это решение (сжатые множества) может быть формализовано в ZFC без проблем.
Итак, я утверждаю, что вселенные Гротендика на самом деле не решили проблему, которую они намеревались решить, поскольку
а) они по-прежнему не позволяют вам доказывать теоремы о категории всех множеств / групп / ... (кроме как в качестве результата согласованности или при более сильных аксиомах с большими кардиналами)
б) работая с ними, вам все равно придется беспокоиться о размерах - ваша категория всех наборов теперь разделена на наборы всех видов разных размеров (то есть в разных вселенных).
Кроме того, они также увеличивают прочность консистенции.
Теперь, после этого замечательного обсуждения здесь, я думаю, что предложение Фефермана на самом деле намного лучше. Однако, как также прокомментировал Майк Шульман, я считаю аксиомы Фефермана не описанием какого-либо онтологически правильного мира, но я рассматриваю «вселенные» теории Фефермана просто как удобство для того, чтобы говорить о больших категориях, как если бы они были маленькими. Другими словами, теория Фефермана в точности дает вам метатеорию, в которой можно спорить о таких больших категориях «извне». Но эту теорию я бы использовал только для доказательства теоремы ZFC. По сравнению с вселенными Гротендика теория Фефермана
a) действительно позволяет вам доказывать теоремы о категории всех множеств / групп / ..., потому что он явно включает схему аксиом, согласно которой все теоремы о малых множествах также являются теоремами о всех множествах.
б) Конечно, в рамках доказательства теоремы ZFC, которое вызывает некоторые нетривиальные проблемы с размером, очень приветствуется, что теория позволяет вам говорить о различных размерах. Более того, он делает это таким образом, что вы по-прежнему можете применять все аксиомы ZFC к каждой из «вселенных», а также заботится «за кулисами» о том, как все переписать в терминах (потенциально чрезвычайно тонких) кардинальных границ. в самом ZFC. Так что это похоже на язык программирования высокого уровня для аргументов, связанных со сложными кардинальными оценками в ZFC.
Кроме того, это не увеличивает силу согласованности, и фактически любые утверждения ZFC, доказанные на этом языке, являются теоремами ZFC. (Как я напомнил выше, мы могли бы также иметь а) + б) с вселенными Гротендика, но тогда они достигли бы последовательности кардинала Мало.)
Итак, в результате, я думаю, вселенные Фефермана гораздо лучше справляются с задачей предоставления мета-теории, чтобы «говорить о больших категориях, как если бы они были маленькими», чем вселенные Гротендика.
Позвольте мне добавить несколько заключительных причин, чтобы задать вопрос. Я думаю, что методы высших категорий, такие как изложенные в HTT, имеют очень важное значение не только в алгебраической топологии, откуда они возникли, но и во всей математике. Я, конечно, могу засвидетельствовать это в отношении теории чисел и алгебраической геометрии. Таким образом, их центральность также является важной причиной для анализа их устойчивости.
Чтение HTT - дело очень нетривиальное - долгое и сложное. Однако некоторые коллеги по теории чисел сказали, что одна из основных причин, по которой они не могут читать HTT, заключается в том, что он использует вселенные . А именно, они настолько привыкли к ZFC (и к проверке с особой осторожностью!), Что автоматически попытаются исключить любое использование юниверсов в аргументе. Теперь в SGA, по крайней мере, если бы вас интересовали только приложения для эталонных когомологий разумных схем, это было бы чем-то, что вы могли бы сделать вручную - например, просто добавить некоторые предположения о счетности, чтобы упростить задачу. Однако в HTT я не вижу никакого способа, чтобы кто-то смог установить кардинальные границы, пока вы читаете - аргументы слишком сложны для этого.
Итак, теперь я надеюсь, что смогу сказать им, что они могут проверить, что все работает в ZFC, и они все еще могут читать HTT (по сути), как написано, если они читают его в теории множеств Фефермана. Если они тщательно проверит (что они и сделают), им все равно может потребоваться заполнить небольшую лемму здесь и некоторые небольшие дополнительные аргументы там - но им все равно придется это сделать в любой книге из ~ 1000 страниц, и я могу представить что менее половины этих побочных замечаний имеют отношение к замене вселенных Гротендика «вселенными» Фефермана. Если кто-то действительно возьмется за этот проект, он, конечно, заслуживает полного уважения, если ему удастся в этой важной работе!
Позвольте мне закончить очень кратким замечанием о том, что, по-видимому, является ключевым моментом в переводе теории Фефермана. Я пришел к пониманию того, что Тим Кэмпион поднял в своем ответе, и теперь я вижу, что это также упоминалось во втором ответе Джейкоба Лурье. Грубо говоря, это следующее. Если$C$ презентабельная категория, то есть небольшая категория $C_0$ такой, что $C=\mathrm{Ind}_\kappa(C_0)$
для какого-то обычного кардинала $\kappa$, прилегая свободно все мелкие $\kappa$-фильтрованные копределы. Это делает$C$ естественно союз $C_\tau$s, где $C_\tau$ только собирает $\tau$-небольшой $\kappa$-фильтрованные копределы. Здесь$\tau$ - обычный кардинал такой, что $\tau\gg \kappa$. Эта возрастающая структура$C$ как союз $C_\tau$является центральным в теории презентабельных категорий, но на самом деле уровни перечисляются (определенными) обычными кардиналами. $\tau$. Если вы увеличите свою вселенную, вы также получите более крупную версию$C'$ из $C$ сам, а во вселенных Гротендика $C$ теперь один из хороших слоев $C'_\tau$ из $C$, где $\tau$- крайний кардинал предыдущей вселенной. Но во вселенных Фефермана это$\tau$не регулярно. Это может сделать некоторые аргументы более тонкими, но я ожидаю, что обычно эту проблему можно решить, просто вставив$C$ в некоторые $C'_\tau$ с участием $\tau$ некоторый обычный кардинал, больший, чем предельный кардинал меньшей вселенной.
В ответ на правку, которая сводит все к формальной системе с участием кардиналов $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
Я собираюсь пойти на, возможно, более опрометчивый шаг и предсказать, что для того, чтобы вписать главы 1–4 в эту формальную систему, не потребуется никакой реальной кардинальной арифметики. Скорее всего, для этой части книги все, что вам нужно сделать, это пройтись и добавить к различным утверждениям теорем гипотезы вида "$X$ является $\kappa_{-1}$-small ». В конце концов, эта часть книги действительно имеет дело только с небольшими объектами, за исключением нескольких конкретных больших объектов, таких как категория малых симплициальных множеств, категория малых симплициальных категорий и т. д., и такие вещи, как конструируются различные модельные структуры, но я считаю, что в каждом случае можно обойтись с использованием частного случая аргумента малого объекта для генерации кофибраций / ациклических кофибраций между конечно-представимыми объектами, так что трансфинитная индукция не требуется. На первый взгляд, выпрямление / распрямление выглядит как конструкции, которые могут серьезно использовать теорию множеств, но я собираюсь пойти дальше и предсказать, что они не представляют проблем для предлагаемой формальной системы.
Глава 5 становится все более раздражающей. Я считаю, что нужно будет сделать осторожный выбор в отношении основных теорем представимого ($\infty$) -категории. Что отличает презентабельные категории, так это то, что они очень чисто упаковывают теорему о сопряженном функторе, но, как вы говорите, обычная теорема о сопряженном функторе в этом случае имеет некоторые оговорки. Я мог бы пойти так далеко, чтобы сказать, что весь смысл размышлений о презентабельных категориях в первую очередь полностью теряется в этой обстановке. Вы не сможете доказать элементарные вещи вроде «презентабельные категории - это как раз доступные локализации предпучковых категорий». Я предсказываю, что какой бы выбор ни был сделан в отношении формулировки слабых версий основных теорем представимых категорий в этом контексте, будет какое-то приложение или потенциальное приложение, которое пострадает.
Главы 5 и 6 также содержат некоторые теоремы о конкретных очень больших категориях, таких как $\infty$-категория презентабельных $\infty$-категории и $\infty$-категория $\infty$-топои [1]. Кажется, что система такова, что это не будет проблемой как таковой , за исключением того, что проблемы, встречающиеся в базовой теории презентабельности, теперь будут усложнены. Вы не сможете доказать, что$Pr^L$ двойственен $Pr^R$. Вы не сможете доказать теорему Жиро (что ж, определения в любом случае будут меняться, поэтому я должен уточнить: вы не сможете доказать, что левые точные доступные локализации предпучковых категорий такие же, как локально малые категории, удовлетворяющие списку условий полноты, генерации и точности). Итак, любая теорема о$\infty$-topoi, доказательство которого начинается с предварительного пучка, а затем выполняется локализация, придется полностью переосмыслить.
Возможно, я здесь вне базы, но я считаю, что для глав 5 и 6 потребуются значительные дополнительные работы и действительно новые математические идеи, и в результате получится теория, которую будет значительно труднее использовать.
Напротив, я думаю, что если вы готовы ограничить внимание большими категориями, которые можно определить с помощью небольших параметров, тогда, хотя вам будет не хватать красивой возможности сказать: «Мы доказали это для небольших категорий, но теперь мы можем применить это к большим. one », вы получите гораздо более полезную теорию презентабельности, не покидая ZFC.
[1] На самом деле, в обычных основаниях эти категории бывают (с точностью до эквивалентности) только большими и не очень большими (точнее, имеют $\kappa_0$-много объектов и $\kappa_0$-размерные хомсы), но требуется немного поработать, чтобы это показать. Будет ли так в этой формальной системе? Я не уверен.
EDIT: Длинный комментарий в ответ на Питер SCHOLZE в ответ .
Я только что понял , что если$\kappa_0$ это не $\beth$-фиксированная точка, то не каждый набор в $V_{\kappa_0}$ имеет мощность $<\kappa_0$, так что множатся понятия «малость». К счастью, я думаю, что ваша формальная система доказывает, что$V_{\kappa_0}$ имеет $\Sigma_1$-замена, подразумевающая, что это $\beth$-фиксированная точка. Кризис предотвращен!
Возможно, этот подход систематического использования гипотез определимости в «сеттинге вселенной» будет работоспособным - сочетая «лучшее из обоих миров». Приятно то, что даже если вы явно используете метаматематические гипотезы, похоже, что вы все равно сможете сформулировать и доказать эти теоремы как отдельные теоремы, а не как схему.
Я немного смущен предложением 5.2.6.3 (последнее из обсуждаемых вами и младшая версия теоремы о присоединенном функторе). Я предполагаю, что предпучковая категория$P(C)$ будет определено, чтобы включать эти функторы $C^{op} \to Spaces$ которые лежат в $Def(V_{\kappa_0})$. Когда мы переходим к более крупной вселенной, переход обычно довольно плавный, потому что мы ожидаем$P(C)$ чтобы все копределы были проиндексированы $\kappa_0$-маленькие категории - совершенно естественное свойство для работы в $V_{\kappa_1}$. В самом деле, первый шаг лурье доказательства 5.2.6.3 состоит в том, чтобы показать, что левый сопряженный существует, используя тот факт, что$P(C)$имеет все малые копределы [2]. Однако в нынешних условиях мы никогда не можем предположить, что$\kappa_0$ является регулярным, и поэтому мы никогда не можем предположить, что $P(C)$имеет все маленькие копределы. Лучшее, что мы можем сказать, это то, что$V_{\kappa_0}$ думает $P(C)$имеет все маленькие копределы. Пока мы работаем в$V_{\kappa_0}$, это свойство «так же хорошо», как и наличие всех малых копределов. Но когда мы перейдем к$V_{\kappa_1}$, внезапно мы должны думать об этом как о метаматематическом свойстве. Возможно, позже я сяду и попробую посмотреть, можно ли заставить доказательство Лурье 5.2.6.3 работать в этих условиях, но я думаю, что на первый взгляд это неясно.
[2] Только после абстрактной проверки существования таким образом он показывает, что левый сопряженный должен быть указанным функтором. Конечно, этот маневр на самом деле является дополнительным осложнением, связанным с$\infty$-категориальная установка - в обычных категориях формулы для двух функторов могут быть непосредственно проверены как сопряженные, но в $\infty$-категории формула для сопряженного слева не является, очевидно, функториальной.