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

2025/12/02 by Arthur Ramos, Tiago M. L. de Veras, Ramos, Arthur F. +5
Computer Science · Mathematics · #Logic, programming, and type systems #Homotopy and Cohomology in Algebraic Topology #Geometric and Algebraic Topology

paper · pdf · doi:10.48550/arxiv.2512.03175

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₁(S¹ v S¹) = Z * Z), 2-sphere (pi₁(S²) = 1), and 3-sphere (pi₁(S³) = 1) with Hopf fibration context. Recent extensions include higher homotopy groups pi_n via weak infinity-groupoid structure (with pi₂ abelian via Eckmann-Hilton), and pi₁ >= 1 in the 1-groupoid truncated setting; truncation levels connecting the framework to HoTT; automated path simplification tactics; basic covering space theory with pi₁-actions on fibers; fibration theory with long exact sequences; and Eilenberg-MacLane space characterization (S¹ = 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.

Citations

• A Topological Application of Labelled Natural Deduction
• On the Calculation of Fundamental Groups in Homotopy Type Theory by\n Means of Computational Paths
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• On the Identity Type as the Type of Computational Paths
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Calculating the Fundamental Group of the Circle in Homotopy Type Theory
• Propositional equality, identity types, and direct computational paths

Related

• An alternative approach to the calculation of fundamental groups based on labeled natural deduction
• Formalizing Computational Paths and Fundamental Groups in Lean
• On Computational Paths and the Fundamental Groupoid of a Type
• A Generalization of Seifert-Van Kampen Theorem for Fundamental Groups
• The fundamental group in discrete homotopy theory