Coslice Colimits in Homotopy Type Theory

إليك ملخص تقني مفصل لورقة "Colimits in Coslice Categories in Homotopy Type Theory" للباحثين بيري هارت وكوين بانغ هو (Favonia).

1. بيان المشكلة

تتناول الورقة بناء وتوصيف الـ colimits داخل فئات الـ coslice (coslice categories) لكون الأنواع (type universe $\mathcal{U}$) داخل نظرية النوع المتجانس (Homotopy Type Theory - HoTT).

• السياق: في HoTT، تُعرف الـ colimits عادةً كأنواع استقرائية عليا (Higher Inductive Types - HITs). وبينما توجد مخططات عامة للـ HITs، إلا أنها غالبًا ما تتعامل مع الـ colimits بطريقة "الصندوق الأسود".
• الفجوة: هناك حاجة لبناء الـ colimits في فئة الـ coslice ($A/\mathcal{U}$) بشكل صريح باستخدام الآليات الأساسية لنظرية نوع مارتن-لوف (MLTT) المعززة بالـ pushouts، وذلك باستخدام فقط الأدوات المتاحة. الهدف هو الكشف عن العلاقة الدقيقة بين هذه الـ "coslice colimits" والـ colimits العادية في الكون $\mathcal{U}$.
• تحديات محددة:
  • فئات الـ coslice ليست بالضرورة فئات محلية كارتيزية مغلقة (Locally Cartesian Closed - LCC)، مما يعقد نقل الخصائص مثل "الكونية" (universality).
  • فهم كيفية تفاعل الـ colimits مع أنظمة التحليل المتعامد (Orthogonal Factorization Systems - OFS) ونظريات الكوهومولوجيا (cohomology theories) في سياق الأنواع المنقطة (pointed types) والمجموعات العليا.

2. المنهجية

يستخدم المؤلفون نهجًا بنائيًا داخل HoTT، متجنبين افتراض مخططات HIT عامة لصالح بناءات صريحة باستخدام الـ pushouts والـ quotients.

• "الارتباط الرئيسي" (بناء الـ Quotient):
  يتضمن الجوهر طريقة بناء الـ colimit لمخطط $F$ في $A/\mathcal{U}$ (يُرمز له بـ $\text{colim}_A(F)$) عبر البدء بالـ colimit العادي للمخطط الأساسي في $\mathcal{U}$ ($\text{colim}(F_g(F))$)، ثم "لصق" الـ 2-cells اللازمة لاستيفاء بنية الـ coslice.

  • يعرفون دالة $\psi: \text{colim } A \to \text{colim}(F_g(F))$ مستحثة من المخطط الثابت عند $A$.
  • يشكلون مربع pushout (أي quotient) يتضمن $\text{colim } A$ و $\text{colim}(F_g(F))$ و $A$. هذا الـ quotient يعمل فعليًا على ملء "الحلقات المميزة" (distinguished loops) في الـ colimit العادي التي تنشأ من بنية الـ coslice (المسارات من الشكل $\eta(\text{pr}_2(F_i)(a))$).
  • يتم إثبات أن هذا البناء هو الـ colimit في $A/\mathcal{mathcal{U}}$ عبر إثبات وجود تكافؤ (equivalence) بين نوع الدوال الخارجة من هذا الكائن ونوع الـ cocones.

• بناء بديل (Pushout of Coproducts):
  باستخدام تمهيدية $3 \times 3$ (3x3 lemma)، يستنتج المؤلفون بناءً ثانيًا لـ coslice colimits كـ pushout لـ coproducts (مجموعات وتد - wedge sums). وهذا يحاكي المبرهنات الكلاسيكية وهو أمر بالغ الأهمية لتحليل التفاعلات مع الكوهومولوجيا.

• الإطار الفئوي (Categorical Framework):
  تستخدم الورقة مفهوم الفئات البرية (wild categories) (وهي الفئات التي تتحقق فيها التركيب والوحدات حتى المسارات/paths وليس بشكل صارم) و الدوال البرية (wild functors). هذا الإطار ضروري لأن الكون $\mathcal{U}$ وفئات الـ coslice الخاصة به لا تشكل فئات صارمة بالمعنى التقليدي. كما يطورون نظرية أنظمة التحليل المتعامد (OFS) ضمن هذا الإطار "البري".

3. المساهمات الرئيسية

أ. توصيف الـ Coslice Colimits

المساهمة الأساسية هي البناء الصريح لـ $\text{colim}_A(F)$ كـ quotient للـ colimit العادي. هذا يثبت "الارتباط الرئيسي" الذي يوضح أن الـ coslice colimits ليست HITs تعسفية، بل هي مشتقة بنيويًا من الـ colimits العادية عبر تقليص حلقات محددة.

ب. إنشاء الـ Colimits بواسطة دالة النسيان (Forgetful Functor)

يثبت المؤلفون أن دالة النسيان $U: A/\mathcal{U} \to \mathcal{U}$ تنشئ (creates) الـ colimits فوق الأشجار (trees) (الرسوم البيانية التي يكون الـ quotient الخاص بها متصلًا/contractible).

