반사 원리와 우주
범주 이론 토론에서 모든 아벨 그룹 또는 모든 범주 등의 범주를 보려는 유혹이 종종 있으며, 이는 일반적인 집합 이론 문제로 빠르게 이어집니다. 이는 종종 Grothendieck 유니버스를 사용하여 방지됩니다. 집합 이론 언어에서는 접근하기 어려운 추기경을 수정합니다.$\kappa$ -이것은 $\kappa$ 모두를 위해 셀 수없는 추기경입니다 $\lambda<\kappa$, 또한 $2^\lambda<\kappa$및 모든 세트에 대해 $<\kappa$ 많은 세트 $S_i$ 크기 $<\kappa$, 또한 그들의 조합은 크기입니다 $<\kappa$. 이것은 무대가$V_\kappa\subset V$ "크기 세트 $<\kappa$"은 그 자체가 ZFC의 모델입니다. 파워 셋이나 유니온을 가져 오는 것과 같은 작업을 세트에 적용하면 절대 떠날 수 없습니다. $V_\kappa$. 그런 다음 이러한 집합을 "작은"이라고하며 작은 아벨 그룹의 범주는 확실히 잘 정의되어 있습니다.
역사적으로이 접근 방식은 Grothendieck에서 처음 사용되었습니다. 보다 최근의 기본 텍스트는 Lurie의$\infty$-카테고리. 그러나 이들의 사용은 항상 다소 반발을 불러 일으켰으며, 일부 사람들은 ZFC를 넘어서는 공리가 기존 문헌에 빠져 나가는 것을 꺼려합니다. 예를 들어, 페르마의 마지막 정리가 현재 McLarty에 의해 해결 된 ZFC에서 증명되었는지 여부에 대한 긴 논의가 있었던 것 같습니다. 최근에 나는 Lurie의 작업을 증명하는 정리에 대해 비슷한 주장이 나오는 것을 보았습니다. (개인적으로 나는 이것에 대해 강한 감정이 없으며 어느 쪽이든 논쟁을 이해합니다.)
다른 한편으로, 면밀한 조사를 통해 우주를 사용하는 것이 사실상 불필요하다는 사실이 항상 밝혀졌습니다. 예를 들어 스택 프로젝트는 유니버스를 사용하지 않습니다. 대신 ( 태그 000H가 말한 것을 참조하십시오 ) 그것은 효과적으로 가설을 약화시킵니다.$\kappa$ 강하게 접근 할 수 없습니다. 셀 수없는 공동 결승의 강력한 한계 추기경 같은 것입니다. 즉 : 모두를 위해 $\lambda<\kappa$, 하나는 $2^\lambda<\kappa$, 그리고 셀 수있는 세트 컬렉션 이있을 때마다$S_i$ 크기 $<\kappa$, 또한 $S_i$ 크기가있다 $<\kappa$. ZFC는 그러한 존재를 쉽게 증명합니다.$\kappa$, 그리고 아벨 그룹의 범주에서 상상할 수있는 거의 모든 논쟁은 실제로 다음 범주에서도 작동합니다. $\kappa$-그런 작은 아벨 그룹 $\kappa$. 더 복잡한 주장을한다면 그에 따라 초기 가설을 강화할 수 있습니다.$\kappa$. 이 게임을 직접 해보았 습니다. 결과 는 www.math.uni-bonn.de/people/scholze/EtCohDiamonds.pdf의 섹션 4를 참조하십시오 . 이 경험을 통해 나는 Lurie의 "Higher Topos Theory"또는 다른 유사한 범주 이론 작업을 유사하게 재 작성하여 접근 할 수없는 모든 추기경을 제거하고 신중하게 선택한 것으로 대체 할 수 있다고 확신합니다.$\kappa$ 위와 같은 속성으로.
사실, 반사 원리 ( 예를 들어 Stacks 프로젝트의 Tag 000F 에서 간략하게 논의 됨) 인 ZFC 의 정리 가 항상 가능 하다는 것을 보장하는 것처럼 보입니다 . 즉, 집합 이론의 유한 한 공식 집합에 대해 충분히 큰$\kappa$ 대략적으로 말하면 이러한 공식은 $V_\kappa$ 그들이 붙잡는 경우에만 $V$. 이것은 주어진 유한 공식 세트에 대해 몇 가지를 찾을 수 있다고 말하는 것 같습니다.$\kappa$ 그런 $V_\kappa$이 공식과 관련하여 우주처럼 행동하지만 반사 원리에 대한 순진한 이해로 저를 수정하십시오! (관련 사실은 ZFC가 ZFC 공리의 주어진 유한 조각의 일관성을 증명한다는 것입니다.)
반면에 주어진 수학 텍스트에는 유한하게 많은 공식 만 포함되어 있습니다 (일반적으로 발생하지 않는 "정리 스키마"를 언급하지 않는 한). 따라서 질문은 약간 도발적으로 표현됩니다.
반사 원리는 우주의 사용을 피하는 방식으로 고등 위상 이론을 재 작성하는 것이 가능해야 함을 의미합니까?
편집 (28.01.2021) : 모든 유용한 답변에 감사드립니다! 나는 지금 상황에 대해 훨씬 더 명확한 그림을 가지고 있다고 생각하지만 여전히 질문에 대한 답이 정확히 무엇인지 확실하지 않습니다.
내가 이해하는 바에 따르면 (대략)이 방향에서 가장 좋은 메타 정리는 다음과 같습니다 (HTT에 특화된). HTT는 두 개의 강력하게 접근 할 수없는 추기경을 수정합니다.$\kappa_0$ 과 $\kappa_1$, 따라서 작은 (in $V_{\kappa_0}$), 큰 (in $V_{\kappa_1}$), 매우 큼 ( $V$) 사물. 그런 다음 다음 공리 시스템에서 HTT를 읽으려고 시도 할 수 있습니다 (이것은 본질적으로 Feferman의 "범주 이론의 집합 이론적 기초"기사 중 하나이며 아래의 Rodrigo Freire의 답변에서도 제안되었습니다).
(i) 일반적인 ZFC 공리
(ii) 다른 두 개의 기호 $\kappa_0$ 과 $\kappa_1$, 그들이 추기경이라는 공리와 함께 $\kappa_0$ 셀 수 없으며, $\kappa_1$ 보다 크다 $\kappa_0$.
(iii) 모든 공식에 대해 말하는 공리 스키마 $\phi$ 집합 이론의 $\phi\leftrightarrow \phi^{V_{\kappa_0}}$ 과 $\phi\leftrightarrow \phi^{V_{\kappa_1}}$.
그런 다음 반사 원리를 사용하여 보여줄 수 있습니다 (증명 스케치는 아래 Rodrigo Freire의 답변 참조).
정리. 이 공리 시스템은 ZFC보다 보수적입니다. 즉,이 형식 체계에서 언급하지 않는 모든 정리$\kappa_0$ 과 $\kappa_1$ ZFC의 정리이기도합니다.
이것이 제가 갖고 싶은 결론입니다.
참고 $V_{\kappa_0}$ 과 $V_{\kappa_1}$ ZFC의 모델이지만 (비판적으로!) ZFC는 유한하게 공리화할 수없고 ZFC의 각 개별 공리 만이 (iii)에 의해 정해 지므로 공식 시스템 내에서 증명할 수 없습니다.
이 공리 시스템의 한 가지 좋은 점은 "우리는이 정리를 작은 범주에 대해 입증했지만 큰 범주에도 적용 할 수 있습니다"라는 형식의 가끔 인수를 명시 적으로 허용한다는 것입니다.
더 정확한 질문은 다음과 같습니다.
HTT의 주장이이 공식 시스템에서 작동합니까?
섹션 11의 Mike Shulman 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를 읽는 것이 매우 쉽다고 실제로 상상할 수 있습니다. Shulman은 이러한 경고와 함께 인접 펑터 정리가 증명 될 수 있다고 말하며 Lurie가 그의 답변에서 말했듯이 HTT의 주장은 집합 이론적 복잡성이 비슷합니다. 그러나 질문에 대한 답이 "예, 서면으로"인지 아니면 "아마도 예,하지만 약간의 노력을 기울여야합니다"인지 실제로 "아니요"인지 판단하는 데 여전히 관심이 있습니다. (이 스펙트럼에 대한 대답이 대략 어디에 속하는지 전문가들이 동의 할 수 있기를 진심으로 바랍니다.)
마지막 발언 : "불가 산성"가정이 약간 임의적이라는 것을 알 수 있습니다. 약간 더 큰 조합을 허용하지 않는 이유는 무엇입니까? 이를 처리하는 한 가지 방법은 기호를 추가하는 것입니다.$\kappa_{-1}$ 동일한 속성을 가지고 대신 $\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$ 그러나 약간 조작되었습니다.
추신 : 지금은 모든 관련 이전 MO 질문과 답변을 찾고 있습니다. 매우 관련성이 높은 것들은 여기 와 여기에 Joel Hamkins의 답변 입니다.
답변
나는 팔다리로 나가서 책 HTT가 대체물보다 더 강한 것을 사용하지 않는다고 제안 할 것입니다. $\Sigma_{15}$-집합 이론의 공식. (여기$15$ 무작위로 선택된 큰 숫자이고 HTT는 집합 이론에 관한 것이 아닌 무작위로 선택된 수학 책입니다.)
내 원래 답변에 대한 Gabe의 의견을 반영하여 이제 두 개의 개별 (그러나 관련) 주장을 결합하기 때문에 내가 쓴 내용이 오해의 소지가 있다고 생각합니다.
강하게 접근 할 수없는 추기경의 존재는 범주 이론에서 실제로 필요하지 않습니다.
ZFC의 전체 강도는 범주 이론에서 실제로 필요하지 않습니다.
나는이 두 가지 진술에 모두 동의하지만, 1)의 누군가를 설득하는 가장 좋은 방법은 2) 반성 원칙과 결합하는 것이 아니라고 생각합니다. 즉, 강하게 접근 할 수없는 추기경의 사용을 대체하려고 시도해서는 안됩니다. $\kappa$ 하나에 의해 $V_{\kappa}$ ZFC의 대부분을 모델링합니다.
내가보기에 우주가 해결하는 "문제"는 두 가지 유형의 추론의 조합을 정당화하는 것입니다.
A) 때로는 작은 범주에 대한 정리를 증명하는 것이 유용합니다. $\mathcal{C}$ 예를 들어 한계 및 공동 한계의 존재와 같은 멋진 추가 기능이있는 "큰"범주 (예 : Yoneda 임베딩 사용)에 임베드함으로써.
B) 큰 범주도 범주이므로 일반적으로 범주에 적용되는 모든 정리는 큰 범주에도 적용되어야합니다.
B)에 대해서만 걱정했다면 반성 원리가 적절할 수 있습니다. 추기경 선택$\kappa$ 그런 $V_{\kappa}$ ZFC의 큰 덩어리를 충족하는 경우 "작은 범주"를 "다음에 속하는 범주"로 다시 정의 할 수 있습니다. $V_{\kappa}$"및"큰 범주 "는"반드시 속할 필요는없는 범주 "를 의미합니다. $V_{\kappa}$"그리고 원하는 모든 기본 정리가 두 경우 모두에서 유효하다는 확신을 가질 수 있습니다.
그러나 A)에 대해서도 걱정한다면 이것이 반드시 도움이되는 것은 아닙니다. 카테고리로 시작한다고 가정 해 보겠습니다.$\mathcal{C}$ 에 속하는 $V_{\kappa}$, Yoneda 임베딩의 일부 버전이 필요합니다. 당연한 추측은 다음에서 펑터 범주에 포함시키는 것입니다.$\mathcal{C}^{\mathrm{op}}$ 크기 세트의 범주에 $<\tau$ (또는 그와 동등한 모델), 일부 추기경 $\tau$. 첫 번째 추측은$\tau = \kappa$,하지만 이것은 단지 의미가 있다고 생각합니다 $\kappa$액세스 할 수 없습니다 (그렇지 않으면 일부 홈 세트가 너무 큽니다). 어쨌든이 구조가 좋은 특성을 가지고 있다는 것을 보장한다면 , 추기경의 다른 특성 을 요구하고 싶을 것 입니다.$\tau$. 예를 들어,이 카테고리의 presheaves에 많은 colimits가 있기를 원한다면, 당신은$\tau$큰 공동 확정 성을 갖습니다. 그리고 어떤 종류의 추가 가정을해야할지 생각하기 시작하면 다시 시작한 곳으로 돌아갑니다. 어떤 종류의 카디널리티 추정치가 "크기 집합의 미리보기$< \tau$"는 세트의 모든 프리 시브 범주에 대한 좋은 근사치입니다. 따라서 반사 원리는 이러한 문제를 피하는 데 실제로 도움이되지 않습니다.
(편집 : 아래 글이 대부분 Peter의 원래 글을 반복한다는 것을 글을 쓰고 깨달았습니다. 그러나 누군가 유용하다고 생각되면 여기에 남겨 두겠습니다.)
ZFC와 같은 형식으로 엄격한 형식화를 원할 경우 가장 좋은 방법은 큰 범주를 모두 없애는 것입니다. 따라서 B)는 문제가되지 않습니다. A)를 다루기 위해 말하고 싶은 "큰"범주의 대부분이 특정한 방식으로 발생한다는 점에 주목하겠습니다. 하나는 작은 범주로 시작합니다.$\mathcal{C}$ 이미 특정 종류의 colimits가 있고 공식적으로 확대됩니다. $\mathcal{C}$ 더 큰 카테고리를 만들기 위해 $\mathcal{C}^{+}$임의의 공동 제한이 있습니다 (시작한 항목을 변경하지 않고). 이러한 방식으로 발생하는 카테고리를 로컬에서 표시 가능 이라고 하며 다음과 같은 간단한 공식이 있습니다.$\mathcal{C}^{+}$: 펑터의 범주 $F: \mathcal{C}^{\mathrm{op}} \rightarrow \mathrm{Set}$ 이것은 당신이 시작한 한계 (즉, 당신이 시작한 colimits $\mathcal{C}$).
이제 작은 범주의 세계에서 이것을 모방하고 싶다면 대신 몇 가지 추기경을 선택할 수 있습니다. $\kappa$ 대신 펑터를 고려하십시오. $F: \mathcal{C}^{\mathrm{op}} \rightarrow \{ \text{Sets of size < $\카파$} \}$, 이는 작은 카테고리에 해당합니다. $\mathcal{C}^{+}_{\kappa}$. 당신이 만나는 질문은 이것이 큰 카테고리에 대한 충분한 대체물인지 여부입니다.$\mathcal{C}^{+}$위. 예를 들어, 많은 제한과 공동 제한이 있습니까? 모든 공동 제한 을 갖도록 요청하는 것은 불합리 하지만 대신 다음을 요청할 수 있습니다.
Q) 카테고리는 $\mathcal{C}^{+}_{\kappa}$ 크기 다이어그램으로 인덱싱 된 colimits $< \kappa$?
Q)에 대한 대답은 "일반적으로 아니오입니다. $\kappa$ 예를 들어 무한 추기경이 있다면 $\lambda$ 크기 경계 $\mathcal{C}$ 그리고 당신이 시작하는 colimit 다이어그램의 수는 당신이 (i) $\kappa = (2^{\lambda})^{+}$ (및 카테고리 $\mathcal{C}^{+}_{\kappa}$예상되는 보편적 속성으로 특징 지을 수 있습니다). 또한이를 증명하기 위해 어떤 형태의 교체도 필요하지 않습니다.
이제 다음과 같이 질문 할 수도 있습니다.
Q ') 카테고리는 $\mathcal{C}^{+}_{\kappa}$ 크기의 다이어그램으로 색인 된 한계가 있습니다. $< \kappa$?
여기서 대답은 일반적으로 "아니오"입니다. $\kappa$액세스 할 수 없습니다. 그러나 특정 유형의 제한에만 관심이있는 경우 (예를 들어 Grothendieck topoi를 연구하는 경우 특히 유한 제한에 관심이있을 수 있음) 대답은 다시 "예 :$\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.
반성 원리가 유용한 한 (다른 답변이 지적했듯이 적어도 질문이있을 수 있음), Grothendieck 우주의 관련 속성이 ZFC 모델이라는 주장에만 직접적으로 도움이됩니다. 그러나 적어도 순진하게 공식화되면 범주 이론이 이것보다 더 많이 사용하는 곳이 많이 있습니다. 구체적으로, 우리는 그로 텐 디크 우주 만족 사실 이용해 2 차 대체 한다는 의미를 어떤 함수$f:A\to V_\kappa$, 어디 $A \in V_\kappa$에 이미지가 있습니다. 에 대해 말하는 것$V_\kappa$ZFC 모델은 1 차 교체를 만족한다는 것을 의미 할뿐입니다.$f$ 이미지가있는 경우 $f$ 정의 가능하다 $V_\kappa$ 논리 공식으로.
나는 일반적으로 공식화 된 우주 기반 범주 이론에서 2 차 대체가 어디에나 있다고 생각합니다. 예를 들어${\rm Set}_\kappa$ 세트의 범주를 나타냅니다. $V_\kappa$, 증명하기 위해 ${\rm Set}_\kappa$ 도메인이 작은 모든 펑터에 대해 제한과 공동 제한을 인정한다는 순진한 의미에서 "완전하고 공동 완성"입니다. 이러한 펑터의 이미지를 단일 세트로 수집하려면 2 차 교체가 필요합니다.
이제 이것을 피하기 위해 범주 이론을 재구성하는 방법이 있습니다. McLarty의 논문은 집합 이론적 인 방식으로이를 수행합니다. 범주 적으로 일관된 접근 방식은 순진한 "대형 범주"(객체 및 형태가 속하지 않을 수있는 범주를 의미 함)를 대체하는 것입니다.$V_\kappa$) 큰 ${\rm Set}_\kappa$- 색인 된 카테고리 . 그러나 이것은 수작업으로 수행하는 훨씬 더 실질적인 종류의 재구성입니다.
내가 올바르게 이해했다면 다음과 같은 양식의 진술을 따르십시오.
"유니버스를 사용하여 HTT에서 어떤 것이 증명 되었다면, 일부로 제한하여 그들 없이도 증명할 수 있습니다. $V_\kappa$ ...에 대한 $\kappa$ 충분히 큰"
이에 대한 엄격한 대답은 HTT에 대한 자세한 정보가 없다면 ZFC가 일관성이 있으면 그러한 진술이있을 수 없다는 것입니다.
사실, 우주의 존재가 일치하지 않을 수 있으며 (사실 일관성이 있다는 것을 증명할 수 없음), 그런 상황에서 우주를 사용하여 무엇이든 증명할 수 있으므로 그러한 진술은 모든 것이 증명 될 수 있음을 암시합니다. 즉, ZFC가 일치하지 않습니다.
나는 무엇에서 증명할 수 있는지에 대해 약간 조잡하지만 주요 아이디어는 거기에 있습니다.
물론 우리는 HTT에 대해 알고 있습니다.주의 깊게 읽으면 우주를 사용하는 곳을 분석 할 수 있으며 실제로는 ZC + 대체의 전이 모델로 대체 될 수 있습니다. $\Sigma_{15}$-제이콥이 지적했듯이 공식. 이 경우 멋지게 동작하는 모델 (형식$V_\kappa$, for $\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$ Higher Topos 이론의 일부로 간주하는 모든 정리 (및 전제 조건으로 사용되는 다른 이론) 및 적절한 $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가이 형식적인 시스템에서 읽을 수 있다는 주장을 진행하고, 모호성이 발생할 수있는 경우 특정 사항을 해석하는 방법과 왜 모든 것이 작동해야한다고 생각하는지 설명하려고합니다. 그러나 중요한 것을 간과했을 가능성이 높으므로 수정하십시오!
Tim Campion이 지적했듯이, 대부분의 초기 작업은 문제없이 작동합니다. 사실, 우주에 대해서는 언급조차하지 않습니다. 그렇지 않은 한 모든 것이 작동합니다.$V_{\kappa_0}$, 에 $V_{\kappa_1}$, 및 $V$, 주어진 공리 스키마는 만들어진 모든 구성이 호환된다는 것을 보장합니다.
5 장과 6 장에 이르면 더주의를 기울여야합니다. 세 가지 다른 관점에서이 장의 정의와 제안을 몇 가지 소개하겠습니다.
고전적인 ZFC 관점 또는 (동일하게) von Neumann-Bernays-Gödel (NBG) 이론 중 하나. 집합에 추가로 클래스를 허용하므로 모든 집합의 (클래스 크기) 범주에 대해 이야기 할 수 있습니다. $\mathrm{Set}$.
ZFC + Grothendieck 유니버스 인 HTT의 관점.
질문에 명시된 형태의 Feferman의 집합 이론의 관점. (사실, 나는이 공동성 경계가 정말로 필요한지 더 이상 확신 할 수 없습니다. 그러나 그것들이 가정 될 수 있다는 것을 아는 것은 좋습니다.)
질문은 한 사람이 첫 번째 관점에 정말로 관심이 있다고 가정하고 다른 사람은 첫 번째 설정에 대해 무언가를 증명할 수있는 편리함을 전제로합니다. 이것은 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 : Let $C$모든 작은 공동 제한을 허용하는 카테고리 여야합니다. 객체$X\in C$이다 완전히 컴팩트 펑 경우$j_X: C\to \widehat{\mathrm{Set}}$ 공동 발표자 $X$ 작은 공동 한계를 보존합니다.
여기 $\widehat{\mathrm{Set}}$ 세트의 (매우 큰) 범주입니다. $V_{\kappa_1}$. 이 정의가 위의 시스템에서 의미하는 바를 해석해 보겠습니다.
여기 $C$모든 (아마도 클래스 크기) 카테고리입니다. 특히 HTT에서 "locally small"은 표준 가설이 아니므로 두 개체 간의 모피 즘이 적절한 집합이 될 수 있습니다. 이러한 이유로 펑 터는 실제로$\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 : Let $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})$.
다음 명제는 presheaf 카테고리를 고려합니다. $\mathcal P(C)=\mathrm{Fun}(C^{\mathrm{op}},\mathrm{Set})$, 그리고 그 증거는 동형 토피 일관성 문제를 해결하기 위해 더 큰 우주로의 통과와 관련된 전형적인 주장입니다.
명제 5.2.6.3 : Let $f: C\to C'$ 작은 카테고리 사이의 펑터가되어 $G: \mathcal P(C')\to \mathcal P(C)$ 구성에 의해 유도 된 presheaf 카테고리의 유도 된 기능 자 $f$. 그때$G$ 바로 옆에 $\mathcal P(f)$.
여기 $\mathcal P(f)$ 고유 한 작은 공동 제한 보존 확장으로 정의됩니다. $f$ (Yoneda 임베딩 아래).
여기에는 두 개의 클래스 크기 범주와 그 사이에 펑터가 있으며 모두 정의 할 수 있습니다. 이 명제는 우리에게 (정의 할 수있는!) 단위 및 공동 단위 변환을 찾도록 요청하여 일부 다이어그램을 이동시킵니다. 이것은 너무 어렵지 않은 것 같습니다. 하지만$\infty$-카테고리, 손으로 펑터를 정의하는 것은 유명하기 때문에 실제로 Lurie가 진행하는 방식이 아닙니다!
여기 $\mathcal P(C)$ 과 $\mathcal P(C')$특별한 대형 카테고리입니다. 실제로 Lurie는 증명에 포함 된 큰 Yoneda를 적용합니다. 그래서 이것은 실제로 더 큰 우주에서만 단위와 공동 단위 부속물을 생성합니다. 위에서 논의했듯이이 증명은 실제로 우리가 1)에서 원하는 것을 제공하지 않는다고 생각합니다!
우리는 Lurie가 더 큰 "우주"에서 데이터를 생성하는 것처럼 주장 할 수 있습니다. (편집 : 실제로 Tim Campion이 지적했듯이 작성된 내용을 정당화하기 위해 최소한의 우회를해야합니다. 그의 답변에 대한 주석을 참조하십시오.)
따라서 시스템 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는 대체의 (매우 강력한) 공리 체계를 실제로 사용하지 않습니다. 따라서 그들은 Grothendieck보다 근본적으로 약한 "우주"를 사용할 수 있습니다. 전형적인 예로서 Grothendieck은 대체 공리 계획에 대해 단 한 가지 호소를했습니다. 그것은 생성 세트가있는 모든 AB5 카테고리에 충분한 주입 제가 있다는 그의 매우 중요한 증거입니다. 그리고 이러한 교체 사용은 제거 할 수있는 것으로 밝혀졌습니다. 효과가 있었지만 Grothendieck은 실제로 그의 결과를 얻기 위해 필요하지 않았습니다.
Grothendieck의 대체 사용을 확장하기 위해 : 1940 년대 Reinhold Baer는 모듈 (주어진 링에 걸쳐)에 충분한 주입 제가 있음을 증명하기 위해 초한 유도 (교체 공리 체계가 필요함)를 사용했습니다. 그는 의식적으로 새로운 증명 기술을 탐구하고 있었고 좋은 결과를 얻었습니다. Grothendieck의 Tohoku는 작은 생성기 세트가있는 모든 AB5 범주에 충분한 주입 제가 있음을 보여주는 형식으로 증명을 캐스팅했습니다. 그리고 몇 년 후 Grothendieck은 이것이 그가 topos cohomology에 필요한 정리라는 것을 발견했습니다. Baer와 Grothendieck은 모두 실질적인 목표를 가지고 있었으며 기초 문제와는 관련이 없었지만 둘 다 기초를 올바르게 만들고 싶었습니다. 그리고 그들은했습니다. 그러나 그들은 (대체가 아닌 거듭 제곱 세트를 사용하여) 시작할만큼 충분히 큰 함수 세트를 지정함으로써 거의 동일한 증명으로 대체없이 정확하게 동일한 정리를 얻을 수있었습니다. 진정으로 대체 공리 체계가 필요한 결과가 있습니다. 그러나 이러한 결과는 기초 연구 외에는 거의 발생하지 않습니다.
1960 년대 이후로 매우 다른 각도 (일부 논리 학자, 일부 싫어하는 논리)에서 온 많은 사람들은 대수 기하학과 수 이론의 맥락에서 Grothendieck 우주 공리의 높은 논리 강도가 실제로 사용되지 않는 부산물이라고 언급했습니다. 동종 학을위한 통합 프레임 워크에 대한 Grothendieck의 열망. 이제는 매우 정확할 수 있습니다. toposes의 파생 된 functor cohomology뿐만 아니라 toposes의 2 개 범주 및 파생 된 범주를 포함하는 전체 Grothendieck 장치는 Grothendieck에서 공식화 한 것과 거의 동일한 방식으로 공식화 할 수 있습니다. Zermelo-Fraenkel 또는 심지어 Zermelo 세트 이론보다 훨씬 낮은 논리적 힘. HTT도 마찬가지입니다. 광대 한 (그리고 드물게 사용되는) 대체 힘이 필요 하지 않는 한 접근 할 수없는 우주 나 반사 없이 그것을 얻을 수 있습니다 . 실제로 HTT에 대한 증거는 제공되지 않았습니다. 그것은 Grothendieck의 우주 사용을위한 것입니다 . HTT에서도 동일하게 작동 할 것임이 분명해 보입니다.
필요한 논리적 강도는 단순 유형 이론 (산술 포함), 유한 순서 산술, 집합 범주의 기본 이론, 제한 수량 자 제르 멜로 집합 이론 등 무관심한 방식으로 표현되었습니다. 대략적으로 말하면, 당신은 일련의 자연수를 가정하고, 모든 세트에 검정력 세트가 있다고 가정하지만 무한한 거듭 제곱 세트를 가정하지는 않습니다. 우주에 대한 순진한 이론은 이들 중 어느 하나에 대해 보수적으로 주어질 수 있으며 (Godel-Bernays가 ZFC에 대해 보수적 인 방식) Grothendieck 학교의 모든 대형 구조 장치에 적합합니다.
상수를 추가하여 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 정리라고 말합니다. Modus ponens에서 ZFC는$\phi$.
따라서 새로운 공리로 작업 할 수 있습니다. $V_{\alpha}$ 우주처럼 행동하고, 언급하지 않은 모든 증명 된 $\alpha$ 이미 ZFC에서 증명 될 수 있습니다.
댓글에 나온 질문은 질문을 한 동기 에 관한 것이 었습니다 . 여기서이 문제를 해결해 보겠습니다.
무엇보다도 학습에 관한 것입니다! 내가 원래 질문에서 언급했듯이, 나는 약간의 "어리석은"추기경 경계를 가지고 놀았고 나중에 야 반영 원리에 대해 배웠기 때문에 그것이 무엇을 할 수 있는지 (그리고 무엇을 할 수 없는지를) 이해하고 싶었습니다. 이러한 추정치의 더 복잡한 버전을이 기계에 자동으로 전달할 수 있습니다. 그래서 그것은 당신이 어두운 방에서 그냥 걸어 다니는 일반적인 일이며, 방이 조명되기를 매우 좋아할 것입니다! 그래서, 빛나는 답변에 대해 모두 감사합니다!
또 다른 이유는 최근에 당면한 문제에 대한 Grothendieck 우주의 해결책에 약간 실망했기 때문입니다. 설명하겠습니다.
나는 모든 세트 또는 모든 그룹 등 의 범주에 대해 매우 많이 이야기하고 그것에 대한 정리를 증명하고 싶습니다. 그리고 적어도 수업을 허용하는 ZFC 이론의 NBG (von Neumann-Bernays-Gödel) 버전에서 이것은 완벽하게 유효한 개념입니다. 그래서 나는 그것이 존재 론적으로이 환경에서 작업하는 것이 매우 기쁘다는 것을 발견하고, 그런 의미에서 (표현 가능한) 범주에 대한 정리가되는 인접 펑터 정리를 매우 좋아할 것입니다.
이제 표시 가능한 범주는 소량의 데이터에 의해 결정되므로 항상이 소량의 데이터로 작업하고 상대적인 크기를주의 깊게 추적 할 수 있습니다. 사실, HTT의 많은 증명은 이러한 상대적인 크기를 명시 적으로 추적하지만, 먼저 "더 넓은 관점"을 취하고 이러한 큰 범주를 작은 것처럼 보는 것이 좋은 몇 가지 지점이 있습니다.
실제로, adjoint functor 정리는 큰 범주 사이의 functor에 관한 것이며, NBG / ZFC 내에서 이에 대해 이야기하는 것은 금방 불쾌 해집니다. adjoint functor 정리의 진술은 완벽하게 이해됩니다. 단지 adjunction의 모든 데이터를 정의 할 수 있는지 묻습니다. 그러나 "내부"에서 이러한 것들을 말하려는 것은 약간 불쾌합니다. 따라서 이러한 큰 범주에 대해 논쟁 할 수있는 일종의 메타 이론을 사용하고 작은 척하는 것이 분명 좋을 것입니다. "내부로부터의 정의"라는 미묘한 질문은이 메타 이론에서 선험적으로 잃어버린 것일 수 있지만, "내부로부터의 정의"에 대한이 질문을 중심으로 생각합니다. 왜냐하면 제가 원하는 것은 결국 모든 세트 에 대한 정리 였기 때문입니다. 약간의주의를 기울여야하는 것은 괜찮습니다. 요점을 없애기 위해 이것이 바로 그로 텐 디크 우주로 작업하는 것과 Feferman의 "우주"로 작업하는 것의 차이점이라는 것이 밝혀졌습니다.
그래서 이것이 그로 텐 디크 유니버스의 목적입니다. 그들은 항상 여러분이 현재 작업하고있는 모든 유니버스에 대해 더 큰 유니버스를 제공합니다. 저는 그로 텐 디크 유니버스의 존재가 완전히 직관적이라는 것을 알았습니다. 사실 그들의 존재를 포지하는 것은 처음에 무한 세트 : 이미 가지고있는 모든 것을 더 큰 독립 체로 수집 할 수 있습니다.
하지만 이제 갑자기 제가 모든 세트 로 생각했던 것을 작은 세트 라고 부르고 더 큰 세트도 많이 있습니다. 그래서 내가이 설정에서 인접 펑터 정리를 증명하더라도, 더 이상 모든 세트 / 그룹 / ...의 범주 사이의 펑터에 대한 정리가 아니라 작은 세트 / 그룹 / .... 사이의 펑터 중 하나뿐입니다 . ZFC + Grothendieck 유니버스에서도 모든 세트 의 범주에 대해 실제로 원하는 정리를 증명하지 못할 것입니다 . (사실 최근까지 나는 인접 펑터 정리 (for$\infty$-categories)는 "ZFC + Universes"에서 입증 된 ZFC의 진술이지만, 옳지 않습니다. 입증 된 진술은 ZFC + Universes에서만 공식화 될 수 있습니다.)
입증 된 것은 인접 펑터 정리 가 일관 된다는 것입니다 . 즉, ZFC + 유니버스의 일관성을 가정하여 이제 정리가 참인 ZFC 모델 (ZFC + 유니버스 모델의 작은 세트)을 생성했습니다 . 그래서 당신은 이제 "ZFC + a adjoint functor theorem"이론에서 작업 할 수 있습니다. 여기서 adjoint functor theorem은 모든 세트 / 그룹 / ... 의 범주에 적용될 수 있습니다 .하지만 그것은 확실히 제게 속임수처럼 느껴집니다. "ZFC + Universes + the adjoint functor theorem"이 일관성이 있다는 것을 증명하지도 못했습니다! (ZFC + Universes보다 약간 더 일관성이있는 것으로 시작하면$\kappa$ 그런 $V_\kappa$ZFC + Universes를 충족합니다. 다시 말하지만, 그것은 나에게 완전히 공정한 가정처럼 보입니다. 계속 진행하십시오.) 그러나 이제는 작은 세트에서도 입증 된 더 많은 정리를 암시 적으로 호출하기 시작함에 따라 실수로 일관성 사다리를 올라갈 위험을 알게 될 것입니다. 에 대한 모든 설정합니다.
ZFC + Grothendieck 유니버스에서 작은 세트에 대해 증명 한 모든 것이 모든 세트의 전체 주변 범주에 대한 정리라는 것을 알고 있다면 훨씬 더 좋을 것입니다. 이것은 자동이 아니지만 공리 스키마로 추가 할 수 있습니다. 범주 이론에 대한 집합 이론 (arXiv : 0810.1279) 의 섹션 12에있는 Mike Shulman 은이 아이디어 (그는 ZMC를 나타냄)에 대해 설명합니다. 존재 론적으로 매우 만족 스럽습니다. 또한 매우 단순한 공리 화 (ZFC보다 간단합니다!)를 가지고있는 것 같습니다. 그러나
a)이 추가 공리 스키마는 나에게 완전히 자명하지 않습니다. 왜 작은 세트에서 참인 모든 것이 모든 세트에도 적용 되어야 합니까? 특히 경우 (우리는 처음부터 원하는 결과를 증명하는 몇 가지 문제가 있었다 또한, 확실히 않습니다. 하지 누르고 있으면 어떤 작은 세트의 개념 : 오히려, 공리 스키마 보장이 있다는 일부 작은 세트의 개념있는 이런 종류의에 대한 처음에는 작은 세트를 원하지 않았기 때문에 이제는 약간 모호한 것처럼 보이므로 이제는 세트를 배치하고 모든 세트의 전체 동작을 여전히 반영하도록 요청합니다. 나에게 자명하다.)
b)이 공리 스키마의 일관성 강도가 상당히 높습니다 : Mahlo 추기경의 일관성과 동일합니다. 이것은 큰 추기경이 갈수록 여전히 낮지 만 단순한 Grothendieck 유니버스 (계층의 맨 아래에있는 정말 낮은)보다 훨씬 더 높습니다.
a)와 관련하여, Grothendieck 우주의 일관성으로부터 인접 펑터 정리의 일관성을 증명할 수 있다는 사실은 올바른 방향을 가리키고 있지만, 이것이 그 자체로 둘이 함께 일관성을 보장하는 것은 아닙니다. 나는 공리 스키마가 합리적이라고 스스로 확신 할 수 있다고 상상할 수 있지만, 단순한 Grothendieck 우주보다 훨씬 더 많은 정당화가 필요하다고 생각합니다. (부차적 인 질문 : "우리가 이미 가지고있는 모든 것을 모으는 것을 허용한다"라는 아이디어를 사용하여 정당화 할 수있는 큰 추기경은 얼마나 큰가? 이것이 완전히 잘 정의 된 질문인지 확실하지 않습니다 ...하지만 나에게는 측정 가능한 추기경은 확실히 그런 종류가 아닙니다 (하지만 새로운 조합 기능의 출현을 가정하는 것처럼 보이기 때문에 수정되어 기쁩니다).
내가 최근에 Grothendieck 우주에 대해 약간 불만을 느낀 또 다른 이유는 어떤 의미에서 우리는 그것들을 사용하여 집합 이론적 미묘함을 무시할 수 있기를 원하지만, 어떤면에서는 그들이 당신을 물기 위해 돌아옵니다. 어떤 우주가 살고 있습니다. 때로는 다양한 유형의 객체에 대해 여러 가지 다른 우주를 지정해야 할 수도 있습니다 (한정 세트에 대한 단을 생각하십시오). 차라리 모든 물체가 하나의 우주에서 함께 살기를 바랍니다.
그래서 무한한 세트의 단에 대해 생각하면서 나는 단지 하나의 우주만으로 훨씬 더 미학적이고 존재 론적으로 만족스러운 해결책을 찾았고,이 해결책 (압축 된 세트)은 문제없이 ZFC에서 공식화 될 수 있습니다.
좋아요, 저는 Grothendieck 우주가 그들이 해결하기로 한 문제를 실제로 해결하지 못했다고 주장합니다.
a) 여전히 모든 세트 / 그룹 / ... 의 범주에 대한 정리를 증명하는 것을 허용하지 않습니다 (일관성 결과 또는 더 강력한 큰 기본 공리에서 제외).
b) 그들과 함께 일하면서 여전히 크기 문제에 대해 걱정해야합니다. 모든 세트의 카테고리는 이제 모든 종류의 다른 크기의 세트로 계층화됩니다 (즉, 다른 우주에서).
또한 일관성 강도도 증가시킵니다.
자, 여기에서이 멋진 토론 후에 Feferman의 제안이 실제로 훨씬 낫다고 생각합니다. 그러나 Mike Shulman도 언급했듯이, 나는 Feferman의 공리가 존재 론적으로 올바른 세계를 설명하는 것이 아니라 Feferman 이론의 "우주"를 단지 편의로 간주하여 큰 범주를 작은 것처럼 이야기합니다. 즉, Feferman의 이론은 "외부"에서 이러한 큰 범주에 대해 논쟁 할 수있는 메타 이론을 정확하게 제공합니다. 그러나 그것은 내가 ZFC의 정리의 증거를 제공하기 위해서만 사용할 이론입니다. Grothendieck 우주와 비교하여 Feferman의 이론
A) 수행 이의 범주에 대해 정리를 증명 할 수 있도록 모든 세트 / 그룹 / ..., 명시 적으로 작은 세트에 대한 모든 정리는 모든 세트에 대한 정리 있다는 공리 스키마를 포함하고 있기 때문이다.
b) 물론, 사소하지 않은 크기 문제를 불러 일으키는 ZFC 정리의 증명 내에서 이론을 통해 다양한 크기에 대해 이야기 할 수 있다는 것은 매우 환영합니다. 또한 ZFC의 모든 공리를 각 "우주"에 적용 할 수있는 방식으로 그렇게하고, (잠재적으로 극히 미묘한) 카디널 경계의 관점에서 모든 것을 다시 작성하는 방법에 대한 "뒤에서"주의를 기울이고 있습니다. ZFC 자체에서. 따라서 ZFC에서 어려운 추기경 추정을 포함하는 인수를위한 고급 프로그래밍 언어와 같습니다.
또한 일관성 강도를 높이 지 않으며 실제로이 언어로 입증 된 ZFC의 모든 진술은 ZFC의 정리입니다. (위에서 기억했듯이, 우리는 또한 Grothendieck 유니버스와 함께 a) + b)를 가질 수 있지만, 그런 다음 Mahlo 추기경의 일관성까지 달릴 것입니다.)
따라서 결론은 Feferman의 우주가 Grothendieck 우주가하는 것보다 "큰 범주를 작은 것처럼 이야기하는"메타 이론을 제공하는 문제를 해결하는 데 훨씬 더 나은 역할을한다고 생각한다는 것입니다.
질문에 대한 마지막 이유를 추가하겠습니다. 나는 HTT에 배치 된 것과 같은 더 높은 범주의 기술이 그것이 시작된 대수 토폴로지뿐만 아니라 모든 수학에서 매우 중심적으로 중요하다고 생각합니다. 나는 수 이론과 대수 기하학과 관련하여 그것을 확실히 증명할 수 있습니다. 따라서 그들의 중심성은 일관성 강도를 분석하는 중요한 이유이기도합니다.
HTT를 읽는 것은 매우 사소한 문제입니다. 길고 복잡합니다. 그러나 일부 숫자 이론 동료들은 HTT를 읽을 수없는 주된 이유 중 하나 가 우주를 사용하기 때문이라고 말했습니다 . 즉, 그들은 ZFC (그리고 극도의주의를 기울여 확인하는 것!)에 너무 익숙해서 논쟁에서 우주의 사용을 자동으로 제거하려고 시도 할 것입니다. 이제 SGA에서 적어도 합리적인 계획의 etale cohomology에 대한 응용 프로그램에만 관심이 있다면 이것은 손으로 할 수있는 일이었습니다. 예를 들어, 물건을 작게 만들기 위해 몇 가지 가산 성 가정을 추가하면됩니다. 그러나 HTT에서 나는 당신이 따라 읽는 동안 누군가가 추기경 경계를 넣을 수있는 방법을 보지 못합니다. 논쟁은 이것에 대해 너무 복잡합니다.
그래서 지금 나는 그들이 것을 내가 그들에게 말할 수 있기를 바랍니다 수 ZFC에서 모든 것이 작동을 확인하고 그들은 여전히 HTT를 읽을 수 있습니다 (기본적으로) 작성, 그들은 Feferman의 집합 이론에서 읽을 경우. 그들이주의 깊게 확인한다면 (그들이 할 것입니다), 그들은 여전히 여기에 작은 기본형과 거기에 약간의 추가 논증을 채워야 할 수도 있습니다. 그러나 그들은 어쨌든 ~ 1000 페이지의 책에서 그렇게해야 할 것입니다. 이러한 측면 발언의 절반 미만이 Grothendieck 우주를 Feferman의 "우주"로 대체하는 것과 관련이 있습니다. 누군가가 실제로 그 프로젝트를 수행한다면, 물론 그들이이 중요한 일에 성공한다면 전적으로 인정받을 자격이 있습니다!
Feferman의 이론으로의 번역에서 핵심적인 점으로 보이는 것에 대해 아주 간단한 메모로 마무리하겠습니다. 나는 Tim Campion이 그의 답변에서 제기 한 요점을 인식하게되었고, 이것이 Jacob Lurie의 두 번째 답변에서도 언급되었음을 알게되었습니다. 대략 다음과 같습니다. 만약$C$ 표시 할 수있는 카테고리이고 작은 카테고리가 있습니다. $C_0$ 그런 $C=\mathrm{Ind}_\kappa(C_0)$
일부 정기 추기경 $\kappa$, 자유롭게 인접한 모든 작은 $\kappa$-필터링 된 공동 제한. 이것은 만든다$C$ 당연히 $C_\tau$의, 어디서 $C_\tau$ 만 수집 $\tau$-작은 $\kappa$-필터링 된 공동 제한. 여기$\tau$ 다음과 같은 일반 추기경입니다 $\tau\gg \kappa$. 이 증가하는 구조$C$ 조합으로 $C_\tau$의는 표현 가능한 범주 이론의 중심이지만 수준은 실제로 (특정) 일반 추기경에 의해 열거됩니다. $\tau$. 우주를 늘리면 더 큰 버전도 얻게됩니다$C'$ 의 $C$ 그 자체 및 Grothendieck 우주에서 $C$ 이제 멋진 레이어 중 하나입니다. $C'_\tau$ 의 $C$, 어디 $\tau$이전 우주의 컷오프 추기경입니다. 하지만 Feferman의 우주에서는$\tau$규칙적이지 않습니다. 이것은 몇 가지 논쟁을 더 미묘하게 만들 수 있지만 일반적으로 단순히 삽입 하여이 문제를 해결할 수 있다고 기대합니다.$C$ 일부로 $C'_\tau$ 와 $\tau$ 작은 우주의 컷오프 추기경보다 큰 일부 일반 추기경.
추기경을 포함하는 공식 시스템에 일을 고정시키는 편집에 대한 응답 $\kappa_{-1} < \kappa_0 < \kappa_{1/2} < \kappa_1$:
나는 아마도 더 부당한 조언을받은 사지로 나가서 1-4 장을이 형식적인 시스템에 맞추기 위해 실제 기본 산술이 필요하지 않을 것이라고 예측할 것입니다. 오히려이 책의이 부분에서해야 할 일은 ""형식의 다양한 정리 진술에 가설을 추가하는 것뿐입니다.$X$ 이다 $\kappa_{-1}$-작은 ". 결국, 책의이 부분은 작은 단순 집합의 범주, 작은 단순 범주의 범주 등과 같은 몇 가지 특정 큰 개체를 제외하고는 실제로 작은 개체 만 다룹니다 . 다양한 모델 구조가 구성되어 있지만, 각각의 경우에는 유한하게 표현할 수있는 객체들 사이의 cofibration / acyclic cofibration을 생성하기 위해 small object argument의 특별한 경우를 사용하여 얻을 수 있으므로 초 한적 유도가 필요하지 않다고 생각합니다. 겉으로보기에 곧게 펴거나 펴는 것은 집합 이론을 진지하게 사용하고있을 수있는 구조처럼 보이지만, 제안 된 형식 체계에 문제가 없을 것으로 예상합니다.
5 장은 더 짜증나게됩니다. 나는 프레젠터 블의 핵심 정리에 대해 신중한 선택을해야한다고 믿는다.$\infty$)-카테고리. 표현 가능한 범주를 틱하게 만드는 것은 인접 펑터 정리를 매우 깔끔하게 패키지화한다는 것입니다. 그러나 여러분이 말했듯이 일반적인 인접 펑터 정리는이 설정에서주의 사항과 함께 제공됩니다. 처음에 표현 가능한 범주에 대한 생각의 전체 요점이이 설정에서 완전히 취소되었다고 말할 수 있습니다. "표현 가능한 카테고리는 정확하게 presheaf 카테고리의 접근 가능한 지역화"와 같은 기본적인 것을 증명할 수 없습니다. 이 설정에서 표현 가능한 범주의 핵심 정리의 약한 버전을 공식화하는 것에 대해 어떤 선택을하든, 일부 응용 프로그램 또는 잠재적 응용 프로그램이 어려움을 겪을 것으로 예상합니다.
5 장과 6 장은 또한 다음과 같은 매우 큰 범주에 대한 몇 가지 정리를 포함합니다. $\infty$-프레젠터 블 카테고리 $\infty$-카테고리 및 $\infty$-범주 $\infty$-topoi [1]. 이 시스템은 기본 표현성 이론에서 직면 한 문제가 이제 복합화 된다는 점을 제외하고 는 이것이 실제로 문제가되지 않는 것처럼 보입니다 . 증명할 수 없을 것입니다.$Pr^L$ 이중이다 $Pr^R$. 당신은 Giraud의 정리를 증명할 수 없을 것입니다 (음, 정의는 어쨌든 유동적 일 것입니다. 그래서 저는 명확히해야합니다 : 당신은 presheaf 카테고리의 정확한 접근 가능한 지역화가 지역적으로 작은 것과 동일하다는 것을 증명할 수 없을 것입니다. 완전성, 생성 및 정확성 조건 목록을 충족하는 범주). 그래서 모든 정리$\infty$-presheaf 케이스로 시작하여 현지화하여 증명이 진행되는 topoi는 완전히 재검토되어야합니다.
아마도 나는 여기에서 벗어나 있지만 5 장과 6 장에는 상당한 추가 작업과 진정으로 새로운 수학적 아이디어가 필요하며 그 결과는 사용하기 훨씬 더 어려운 이론이 될 것이라고 믿습니다.
반대로, 작은 매개 변수로 정의 할 수있는 큰 카테고리에 관심을 제한하려는 경우 "작은 카테고리에 대해이 사실을 입증했지만 이제는 큰 카테고리에 적용 할 수 있습니다. ones "를 사용하면 ZFC를 떠나지 않고도 훨씬 더 유용한 표현성 이론을 얻을 수 있습니다.
[1] 사실, 일반적인 기초에서 이러한 범주는 (동등한 정도까지) 크지 않고 그다지 크지 않습니다 (더 정확하게는 $\kappa_0$-많은 물건과 $\kappa_0$-크기의 homs), 그러나 이것을 보여주기 위해 약간의 작업이 필요합니다. 이 공식 시스템에서도 여전히 그럴까요? 잘 모르겠습니다.
편집 : Peter Scholze의 답변 에 대한 긴 의견 .
나는 한 가지는 바로 실현이 경우 그$\kappa_0$ 아니다 $\beth$-고정 점, 모든 세트가 아닌 $V_{\kappa_0}$ 카디널리티 있음 $<\kappa_0$, 그래서 "작음"의 개념이 곱해집니다. 다행히도 당신의 공식 시스템이$V_{\kappa_0}$ 있다 $\Sigma_1$-교체, 즉 $\beth$-고정 점. 위기를 피했습니다!
아마도 "우주 환경"내에서 정의 가능성 가설을 체계적으로 사용하는 이러한 접근 방식은 "양 세계의 최고"를 결합하여 실행 가능할 것입니다. 한 가지 좋은 점은 메타 수학적 가설을 명시 적으로 사용하더라도 이러한 정리를 스키마가 아닌 단일 정리로 진술하고 증명할 수 있다는 것입니다.
나는 명제 5.2.6.3에 대해 약간 혼란 스럽습니다 (마지막으로 논의한 것, 그리고 인접 펑터 정리의 아기 버전). 나는 presheaf 카테고리가$P(C)$ 이러한 펑터를 구성하도록 정의됩니다. $C^{op} \to Spaces$ 어떤 거짓말 $Def(V_{\kappa_0})$. 우리가 더 큰 우주로 지나갈 때 전환은 일반적으로 매우 매끄 럽습니다.$P(C)$ 모든 공동 제한을 색인화하려면 $\kappa_0$-작은 카테고리-작업하기에 완벽한 자연 속성 $V_{\kappa_1}$. 실제로 Lurie의 5.2.6.3 증명의 첫 번째 단계는 다음과 같은 사실을 사용하여 왼쪽 인접 요소 가 존재 함 을 보여주는 것 입니다.$P(C)$모든 작은 colimits [2]가 있습니다. 그러나 현재 상황에서 우리는$\kappa_0$ 규칙적이기 때문에 우리는 $P(C)$모든 작은 공동 제한이 있습니다. 우리가 말할 수있는 최선은$V_{\kappa_0}$ 생각 $P(C)$모든 작은 공동 제한이 있습니다. 우리가 일하는 한$V_{\kappa_0}$,이 속성은 실제로 모든 작은 공동 제한을 갖는 것처럼 "좋습니다". 하지만 우리가$V_{\kappa_1}$, 갑자기 우리는 그것을 메타 수학적 속성으로 생각해야합니다. 아마도 나중에 나는 앉아서 5.2.6.3의 루리의 증명이 환경에서 작업을 할 수 있는지 여부를 확인하려고 노력하지만, 나는 생각한다 명백한 이 불분명하다.
[2] 이런 방식으로 추상적으로 존재를 확인한 후에야 왼쪽 인접이 표시된 펑터 여야 함을 보여줍니다. 물론,이 기동은 실제로$\infty$-범주 적 설정-일반 범주에서 두 펑터에 대한 공식이 인접 해 있는지 직접 확인할 수 있지만 $\infty$-범주 왼쪽 인접에 대한 공식은 분명히 기능적이지 않습니다.