HEXAGONbeta

A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem

Primarily AI-generated textHuman understanding: some partsmath.AT — Algebraic Topologymath.CT — Category Theory

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Sep 30, 2026 / CC BY 4.0

Abstract

We explain a Lean 4 formalization of the classical Seifert van Kampen theorem for the full fundamental groupoid. For an arbitrary topological space covered by two open subsets, the inclusion-induced square of ordinary continuous-path fundamental groupoids is a pushout in the category of categories. Every point is retained as an object; no basepoint, connectedness, or separation hypothesis is required. The development identifies an auxiliary directed path category for the indiscrete preorder with Mathlib's fundamental groupoid through strictly inverse functors and naturality equalities. It then assembles the pushout universal property from attributed path-subdivision and homotopy-grid helpers adapted from the directed-topology formalization of Basold, Bruin, and Lawson. We describe the descent construction, its transfer to ordinary fundamental groupoids, and the statement and verification boundaries of the exact artifact registered in Palomar. This is an expository account of a classical theorem and an existing formal artifact, with no claim of mathematical novelty or formalization priority.

Provenance statement

Manuscript drafted primarily with GPT-6.1 assistance for exposition, source alignment, and typesetting. The submitting contributor reports some human understanding; no independent human peer review is claimed. Pinned historical repository metadata separately reports gpt-6-astra assistance for formalization and packaging. The manuscript describes the registered classical theorem at https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000004&version=1 and the exact pinned Lean artifact at https://github.com/Arthur742Ramos/classical-svk-lean/tree/874680e16db88b4a41daadf56eafbac79fd2f748. This is an exposition of a classical theorem and existing formal artifact, with no novelty or formalization-priority claim. No fresh Lean build was performed; fresh source inspection is distinguished from recorded Palomar verification. First-party Lean source is Apache-2.0 and inherited directed source is MIT; the manuscript and uploaded TeX sources are CC BY 4.0.
FormalizationsPalomar

Tools used

Lean
LeanVersion 4.35.0-rc2
OpenAI
CodexVersion GPT-6.1
OpenAI
CodexVersion gpt-6-astra (pinned repository-reported formalization assistance)

References

  1. Basold, Henning; Bruin, Peter; Lawson, Dominique. The Directed Van Kampen Theorem in Lean. 15th International Conference on Interactive Theorem Proving (ITP 2024), vol. 309, pp. 8:1–8:18. 2024. \urlhttps://doi.org/10.4230/LIPIcs.ITP.2024.8DOI
  2. Brown, Ronald. Groupoids and Van Kampen's Theorem. Proceedings of the London Mathematical Society (3), vol. 17, no. 3, pp. 385–401. 1967. \urlhttps://doi.org/10.1112/plms/s3-17.3.385DOI
  3. Lawson, Dominique. Directed-Topology-Lean-4. 2024. Attribution and baseline specified by the registered artifact's vendor manifest. \urlhttps://github.com/Dominique-Lawson/Directed-Topology-Lean-4/tree/009529606c66d37ef93b4b81b8587f71ce4d2c56. Accessed September 30, 2026
  4. Mathlib Contributors. Mathlib fundamental groupoid and categorical infrastructure. 2026. \urlhttps://github.com/leanprover-community/mathlib4/tree/065356127b1dc0016f66b7283ce0ce2c4055aa55. In particular, \nolinkurlMathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean. Accessed September 30, 2026
  5. Palomar Registry. Classical Seifert–van Kampen theorem for the fundamental groupoid. 2026. Registered September 25, 2026. \urlhttps://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000004-v1.json. Accessed September 30, 2026
  6. Ramos, Arthur Freitas. Classical Seifert–van Kampen theorem for the fundamental groupoid. 2026. \urlhttps://github.com/Arthur742Ramos/classical-svk-lean/tree/874680e16db88b4a41daadf56eafbac79fd2f748. Accessed September 30, 2026
  7. Ramos, Arthur Freitas. ComputationalPathsLean. 2026. \urlhttps://github.com/Arthur742Ramos/ComputationalPathsLean/tree/257c659b7973aeda900d86a5da73b208712c7523. Relationship described in the registered artifact's provenance record. Accessed September 30, 2026
  8. Ramos, Arthur Freitas; Hulak, David Barros; de Queiroz, Ruy Jose Guerra Barretto. The Classical Seifert–van Kampen Theorem. 2026. Entry dated May 9, 2026. \urlhttps://isa-afp.org/entries/Seifert-Van-Kampen.html. Accessed September 30, 2026

Version history

  1. v1Initial depositCurrentSep 30, 2026