The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups

The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We formalize this theorem within the framework of computational paths, an approach to equality where witnesses are explicit sequences of rewrites governed by the confluent, terminating LNDEQ-TRS. Our contributions are: (i) pushouts as higher-inductive types with explicit path constructors; (ii) free products and amalgamated free products as quotients of word representations; (iii) an encode-decode proof establishing pi_1(Pushout(A, B, C), f, g) cong pi_1(A) *_{pi_1(C)} pi_1(B); and (iv) applications to the figure-eight (pi_1(S^1 v S^1) cong Z * Z) and 2-sphere (pi_1(S^2) cong 1). The framework makes coherence witnesses explicit as rewrite derivations. The development is formalized in Lean 4, where the pushout axioms and the encode map are assumed, while the decode map, amalgamation compatibility, and applications are fully mechanized (2050 lines). This demonstrates that the encode-decode method for higher-inductive types becomes fully constructive when path equality is decidable via normalization.

arxiv.org · arXiv.org