The fundamental group
Hatcher's Chapter 1 (pages 21–96) builds the first algebraic invariant of a
space and the first real computations with it. Loops at a basepoint, taken up
to homotopy, form a group π₁(X, x₀); a continuous map induces a homomorphism;
homotopy equivalences induce isomorphisms. The invariant only earns its keep
once something can be computed with it, and the chapter's three sections supply
in turn the seed computation, a general gluing tool, and the structural theory
that explains both.
Basic constructions sets up π₁ and computes
π₁(S¹) ≅ ℤ by lifting loops along ℝ → S¹. That one calculation immediately
yields the fundamental theorem of algebra, Brouwer's fixed point theorem for
the disc, and Borsuk–Ulam for S².
Van Kampen's theorem computes π₁ of a space glued
from pieces whose fundamental groups are known, as a free product of the pieces
amalgamated over their intersections. It turns the circle computation into
computations for wedges, the cube graph, and two-dimensional cell complexes.
The general theorem that connected graphs have free fundamental group belongs
to Hatcher §1.A, which is outside the main-line scope here.
Covering spaces recasts both: subgroups of
π₁(X) correspond to covering spaces of X, and the loop-lifting argument
behind the circle computation becomes an instance of a general classification.
Mathlib has FundamentalGroup, FundamentalGroupoid, monodromy, and several
of Hatcher's §1.3 lifting results. It does not contain the circle computation,
van Kampen theorem, universal-cover construction, or classification and deck
spine as a whole. Every formalizable leaf in the selected §1.1, §1.2, and
§1.3 spines is complete locally or backed by an exact declaration in the
pinned Mathlib. The examples and reconstruction results outside those selected
spines remain explicitly deferred.