Formalizing colimits in Cat
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916854989062144 |
|---|---|
| author | Carneiro, Mario Riehl, Emily |
| author_facet | Carneiro, Mario Riehl, Emily |
| contents | Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite $\infty$-category theory has not been formalized. To support future work on formalizing $\infty$-category theory in Lean's mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that Cat has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_20704 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalizing colimits in Cat Carneiro, Mario Riehl, Emily Category Theory 03B38, 18A30, 18A35, 18N50, 68V20 Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite $\infty$-category theory has not been formalized. To support future work on formalizing $\infty$-category theory in Lean's mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that Cat has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete. |
| title | Formalizing colimits in Cat |
| topic | Category Theory 03B38, 18A30, 18A35, 18N50, 68V20 |
| url | https://arxiv.org/abs/2503.20704 |