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

TL;DR

This paper presents a formalized, modular approach to computing fundamental groups using computational paths within Lean 4, extending to higher homotopy groups and covering space theory, with applications to classical spaces.

Contribution

It introduces a novel framework for the Seifert-van Kampen theorem using computational paths, enabling formalized computations of fundamental groups and higher homotopy groups in Lean 4.

Findings

Successfully computed fundamental groups of classical spaces

Extended framework to higher homotopy groups and covering spaces

Formalized the entire development in Lean 4

Abstract

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.