사례 연구 : ZFC에서 Quillen의 작은 객체 주장을 공식화하고 증명하려면 무엇이 필요합니까?
나는 범주 이론의 정리에서 우주에 대한 의존성을 제거하는 것에 대한 Peter Scholze의 흥미로운 질문 에 약간의 길을 잃고 있습니다. 특히, 나는 교체가 언제 호출되는지 정말로 모른다는 것을 인정하도록 강요 당하고 있으며, 그것이 "본질적인 방식으로"호출 될 때 신경 쓰지 않는다. 그래서 저는 그 현상의 합리적으로 구체적인 예를 통해 작업하고 싶습니다. 나는 대체가 초한 재귀를 허용하는 공리로 "정말"로 생각되어야한다는 것을 이해합니다. 내 감각은 범주 이론이 재귀를 무거운 방식으로 사용하지 않는 경향이 있다는 것입니다 (수학의 다른 분야보다 더 그렇긴 하지만 적어도 원시 페이시 가 사소하지 않은 레비 복잡성을 갖는 많은 정의를 가지고 있습니다. 공식$\phi(x,y,z,p,q)$ 세트라고 $z$ 및 기능 $p: z \to x$ 과 $q: z \to y$ 세트의 범주 제품입니다. $x,y$ 구문 상 $\Pi_1$, 이진 곱이 집합 범주에 존재한다는 진술은 구문 상 $\Pi_3$ (물론 한정된 수량 자 무시)).
다음 정리는 범주 이론 비 재귀 사용에 대한 주목할만한 예외 중 하나입니다.
정리 [Quillen] "작은 대상 인수": Let$\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)$A는 약한 분해 시스템 켜짐$\mathcal C$.
증명 은 nlab을 참조하십시오 . 기본적으로 분해는 초한 재귀에 의해 구성됩니다. 재귀는 구성의 각 단계에서 새로운 데이터가 도입되기 때문에 나에게 "필수적"인 것 같습니다.
형식화:
나는이 정리와 그 증명이 MK에서 간단하게 형식화 될 수 있다고 생각하는데, 범주 이론적 "소 / 대"구별은 MK의 "집합 / 클래스"구별로 해석됩니다. 나는 증명이 NBG에서 작동하는지에 대해 언급 할 자격이 없다고 생각하지만, 그 진술은 적어도 간단하게 이해된다.
ZFC에서 공식화 할 때 우리는 작거나 큰 구분과 관련하여 선택할 수 있습니다.
한 가지 옵션은 "우주"를 도입하는 것입니다. $V_\kappa$(실제로 ZFC에서 작업하려는 경우 평소보다 약한 종류의 우주가 될 것입니다). 우리는 "작다"를 "in"을 의미하는 것으로 해석 할 것입니다.$V_\kappa$". 우리는"정말 큰 물체 "를 고려하지 않을 것입니다. 우리가 말하는 모든 것은 세트가 될 것입니다. 특히 우리가 말하는 모든 카테고리는 그 자체로"작은 "것은 아니더라도 세트 크기가 될 것입니다. "현지에서 제공 할 수있는 카테고리"를 "$\kappa$-공동 완성, 로컬 $\kappa$-강력한 작은 카테고리 $\kappa$-작은, $\lambda$-일부 일반에 대한 대표 발전기 $\lambda < \kappa$"(그렇게 말하는 것이 차이를 만드는지 모르겠습니다. $V_\kappa$ 생각 $\lambda$ 정기 추기경입니다).
또 다른 옵션은 우주를 도입하지 않고 "작은"을 "집합 크기"를 의미하는 것으로 해석하는 것입니다. 이 경우 우리가 말하는 "대형"개체는 작은 매개 변수로 정의 할 수 있어야합니다. 따라서 매개 변수로 정의 할 수있는 객체 클래스, 매개 변수로 정의 할 수있는 모피 즘 클래스 등을 구성하는 범주를 정의합니다. 이것은 제한적으로 보일 수 있지만 로컬로 표현할 수있는 범주를 정의 할 수 있으므로 로컬로 표현할 수있는 경우에는 잘 작동합니다.$\mathcal C$ 정의 될, 매개 변수에 상대적 $(\lambda, \mathcal C_\lambda)$ (어디 $\lambda$ 정기 추기경이고 $\mathcal C_\lambda$ 작다 $\lambda$-공동 완성 카테고리), 카테고리로 $\lambda$-Ind 개체 $\mathcal C_\lambda$.
이제 손에있는 정리의 경우, 접근 방식 (2)는 필요한 "전사"가 간단하기 때문에 더 깔끔해 보이며 일단 완료되면 원래 증명이 수정없이 작동해야합니다. 나는 (2)의 주요 단점이 다른 곳에 있다고 생각합니다. 예를 들어, 지역적으로 표현 가능한 범주의 범주에 대한 정리를 공식화하는 것은 아마도 섬세한 문제 일 것입니다. 일반적으로 관련된 범주가 작을 때는 깨끗하고 개념적인 공식과 증명을 가지고 있지만 관련된 범주가 클 때는 성가신 기술적 수정이 필요한 범주에 대한 다양한 정리가있을 것입니다. 이러한 이유로 인해 (1)과 같은 접근 방식이 대규모 범주 이론 프로젝트에 선호되는 경향이 있습니다.
따라서 접근 방식 (1)을 따르고 있다고 가정 해 봅시다. 그러면 질문은 다음과 같습니다.
질문 1 : 접근법 (1)에 따라 위의 정리를 공식화하고 증명하기 위해 정확히 어떤 종류의 우주가 필요합니까?
질문 2 : ZFC에 의해 얼마나 많은 우주가 존재한다고 보장합니까?
아마도 질문 2에 대한 대답은 그러한 우주가 많다는 것입니다. 우리가 범주가 주어지면 그 범주를 작게 만들고 그 우주에 대한 정리를 호출 할 수있을만큼 큰 우주로 전달하는 것과 같은 일을 할 수있을만큼 충분합니다. .
질문 3 : 질문 1과 2에 답하려면 잡초를 얼마나 멀리 가야합니까?
정리의 증명을 깊이 분석해야합니까? 우리가 증명을 한 눈에 볼 수있는 쉬운 기준 루 브릭이 있습니까? 그리고 이와 같은 정리의 99 %에 대해 너무 많이 탐구하지 않고 "통과"라고 쉽게 말할 수 있습니까? 아니면 컴퓨터로도 문제가 없는지 확인할 수 있도록 우리가 호소 할 수있는 공식적인 메타 정리가 있습니까?
답변
Jacob Lurie의 의견 은 질문 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)에 대한 대답은 범주 이론에서 초한 재귀를 사용할 때 실제로 일반적으로 이와 유사한 방식으로 대체 사용을 제거 할 수있는 경우가 될 것입니다. 중요한 것은 요점을 놓친 것입니다. Jacob Lurie 가 Peter Scholze의 질문에 대한 응답으로 주장 했듯이 ZFC 화 범주 이론의 까다로운 문제는 초한 재귀와 관련이있는 것이 아니라 "큰 범주 사이를 자유롭게 오갈 수있는 것과 관련이 있습니다." "및"작은 범주 "는 다양한 방식으로 제공됩니다.
내 생각에 (2)에 대한 대답은 초한 재귀의 "대부분"범주 이론적 사용에 대해 위의 속성을 가진 "아기 우주"에 맞도록 "구성"하는 것이 실제로 매우 간단해야한다는 것입니다. 약간의 연습만으로도 정리가 가능하다는 것을 거의 한 눈에 확인할 수있는 능력을 개발할 수 있습니다. 그러나 나는 틀렸다는 것을 증명하고 이런 종류의 접근이 실패하는 범주 이론의 정리를 보여주고 싶습니다!
마지막으로,이 모든 작업을 수행하는 "더 자동적 인"방법이 있는지 여부에 대한 열린 의문이 남습니다. 아마도 "우리 우주는 어떤 형태의 대체도 만족할 필요가 없습니다"보다 약한 결론을 내릴 수 있습니다.