The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
cs.LO
Dec 2, 2025 · v1
TL;DR
Formalizes a Seifert-van Kampen framework via computational paths in Lean 4, with 41,130 lines across 107 modules.
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.
Problem
Computing fundamental groups of topological spaces requires the Seifert-van Kampen theorem, but a modular formalized framework for SVK within a computational-paths setting did not previously exist in Lean 4.
Approach
The authors develop a modular SVK framework within computational paths, where equality witnesses are explicit rewrite sequences governed by the LNDEQ-TRS. Contributions include pushouts as higher-inductive types with typeclass assumptions, free and amalgamated free products as quotients of word representations, an SVK equivalence schema parametric in user-supplied encode/decode structure, and extensions to higher homotopy groups via weak infinity-groupoid structure.
Results
The development is formalized in Lean 4 with 41,130 lines across 107 modules, using 36 kernel axioms for HIT type-constructor declarations. Instantiations compute pi_1(S^1 v S^1) = Z * Z, pi_1(S^2) = 1, and pi_1(S^3) = 1. Extensions include pi_2 abelian via Eckmann-Hilton, truncation levels, covering space theory, and Eilenberg-MacLane space characterization (S^1 = K(Z,1)).
