Open Research Index

Classical Seifert–van Kampen theorem for the fundamental groupoid

Arthur Freitas Ramos

Palomar Registrypalomar/PALOMAR-2026-09-25-000004Sep 25, 2026math.ATscore 0

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…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-25-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'