กรณีศึกษา: การกำหนดและพิสูจน์อาร์กิวเมนต์วัตถุขนาดเล็กของ Quillen ใน ZFC ต้องใช้อะไรบ้าง?
ฉันหลงทางเล็กน้อยกับคำถามที่น่าสนใจของ Peter Scholze เกี่ยวกับการลบการพึ่งพาจักรวาลจากทฤษฎีบทในทฤษฎีหมวดหมู่ โดยเฉพาะอย่างยิ่งฉันถูกบังคับให้ยอมรับว่าฉันไม่รู้จริงๆว่าเมื่อใดที่มีการเรียกใช้การเปลี่ยนทดแทน แต่ไม่ต้องกังวลเมื่อมีการเรียกใช้ "ในทางที่จำเป็น" ดังนั้นฉันต้องการดำเนินการผ่านตัวอย่างที่เป็นรูปธรรมพอสมควรของปรากฏการณ์นี้ ฉันเข้าใจว่าการแทนที่ควร "จริงๆ" ถูกคิดว่าเป็นสัจพจน์ที่อนุญาตให้มีการเรียกซ้ำแบบไม่สิ้นสุด ความรู้สึกของฉันคือทฤษฎีหมวดหมู่มีแนวโน้มที่จะไม่ใช้การเรียกซ้ำในวิธีที่หนักหน่วง (แม้ว่าจะมากกว่าคณิตศาสตร์สาขาอื่น แต่ก็มีคำจำกัดความมากมายซึ่งอย่างน้อยเบื้องต้นก็มีความซับซ้อนของการจัดเก็บที่ไม่สำคัญตัวอย่างเช่นฉันคิดว่า สูตร$\phi(x,y,z,p,q)$ บอกว่าชุด $z$ และฟังก์ชั่น $p: z \to x$ และ $q: z \to y$ เป็นผลิตภัณฑ์หมวดหมู่ของชุด $x,y$ เป็นไวยากรณ์ $\Pi_1$และคำสั่งที่ว่าผลิตภัณฑ์ไบนารีมีอยู่ในหมวดหมู่ของชุดนั้นเป็นแบบวากยสัมพันธ์ $\Pi_3$ (ไม่สนใจตัวบ่งชี้ที่มีขอบเขตแน่นอน))
ฉันคิดว่าทฤษฎีบทต่อไปนี้คือหนึ่งในข้อยกเว้นที่น่าสังเกตสำหรับหมวดหมู่ - ทฤษฎี - ไม่ใช้การเรียกซ้ำ:
ทฤษฎีบท [Quillen] "อาร์กิวเมนต์วัตถุขนาดเล็ก":ให้$\mathcal C$ เป็นหมวดหมู่ที่นำเสนอได้ในท้องถิ่นและปล่อยให้ $I \subseteq Mor \mathcal C$เป็น morphisms ชุดเล็ก ๆ ปล่อย$\mathcal L \subseteq Mor \mathcal C$ เป็นชั้นของการหดกลับของคอมโพสิตทรานส์ฟินิทของโคเบส - การเปลี่ยนแปลงของผลิตภัณฑ์ร่วมของมอร์ฟิสใน $I$และปล่อยให้ $\mathcal R \subseteq Mor \mathcal C$ ประกอบด้วย morphisms เหล่านั้นที่มีมุมฉากทางขวาอย่างอ่อน ๆ กับ morphsims ของ $I$. แล้ว$(\mathcal L, \mathcal R)$เป็นระบบตีนเป็ดอ่อนแอใน$\mathcal C$.
เพื่อพิสูจน์ให้ดูNLAB โดยทั่วไปการแยกตัวประกอบถูกสร้างขึ้นโดยการเรียกซ้ำแบบไม่สิ้นสุด การเรียกซ้ำดูเหมือน "สำคัญ" สำหรับฉันเพราะมีการนำข้อมูลใหม่มาใช้ในแต่ละขั้นตอนของการก่อสร้าง
การทำให้เป็นทางการ:
ฉันคิดว่าทฤษฎีบทนี้และการพิสูจน์ของมันสามารถเป็นทางการได้อย่างตรงไปตรงมาใน MK โดยที่ความแตกต่าง "เล็ก / ใหญ่" ตามทฤษฎีถูกตีความว่าเป็นความแตกต่าง "ชุด / คลาส" ของ MK ฉันไม่รู้สึกว่ามีคุณสมบัติพอที่จะแสดงความคิดเห็นว่าการพิสูจน์นั้นใช้ได้ผลใน NBG หรือไม่ แต่อย่างน้อยคำแถลงก็สมเหตุสมผลอย่างตรงไปตรงมา
เมื่อพูดถึงการทำให้เป็นทางการใน ZFC เรามีทางเลือกให้เลือกเกี่ยวกับความแตกต่างเล็ก / ใหญ่:
ทางเลือกหนึ่งคือการแนะนำ "จักรวาล" $V_\kappa$(ซึ่งถ้าเราพยายามทำงานใน ZFC จริง ๆ จะเป็นจักรวาลที่อ่อนแอกว่าปกติ) เราจะแปลความหมายว่า "เล็ก" เป็น "ใน"$V_\kappa$"เราจะไม่พิจารณา" วัตถุขนาดใหญ่อย่างแท้จริง "ทุกสิ่งที่เราพูดถึงจะเป็นชุดโดยเฉพาะอย่างยิ่งทุกหมวดหมู่ที่เราพูดถึงจะถูกกำหนดขนาดแม้ว่าจะไม่" เล็ก "ก็ตามเราจะ แปลว่า "หมวดหมู่ที่นำเสนอได้ในท้องถิ่น" เป็นหมายความว่า "$\kappa$- สมบูรณ์ในเครื่อง $\kappa$- หมวดหมู่ขนาดเล็กที่มีความแข็งแรง $\kappa$- เล็ก $\lambda$เครื่องกำเนิดไฟฟ้าที่สามารถนำเสนอได้สำหรับบางคนปกติ $\lambda < \kappa$"(ฉันไม่รู้ว่ามันสร้างความแตกต่างหรือเปล่าที่พูดแบบนั้น $V_\kappa$ คิด $\lambda$ เป็นพระคาร์ดินัลปกติ)
อีกทางเลือกหนึ่งคือการไม่แนะนำจักรวาลใด ๆ และเพียงแค่ตีความว่า "เล็ก" เป็นหมายถึง "ขนาดที่กำหนด" ในกรณีนี้วัตถุ "ใหญ่" ใด ๆ ที่เราพูดถึงจะต้องกำหนดได้จากพารามิเตอร์ขนาดเล็ก ดังนั้นเราจึงกำหนดหมวดหมู่เพื่อประกอบด้วยคลาสของออบเจ็กต์ที่กำหนดพารามิเตอร์ได้, คลาส morphisms ที่กำหนดพารามิเตอร์ได้เป็นต้นสิ่งนี้อาจดูมีข้อ จำกัด แต่จะทำงานได้ดีในกรณีที่นำเสนอได้ในเครื่องเนื่องจากเราสามารถกำหนดหมวดหมู่ที่นำเสนอได้ในเครื่อง$\mathcal C$ ที่จะกำหนดโดยสัมพันธ์กับพารามิเตอร์ $(\lambda, \mathcal C_\lambda)$ (ที่ไหน $\lambda$ เป็นพระคาร์ดินัลปกติและ $\mathcal C_\lambda$ มีขนาดเล็ก $\lambda$- หมวดหมู่ที่สมบูรณ์) เป็นหมวดหมู่ของ $\lambda$-Ind วัตถุใน $\mathcal C_\lambda$.
ตอนนี้สำหรับทฤษฎีบทในมือแนวทาง (2) ดูเหมือนจะสะอาดกว่าเพราะ "tranlsation" ที่จำเป็นนั้นตรงไปตรงมาและเมื่อดำเนินการเสร็จแล้วการพิสูจน์ต้นฉบับควรใช้งานได้โดยไม่ต้องแก้ไข ฉันคิดว่าข้อเสียเปรียบหลักของ (2) มาจากที่อื่น ตัวอย่างเช่นอาจเป็นเรื่องละเอียดอ่อนในการกำหนดทฤษฎีบทเกี่ยวกับประเภทของหมวดหมู่ที่นำเสนอได้ในท้องถิ่น โดยทั่วไปจะมีทฤษฎีบทต่างๆเกี่ยวกับหมวดหมู่ซึ่งมีรูปแบบแนวคิดและการพิสูจน์ที่สะอาดเมื่อหมวดหมู่ที่เกี่ยวข้องมีขนาดเล็ก แต่ต้องมีการปรับเปลี่ยนทางเทคนิคที่น่ารำคาญเมื่อหมวดหมู่ที่เกี่ยวข้องมีขนาดใหญ่ ด้วยเหตุผลดังกล่าวที่แนวทางเช่น (1) มักจะได้รับการสนับสนุนสำหรับโครงการประเภททฤษฎีขนาดใหญ่
สมมติว่าเรากำลังทำตามแนวทาง (1) คำถามจะกลายเป็น:
คำถามที่ 1:เราต้องกำหนดและพิสูจน์ทฤษฎีข้างต้นตามแนวทาง (1) อย่างไร?
คำถามที่ 2: ZFC รับประกันว่าจักรวาลเหล่านี้มีอยู่กี่จักรวาล?
สันนิษฐานว่าคำตอบสำหรับคำถาม 2 จะมีจักรวาลจำนวนมาก - เพียงพอที่เราจะสามารถทำสิ่งต่างๆเช่นกำหนดหมวดหมู่ส่งผ่านไปยังจักรวาลที่มีขนาดใหญ่พอที่จะทำให้หมวดหมู่นั้นมีขนาดเล็กและเรียกใช้ทฤษฎีบทสำหรับจักรวาลนั้น .
คำถามที่ 3:เราต้องเข้าไปในวัชพืชเพื่อตอบคำถาม 1 และ 2 มากแค่ไหน?
เราต้องวิเคราะห์การพิสูจน์ทฤษฎีบทในเชิงลึกหรือไม่? มีเกณฑ์ง่าย ๆ หรือไม่ที่ช่วยให้เราสามารถดูการพิสูจน์ได้และสำหรับ 99% ของทฤษฎีบทเช่นนี้พูดง่ายๆว่า "ผ่าน" โดยไม่ต้องเจาะลึกสิ่งต่างๆมากเกินไปหรือไม่? หรือมีแม้กระทั่ง metatheorem ที่เป็นทางการบางอย่างที่เราสามารถอุทธรณ์ได้เช่นนั้นแม้แต่คอมพิวเตอร์ก็สามารถตรวจสอบได้ว่าทุกอย่างเรียบร้อยดี
คำตอบ
ความคิดเห็นของ 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-ifying นั้นไม่เกี่ยวข้องกับการเรียกซ้ำแบบไม่ จำกัด แต่จะสามารถย้อนกลับไปมาระหว่าง "หมวดหมู่ใหญ่ ๆ ได้อย่างอิสระ "และ" หมวดหมู่เล็ก ๆ น้อย ๆ "ในรูปแบบต่างๆ
ฉันเดาว่าคำตอบของ (2) ก็คือสำหรับการใช้การเรียกซ้ำตามทฤษฎีประเภท "ส่วนใหญ่" จริงๆแล้วมันควรจะค่อนข้างตรงไปตรงมาที่จะ "สร้างโครงสร้าง" เพื่อให้พอดีกับ "จักรวาลทารก" ที่มีคุณสมบัติข้างต้นหรือ สิ่งที่คล้ายกันและด้วยการฝึกฝนเพียงเล็กน้อยเราสามารถพัฒนาความสามารถในการตรวจสอบได้เกือบในพริบตาว่าเป็นไปได้แม้ว่าจะยังคงอยู่บนพื้นฐานของทฤษฎีบทโดยทฤษฎี แต่ฉันชอบที่จะได้รับการพิสูจน์ว่าผิดและแสดงทฤษฎีบทในทฤษฎีหมวดหมู่ที่วิธีการแบบนี้ล้มเหลว!
สุดท้ายนี้เป็นคำถามที่เปิดกว้างว่ามีวิธีที่ "อัตโนมัติกว่า" ในการทำทั้งหมดนี้หรือไม่บางทีอาจมีข้อสรุปที่อ่อนแอกว่า "จักรวาลของเราไม่จำเป็นต้องตอบสนองทุกรูปแบบของการทดแทนเลย"