Case study: what does it take to formulate and prove Quillen's small object argument in ZFC?
Tôi hơi mất hứng trước câu hỏi thú vị của Peter Scholze về việc loại bỏ sự phụ thuộc vào vũ trụ khỏi các định lý trong lý thuyết phạm trù. Đặc biệt, tôi buộc phải thừa nhận rằng tôi không thực sự biết khi nào người thay thế đang được gọi, đừng bận tâm khi nó được gọi "theo cách cần thiết". Vì vậy, tôi muốn làm việc thông qua một ví dụ cụ thể hợp lý về hiện tượng. Tôi hiểu rằng sự thay thế "thực sự" nên được coi là tiên đề cho phép đệ quy vô hạn. Cảm nhận của tôi là lý thuyết phạm trù có xu hướng không sử dụng đệ quy một cách nặng nề (mặc dù, hơn các nhánh khác của toán học, nó có rất nhiều định nghĩa mà ít nhất là loại nguyên tố có độ phức tạp Levy không đáng kể. Ví dụ, tôi nghĩ công thức$\phi(x,y,z,p,q)$ nói rằng bộ $z$ và chức năng $p: z \to x$ và $q: z \to y$ là một sản phẩm phân loại của các bộ $x,y$ là cú pháp $\Pi_1$và tuyên bố rằng các sản phẩm nhị phân tồn tại trong danh mục tập hợp là theo cú pháp $\Pi_3$ (tất nhiên là bỏ qua các định lượng bị giới hạn)).
Tôi nghĩ rằng định lý sau đây là một trong những ngoại lệ đáng chú ý đối với phạm trù-lý thuyết-không sử dụng-đệ quy:
Định lý [Quillen] "Đối số vật thể nhỏ": Cho$\mathcal C$ là một danh mục có thể sử dụng được ở địa phương và để $I \subseteq Mor \mathcal C$là một tập hợp các hình thái nhỏ. Để cho$\mathcal L \subseteq Mor \mathcal C$ là lớp rút lại của vật liệu tổng hợp vô hạn của sự thay đổi cobase của các sản phẩm đồng dạng của các hình thái trong $I$, và để $\mathcal R \subseteq Mor \mathcal C$ bao gồm những hình thái đó trực giao bên phải một cách yếu ớt với những hình thái của $I$. Sau đó$(\mathcal L, \mathcal R)$là một hệ thống phân tích nhân tử yếu trên$\mathcal C$.
Để có bằng chứng, hãy xem nlab . Về cơ bản, các thừa số được xây dựng bằng đệ quy vô hạn. Đối với tôi, đệ quy có vẻ "cần thiết" vì dữ liệu mới được đưa vào ở mỗi giai đoạn của quá trình xây dựng.
Chính thức hóa:
Tôi nghĩ rằng định lý này và cách chứng minh của nó có thể được chính thức hóa một cách đơn giản trong MK, trong đó sự phân biệt phạm trù định lý "nhỏ / lớn" được hiểu là sự phân biệt "tập hợp / lớp" của MK. Tôi không cảm thấy đủ điều kiện để bình luận về việc liệu bằng chứng có hoạt động trong NBG hay không, nhưng tuyên bố ít nhất cũng có ý nghĩa một cách dễ hiểu.
Khi nói đến việc chính thức hóa trong ZFC, chúng tôi có các lựa chọn để thực hiện liên quan đến sự khác biệt nhỏ / lớn:
Một lựa chọn là giới thiệu một "vũ trụ" $V_\kappa$(mà nếu chúng tôi thực sự đang cố gắng làm việc trong ZFC, sẽ là một loại vũ trụ yếu hơn bình thường). Chúng tôi sẽ giải thích "nhỏ" có nghĩa là "trong$V_\kappa$". Chúng tôi sẽ không coi" các đối tượng thực sự lớn "- mọi thứ chúng tôi nói đến sẽ là một tập hợp - đặc biệt, mọi danh mục chúng tôi nói đến sẽ có kích thước được thiết lập, ngay cả khi không phải là" nhỏ ". Chúng tôi sẽ giải thích "danh mục có thể trình bày được ở địa phương" thành "$\kappa$- không đầy đủ, cục bộ $\kappa$-loại nhỏ với mạnh $\kappa$-nhỏ, $\lambda$- máy phát điện đại diện cho một số $\lambda < \kappa$"(Tôi không biết nếu nói điều đó có tạo ra sự khác biệt không $V_\kappa$ suy nghĩ $\lambda$ là một hồng y thông thường).
Một lựa chọn khác là không giới thiệu bất kỳ vũ trụ nào và chỉ giải thích "nhỏ" có nghĩa là "có kích thước thiết lập". Trong trường hợp này, bất kỳ đối tượng "lớn" nào mà chúng ta nói đến phải được xác định từ các tham số nhỏ. Vì vậy, chúng tôi xác định một danh mục để bao gồm một lớp đối tượng có thể xác định tham số, một lớp hình thái có thể xác định tham số, v.v. Điều này có vẻ hạn chế, nhưng nó sẽ hoạt động tốt trong trường hợp hiển thị cục bộ, vì chúng ta có thể xác định một danh mục hiển thị cục bộ$\mathcal C$ được xác định, liên quan đến các tham số $(\lambda, \mathcal C_\lambda)$ (Ở đâu $\lambda$ là một hồng y bình thường và $\mathcal C_\lambda$ là một nhỏ $\lambda$danh mục -cocomplete), như danh mục của $\lambda$-Và các đối tượng trong $\mathcal C_\lambda$.
Bây giờ, đối với định lý trong tầm tay, cách tiếp cận (2) có vẻ rõ ràng hơn bởi vì "tranlsation" cần thiết là đơn giản, và một khi nó được thực hiện, chứng minh ban đầu sẽ hoạt động mà không cần sửa đổi. Tôi nghĩ rằng những hạn chế chính của (2) đến ở chỗ khác. Ví dụ, có lẽ sẽ là một vấn đề tế nhị để hình thành các định lý về phạm trù các phạm trù khả dụng cục bộ. Nói chung, sẽ có nhiều định lý khác nhau về các danh mục có công thức khái niệm và chứng minh rõ ràng khi các danh mục liên quan là nhỏ, nhưng đòi hỏi những sửa đổi kỹ thuật khó chịu khi các danh mục liên quan lớn. Chính vì những lý do đó mà các cách tiếp cận giống như (1) có xu hướng được ưa chuộng hơn cho các dự án lý thuyết phạm trù quy mô lớn.
Vì vậy, giả sử chúng ta đang theo cách tiếp cận (1). Câu hỏi sau đó trở thành:
Câu 1: Theo cách tiếp cận (1), chúng ta cần xây dựng và chứng minh chính xác loại vũ trụ nào?
Câu hỏi 2: Có bao nhiêu vũ trụ như vậy được ZFC đảm bảo tồn tại?
Có lẽ, câu trả lời cho Câu hỏi 2 sẽ là có rất nhiều vũ trụ như vậy - đủ để chúng ta có thể làm những việc như, cho một loại, chuyển đến một vũ trụ đủ lớn để làm cho loại đó nhỏ lại và gọi ra định lý cho vũ trụ đó. .
Câu hỏi 3: Chúng ta phải đi bao xa để trả lời câu hỏi 1 và 2?
Chúng ta phải phân tích cách chứng minh của Định lý một cách sâu sắc? Có một tiêu chí đánh giá dễ dàng cho phép chúng ta xem qua bằng chứng và, đối với 99% các định lý như thế này, có thể dễ dàng nói rằng nó "đạt" mà không cần đi sâu vào mọi thứ quá nhiều không? Hay thậm chí có một số siêu định lý chính thức mà chúng ta có thể áp dụng để ngay cả máy tính cũng có thể kiểm tra xem mọi thứ có ổn không?
Trả lời
Nhận xét của Jacob Lurie đưa ra câu trả lời cho Câu hỏi 1. Cụ thể, giả sử rằng các ước lượng mà tôi đưa ra trong nhận xét của mình là đúng, để xây dựng và chứng minh định lý thì chỉ cần giả sử rằng
- $\kappa$ là thường xuyên
và điều đó
- Cho mọi $\mu < \kappa$, có tồn tại $\rho < \kappa$ như vậy mà $\mu \ll \rho$ (điều đó có nghĩa là $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Có lẽ tài sản này của $\kappa$có thể được xem như một "hình thức" thay thế. Nhưng thực sự, những gì chúng tôi có là hai điều kiện về$\kappa$ hoàn toàn là lý thuyết tập hợp chứ không phải là siêu toán học, do đó câu trả lời cho Câu hỏi 1 là một cái gì đó rõ ràng hơn nhiều so với tôi đã nghĩ.
Điều này cho phép chúng tôi giải quyết Câu hỏi 2. Có lẽ, kết quả là ZFC chứng minh rằng có rất nhiều $\kappa$ thỏa mãn hai điều kiện trên.
Khi nói đến Câu hỏi 3, có vẻ như trong cách tiếp cận này, trên thực tế, chúng ta cần đi sâu vào chứng minh. Trên thực tế, có vẻ như để thực hiện cách tiếp cận này, chúng ta phải thêm một số nội dung toán học xác thực vào chứng minh, và thực sự chứng minh một tuyên bố mạnh mẽ hơn. Các câu hỏi tiếp theo sau đó trở thành
Nói chung sẽ có thể "xây dựng" "hầu hết" các định lý phạm trù theo cách này, hay các vấn đề khác sẽ xuất hiện trong quá trình của dự án "lý thuyết phạm trù ZFC-ify"?
Nếu câu trả lời cho (1) là "có" (hoặc nếu nó nói chung là "không" và chúng tôi hạn chế sự chú ý của mình vào các trường hợp là "có"), thì một dự án như vậy sẽ thực sự là bao nhiêu công việc?
Tôi đoán rằng câu trả lời cho (1) là khi nói đến việc sử dụng đệ quy vô hạn trong lý thuyết phạm trù, thực sự sẽ có trường hợp việc sử dụng thay thế có thể được loại bỏ theo cách tương tự như điều này, nhưng điều đó hơn quan trọng là tôi đã bỏ qua điểm: như Jacob Lurie lập luận để trả lời câu hỏi của Peter Scholze, các vấn đề hóc búa hơn với lý thuyết phạm trù ZFC-ifying không liên quan đến đệ quy vô hạn mà là với việc có thể tự do qua lại giữa "các danh mục lớn "và" danh mục nhỏ "theo nhiều cách khác nhau.
Tôi đoán rằng câu trả lời cho (2) là đối với "hầu hết" các sử dụng lý thuyết phạm trù của phép đệ quy biến đổi vô hạn, thực sự sẽ khá dễ dàng để "kiến tạo" chúng để chúng phù hợp với một "vũ trụ con" với các đặc tính ở trên hoặc một cái gì đó tương tự, và điều đó chỉ với một chút thực hành, người ta có thể phát triển khả năng xác minh gần như trong nháy mắt rằng điều đó có thể xảy ra, mặc dù vẫn trên cơ sở từng định lý. Nhưng tôi muốn được chứng minh là sai và chỉ ra một định lý trong lý thuyết phạm trù mà kiểu tiếp cận này không thành công!
Cuối cùng, đây là một câu hỏi mở liệu có cách nào "tự động hơn" để thực hiện tất cả những điều này - có lẽ với một kết luận yếu hơn là "vũ trụ của chúng ta không cần phải đáp ứng bất kỳ hình thức thay thế nào".