• النتيجة: إذا كان $\Gamma$ شجرة، فإن دالة النسيان تحفظ وتعكس الـ colimits.
• الأهمية: يعني هذا أنه بالنسبة للمخططات ذات شكل الأشجار، فإن الـ coslice colimit يكافئ الـ colimit العادي للأنواع الأساسية. وهذا يسمح بنقل الخصائص (مثل الكونية) من $\mathcal{U}$ إلى $A/\mathcal{U}$ في هذه الحالات المحددة.

ج. حفظ الاتصال وأنظمة التحليل (Factorization Systems)

توضح الورقة أن الـ coslice colimits تحفظ الفئة اليسرى لأنظمة التحليل المتعامد على الكون $\mathcal{U}$.

• مبرهنة: إذا كان المخطط يتكون من أنواع $(n, k)$-connected، فإن الـ coslice colimit الخاص به سيكون أيضًا $(n, k)$-connected.
• التطبيق: يثبت هذا أن فئة المجموعات العليا (وتحديدًا الـ $k$-tuply groupal $n$-groupoids، ويُرمز لها بـ $(n, k)\text{GType}$) هي كاملة من جهة الـ colimits (cocomplete). وهذه نتيجة هامة لأن هذه الفئات ليست مغلقة بوضوح تحت الـ colimits في السياقات القياسية.

د. الاستمرارية الضعيفة للكوهومولوجيا

يتحرى المؤلفون التفاعل بين الـ colimits ونظريات كوهومولوجيا Eilenberg-Steenrod.

• النتيجة: يثبتون أن دوال الكوهومولوجيا ترسل الـ finite colimits في $A/\mathcal{U}$ إلى limits ضعيفة (weak limits) في $\text{Set}$.
• الآلية: عبر الجمع بين بناء الـ pushout-coproduct وتسلسل Mayer-Vietoris، يظهرون أن الخريطة القانونية من الـ colimit إلى الـ limit لمجموعات الكوهومولوجيا هي surjective (epimorphism). وتحت فرضية بديهية الاختيار (Axiom of Choice)، يعني هذا وجود section، مما يجعلها limit ضعيف.

4. النتائج الرئيسية

1. الكونية فوق الأشجار (Universality over Trees): دالة النسيان $A/\mathcal{U} \to \mathcal{U}$ تنشئ الـ colimits للمخططات المفهرسة بالأشجار. وبناءً عليه، فإن الـ colimits فوق الأشجار في $A/\mathcal{U}$ تكون كونية (universal/pullback-stable).
2. تمامية الـ Colimits للمجموعات العليا (Cocompleteness of Higher Groups): فئة $(n, k)\text{GType}$ هي cocomplete. ويُستنتج ذلك من خلال إثبات أن الفئة الفرعية للأنواع $(k-1)$-connected في $A/\mathcal{U}$ هي reflective ومغلقة تحت الـ colimits.
3. حفظ الاتصال (Preservation of Connectedness): الـ colimits للأنواع المنقطة (pointed) من النوع $n$-connected تظل $n$-connected. وهذا يعمم حقيقة أن الـ suspension لنوع متصل هو نوع متصل.
4. الكوهومولوجيا والـ Weak Limits: بالنسبة للرسوم البيانية النهائية (finite graphs)، ترسل نظريات الكوهومولوجيا الـ colimits إلى weak limits. وهذا يوفر نسخة من نظرية النوع لـ الشروط المطلوبة لـ مبرهنة براون (Brown representability).

5. الأهمية

• الوضوح التأسيسي: تعمل الورقة على إزالة الغموض عن بناء الـ colimits في فئات الـ coslice، منتقلة من الوجود المجرد (عبر مخططات HIT عامة) إلى بناءات ملموسة وقابلة للحساب باستخدام الـ pushouts. وهذا أمر حيوي للتحقق الصوري (formal verification).
• الصورية (Formalization): تم صياغة أجزاء كبيرة من العمل، بما في ذلك البناء الرئيسي وحفظ أنظمة التحليل، باستخدام لغة Agda. وهذا يوفر أساسًا موثقًا لنظرية النوع المتجانس الاصطناعية (synthetic homotopy theory).
• نظرية النوع المتجانس الاصطناعية: تربط النتائج بين نظرية الهوموتوبي الكلاسيكية (حيث تُعرف أو تُفترض خصائص مثل cocompleteness لفئات المجموعات العليا) والمنطق الداخلي لـ HoTT. وهي تؤكد أن المنطق الداخلي يدعم هذه البنى الفئوية عالية المستوى.
• القابلية للتعميم: يمكن تطبيق إطار "الفئات البرية" والتقنيات المحددة للتعامل مع coslice colimits على سياقات أخرى في Hoots حيث تفشل الافتراضات الفئوية القياسية (مثل LCC).

باختصار، يقدم هارت وفافونيا نظرية بنائية رصينة للـ colimits في فئات الـ coslice، ويثبتان أنها تتوافق جيدًا مع الأشجار، وأنظمة التحليل، والكوهومولوجيا، مما يؤسس لتمامية (cocompleteness) الفئات الهامة للبنى الجبرية العليا داخل HoTT.