Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

TL;DR

The work develops a constructive Seifert–van Kampen theorem within the computational-paths framework, modeling pushouts as higher-inductive types and computing π1 via an encode-decode method. It delivers a complete SVK argument, with applications to the figure-eight and spheres, and presents a substantial Lean 4 formalization. The approach provides explicit coherence witnesses in the form of rewrite derivations and outlines avenues for higher homotopy, truncation, and covering-space theory within a machine-checked setting. The combination of explicit path computations, quotient-based fundamental groups, and a Lean implementation offers a constructive, verifiable alternative to traditional HoTT treatments of SVK.

Abstract

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 LND_EQ-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)) = pi_1(A) *_{pi_1(C)} pi_1(B); and (iv) applications to the 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 the weak omega-groupoid structure (with pi_2 abelian via Eckmann-Hilton, and pi_2 = 1 in the 1-groupoid truncated setting); truncation levels connecting the framework to HoTT n-types; 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 framework makes coherence witnesses explicit as rewrite derivations. The development is formalized in Lean 4 with over 25,000 lines of mechanized proofs. This demonstrates that the encode-decode method for higher-inductive types becomes fully constructive when path equality is decidable via normalization.

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

TL;DR

The work develops a constructive Seifert–van Kampen theorem within the computational-paths framework, modeling pushouts as higher-inductive types and computing π1 via an encode-decode method. It delivers a complete SVK argument, with applications to the figure-eight and spheres, and presents a substantial Lean 4 formalization. The approach provides explicit coherence witnesses in the form of rewrite derivations and outlines avenues for higher homotopy, truncation, and covering-space theory within a machine-checked setting. The combination of explicit path computations, quotient-based fundamental groups, and a Lean implementation offers a constructive, verifiable alternative to traditional HoTT treatments of SVK.

Abstract

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 LND_EQ-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)) = pi_1(A) *_{pi_1(C)} pi_1(B); and (iv) applications to the 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 the weak omega-groupoid structure (with pi_2 abelian via Eckmann-Hilton, and pi_2 = 1 in the 1-groupoid truncated setting); truncation levels connecting the framework to HoTT n-types; 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 framework makes coherence witnesses explicit as rewrite derivations. The development is formalized in Lean 4 with over 25,000 lines of mechanized proofs. This demonstrates that the encode-decode method for higher-inductive types becomes fully constructive when path equality is decidable via normalization.

Paper Structure

This paper contains 51 sections, 14 theorems, 32 equations, 3 tables.

Table of Contents

  1. Introduction
  2. Relation to Classical SVK.
  3. Main Contributions
  4. Related Work
  5. Reading Guide
  6. Structure of the Paper
  7. Background: Computational Paths
  8. Computational Paths
  9. Notation.
  10. The Step Relation
  11. Rewrite Equality
  12. Loop Spaces and Fundamental Groups
  13. Pushouts as Higher-Inductive Types
  14. The Pushout Type
  15. Recursion Principle
  16. ...and 36 more sections

Key Result

Theorem 2.4

In Lean 4 (with proof-irrelevant Prop), for any paths $p, q : \mathrm{Path}(a, b)$, we have $p \sim q$.

Theorems & Definitions (46)

  • Remark 2.1: Implementation Note
  • Remark 2.2: Critical Pairs
  • Example 2.3: Rewrite Derivation
  • Theorem 2.4: Canonicity
  • proof
  • Remark 2.5: $\sim$ Triviality in Lean
  • Definition 2.6: Path-Connected
  • Definition 2.7: Loop Space
  • Definition 2.8: Fundamental Group
  • Remark 2.9: Base Point Dependence
  • ...and 36 more