{"id":"palomar/PALOMAR-2026-09-25-000004","url":"https://github.com/Arthur742Ramos/classical-svk-lean/tree/874680e16db88b4a41daadf56eafbac79fd2f748","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000004-v1.json","repo":"https://github.com/Arthur742Ramos/classical-svk-lean","tags":["math.AT","math.CT","msc:55Q05","msc:18B40","algebraic-topology","fundamental-groupoid","lean-formalization"],"score":0,"title":"Classical Seifert–van Kampen theorem for the fundamental groupoid","trust":"high","domain":"math.AT","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"math.AT","summary":"Proves that for every topological space X and open cover X = U ∪ V, the inclusion-induced square of Mathlib's ordinary continuous-path fundamental groupoids for U ∩ V, U, V, and X is a pushout in Cat. The statement retains all points as objects and assumes no basepoint, connectedness, or separation conditions. The proof uses continuous paths and endpoint-preserving homotopies, specializes an auxiliary preorder to the indiscrete relation, and proves a natural equivalence with Mathlib's ordinary fundamental groupoid. It constructs the categorical descent functor by path subdivision and proves…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Groupoids and Van Kampen's Theorem","identifier":"10.1112/plms/s3-17.3.385","relationship":"formalizes"},{"title":"The Directed Van Kampen Theorem in Lean","identifier":"10.4230/LIPIcs.ITP.2024.8","relationship":"adapts"}]}