The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
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_ | 1866908729573638144 |
|---|---|
| author | Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| author_facet | Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. |
| contents | The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of computational paths - an approach to equality where witnesses are explicit sequences of rewrites governed by the LNDEQ-TRS. Our contributions are: (i) pushouts as higher-inductive types with modular typeclass assumptions for computation rules; (ii) free products and amalgamated free products as quotients of word representations; (iii) an SVK equivalence schema parametric in user-supplied encode/decode structure; and (iv) instantiations for classical spaces - figure-eight (pi_1(S^1 v S^1) = Z * Z), 2-sphere (pi_1(S^2) = 1), and 3-sphere (pi_1(S^3) = 1) with Hopf fibration context. Recent extensions include higher homotopy groups pi_n via weak infinity-groupoid structure (with pi_2 abelian via Eckmann-Hilton), and pi_1 >= 1 in the 1-groupoid truncated setting; truncation levels connecting the framework to HoTT; automated path simplification tactics; basic covering space theory with pi_1-actions on fibers; fibration theory with long exact sequences; and Eilenberg-MacLane space characterization (S^1 = K(Z,1)). The development is formalized in Lean 4 with 41,130 lines across 107 modules, using 36 kernel axioms for HIT type-constructor declarations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_03175 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups Ramos, Arthur F. de Veras, Tiago M. L. de Queiroz, Ruy J. G. B. de Oliveira, Anjolina G. Logic in Computer Science 55Q05, 03B38, 68N18 F.4.1; I.1.3 The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of computational paths - an approach to equality where witnesses are explicit sequences of rewrites governed by the LNDEQ-TRS. Our contributions are: (i) pushouts as higher-inductive types with modular typeclass assumptions for computation rules; (ii) free products and amalgamated free products as quotients of word representations; (iii) an SVK equivalence schema parametric in user-supplied encode/decode structure; and (iv) instantiations for classical spaces - figure-eight (pi_1(S^1 v S^1) = Z * Z), 2-sphere (pi_1(S^2) = 1), and 3-sphere (pi_1(S^3) = 1) with Hopf fibration context. Recent extensions include higher homotopy groups pi_n via weak infinity-groupoid structure (with pi_2 abelian via Eckmann-Hilton), and pi_1 >= 1 in the 1-groupoid truncated setting; truncation levels connecting the framework to HoTT; automated path simplification tactics; basic covering space theory with pi_1-actions on fibers; fibration theory with long exact sequences; and Eilenberg-MacLane space characterization (S^1 = K(Z,1)). The development is formalized in Lean 4 with 41,130 lines across 107 modules, using 36 kernel axioms for HIT type-constructor declarations. |
| title | The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups |
| topic | Logic in Computer Science 55Q05, 03B38, 68N18 F.4.1; I.1.3 |
| url | https://arxiv.org/abs/2512.03175 |