Studi kasus: apa yang diperlukan untuk merumuskan dan membuktikan argumen objek kecil Quillen di ZFC?
Saya sedikit tersesat pada pertanyaan menarik Peter Scholze tentang menghilangkan ketergantungan pada alam semesta dari teorema dalam teori kategori. Secara khusus, saya dipaksa untuk mengakui bahwa saya tidak benar-benar tahu kapan penggantian dipanggil, apalagi ketika itu dipanggil "dengan cara yang penting". Jadi saya ingin bekerja melalui contoh nyata dari fenomena tersebut. Saya memahami bahwa penggantian harus "benar-benar" dianggap sebagai aksioma yang memungkinkan rekursi transfinite. Saya rasa bahwa teori kategori cenderung tidak digunakan rekursi dengan cara tugas berat (meskipun, lebih dari cabang lain dari matematika, itu memang memiliki banyak definisi yang paling prima facie memiliki kompleksitas Levy trivial. Misalnya, saya pikir rumus$\phi(x,y,z,p,q)$ mengatakan bahwa set $z$ dan fungsi $p: z \to x$ dan $q: z \to y$ adalah produk kategoris dari himpunan $x,y$ secara sintaksis $\Pi_1$, dan pernyataan bahwa produk biner ada dalam kategori himpunan secara sintaksis $\Pi_3$ (mengabaikan bilangan terbatas tentu saja)).
Teorema berikut, menurut saya, adalah salah satu pengecualian penting untuk kategori-teori-non-penggunaan-rekursi:
Teorema [Quillen] "Argumen objek kecil": Biarkan$\mathcal C$ menjadi kategori yang dapat ditampilkan secara lokal, dan biarkan $I \subseteq Mor \mathcal C$menjadi sekumpulan kecil morfisme. Membiarkan$\mathcal L \subseteq Mor \mathcal C$ menjadi kelas retraksi komposit transfinite dari perubahan cobase dari koproduk morfisme di $I$, dan biarkan $\mathcal R \subseteq Mor \mathcal C$ terdiri dari morfisme yang lemah ortogonal kanan ke morfim dari $I$. Kemudian$(\mathcal L, \mathcal R)$adalah sistem faktorisasi lemah di$\mathcal C$.
Untuk buktinya, lihat nlab tersebut . Pada dasarnya, faktorisasi dibangun oleh rekursi transfinite. Rekursi tampaknya "penting" bagi saya karena data baru diperkenalkan pada setiap tahap konstruksi.
Formalisasi:
Saya pikir teorema ini dan buktinya secara langsung dapat diformalkan di MK, di mana perbedaan kategori-teori "kecil / besar" ditafsirkan sebagai perbedaan "set / kelas" MK. Saya merasa tidak memenuhi syarat untuk mengomentari apakah buktinya berfungsi di NBG, tetapi pernyataan itu setidaknya masuk akal secara langsung.
Dalam hal formalisasi di ZFC, kami memiliki pilihan terkait perbedaan kecil / besar:
Salah satu opsinya adalah memperkenalkan "alam semesta" $V_\kappa$(yang, jika kita benar-benar mencoba bekerja di ZFC, akan menjadi alam semesta yang lebih lemah dari biasanya). Kami akan menafsirkan "kecil" berarti "dalam$V_\kappa$". Kami tidak akan mempertimbangkan" objek yang benar-benar besar "- semua yang kami bicarakan akan menjadi satu set - khususnya, setiap kategori yang kita bicarakan akan berukuran set, bahkan jika bukan" kecil "per se. Kami akan menafsirkan "kategori yang dapat ditampilkan secara lokal" menjadi "$\kappa$-cocomplete, secara lokal $\kappa$kategori -kecil dengan yang kuat $\kappa$-kecil, $\lambda$generator -presentable untuk beberapa reguler $\lambda < \kappa$"(Saya tidak tahu apakah ada bedanya mengatakan itu $V_\kappa$ berpikir $\lambda$ adalah kardinal biasa).
Pilihan lainnya adalah tidak memperkenalkan alam semesta apa pun, dan hanya menafsirkan "kecil" sebagai "ukuran set". Dalam kasus ini, setiap objek "besar" yang kita bicarakan harus ditentukan dari parameter kecil. Jadi kami mendefinisikan kategori untuk terdiri dari kelas objek yang dapat ditentukan parameter, kelas morfisme yang dapat ditentukan parameter, dll. Ini mungkin tampak membatasi, tetapi ini akan berfungsi dengan baik dalam kasus yang dapat disajikan secara lokal, karena kami dapat mendefinisikan kategori yang dapat disajikan secara lokal$\mathcal C$ untuk didefinisikan, relatif terhadap parameter $(\lambda, \mathcal C_\lambda)$ (dimana $\lambda$ adalah kardinal biasa dan $\mathcal C_\lambda$ kecil $\lambda$kategori -cocomplete), sebagai kategori $\lambda$-Ind objek dalam $\mathcal C_\lambda$.
Sekarang, untuk teorema yang ada, pendekatan (2) tampaknya lebih bersih karena "tranlsation" yang diperlukan adalah langsung, dan setelah selesai, pembuktian asli harus bekerja tanpa modifikasi. Saya pikir kelemahan utama (2) datang di tempat lain. Misalnya, mungkin akan menjadi masalah rumit untuk merumuskan teorema tentang kategori kategori yang dapat disajikan secara lokal. Secara umum, akan ada berbagai teorema tentang kategori yang memiliki formulasi dan bukti konseptual yang bersih jika kategori yang terlibat kecil, tetapi memerlukan modifikasi teknis yang mengganggu jika kategori yang terlibat berukuran besar. Karena alasan seperti itulah pendekatan yang lebih seperti (1) cenderung disukai untuk proyek teori kategori skala besar.
Jadi mari kita asumsikan kita mengikuti pendekatan (1). Pertanyaannya kemudian menjadi:
Pertanyaan 1: Sebenarnya alam semesta seperti apa yang kita perlukan untuk merumuskan dan membuktikan teorema di atas dengan pendekatan berikut (1)?
Pertanyaan 2: Berapa banyak alam semesta yang dijamin keberadaannya oleh ZFC?
Agaknya, jawaban untuk pertanyaan 2 adalah bahwa ada banyak alam semesta seperti itu - cukup sehingga kita dapat melakukan hal-hal seperti, diberi kategori, lolos ke alam semesta yang cukup besar untuk membuat kategori itu kecil dan menggunakan teorema untuk alam semesta itu. .
Pertanyaan 3: Seberapa jauh kita harus pergi ke dalam gulma untuk menjawab Pertanyaan 1 dan 2?
Apakah kita harus menganalisis bukti Teorema secara mendalam? Adakah rubrik kriteria yang mudah yang memungkinkan kita melihat sekilas bukti dan, untuk 99% teorema seperti ini, dengan mudah mengatakan bahwa ia "lolos" tanpa terlalu banyak menggali lebih dalam? Atau adakah beberapa metatheorem formal yang dapat kami ajukan sedemikian rupa sehingga bahkan komputer dapat memeriksa bahwa semuanya baik-baik saja?
Jawaban
Komentar Jacob Lurie memberikan jawaban untuk pertanyaan 1. Yaitu, dengan asumsi bahwa perkiraan yang saya berikan dalam komentar saya benar, untuk merumuskan dan membuktikan teorema itu akan cukup untuk mengandaikan bahwa
- $\kappa$ biasa
dan itu
- untuk setiap $\mu < \kappa$, disana ada $\rho < \kappa$ seperti yang $\mu \ll \rho$ (yang berarti bahwa $\mu' < \mu, \rho' < \rho \Rightarrow (\rho')^{\mu'} < \rho$).
Mungkin properti ini dari $\kappa$dapat dilihat sebagai "bentuk" pengganti. Tapi sungguh, yang kita punya adalah dua syarat$\kappa$ yang murni teori-set daripada metamathematical, sehingga jawaban untuk pertanyaan 1 adalah sesuatu yang jauh lebih bersih dari yang saya kira.
Hal ini memungkinkan kita untuk menjawab Pertanyaan 2. Agaknya, hasilnya adalah ZFC membuktikan bahwa ada banyak dan banyak $\kappa$ memenuhi kedua kondisi di atas.
Ketika sampai pada Pertanyaan 3, tampaknya dalam pendekatan ini yang kita lakukan sebenarnya perlu menggali bukti yang cukup dalam. Faktanya, tampaknya untuk melakukan pendekatan ini, kita harus menambahkan beberapa konten matematika asli ke pembuktian, dan benar-benar membuktikan pernyataan yang lebih kuat. Pertanyaan selanjutnya kemudian menjadi
Apakah secara umum mungkin untuk "mengonstruksi" "sebagian besar" teorema teori kategori dengan cara ini, atau akankah masalah lain muncul selama proyek "teori kategori ZFC-ify"?
Jika jawaban untuk (1) adalah "ya" (atau jika umumnya "tidak" dan kita membatasi perhatian kita pada kasus di mana jawabannya "ya"), lalu "berapa banyak pekerjaan ekstra" yang akan dilakukan untuk proyek semacam itu?
Dugaan saya adalah bahwa jawaban untuk (1) adalah bahwa ketika datang ke penggunaan rekursi transfinite dalam teori kategori, memang biasanya penggunaan pengganti dapat dihilangkan dengan cara yang mirip dengan ini, tetapi lebih dari itu yang penting saya telah melewatkan intinya: seperti pendapat Jacob Lurie dalam menanggapi pertanyaan Peter Scholze, masalah pelik dengan teori kategori ZFC tidak berkaitan dengan rekursi transfinite melainkan dengan kemampuan untuk bebas bolak-balik antara "kategori besar "dan" kategori kecil "dengan berbagai cara.
Dugaan saya adalah bahwa jawaban untuk (2) adalah bahwa untuk penggunaan teoretis kategori "sebagian besar" dari rekursi transfinite, seharusnya cukup mudah untuk "membangun" mereka sehingga sesuai dengan "bayi semesta" dengan properti di atas atau sesuatu yang serupa, dan hanya dengan sedikit latihan, seseorang dapat mengembangkan kemampuan untuk memverifikasi hampir sekilas bahwa itu mungkin, meskipun masih berdasarkan teorema-demi-teorema. Tetapi saya ingin sekali terbukti salah dan menunjukkan teorema dalam teori kategori di mana pendekatan semacam ini gagal!
Akhirnya, ini meninggalkan pertanyaan terbuka apakah ada cara yang "lebih otomatis" untuk melakukan semua ini - mungkin dengan kesimpulan yang lebih lemah daripada "alam semesta kita tidak perlu memenuhi segala bentuk penggantian sama sekali".