Van Kampen's theorem
Hatcher §1.2 (pages 40–55). The selected 67-node spine is completely formalized: free products, van Kampen, wedges, cell attachments, finite skeleta, and realization of groups as fundamental groups.
If X is covered by path-connected open sets Aα sharing the basepoint, and
the pairwise intersections are path-connected, then the inclusions induce a
surjection from the free product ∗α π₁(Aα) onto π₁(X). When the triple
intersections are path-connected too, the kernel is generated by the relations
identifying the two images of each loop in a pairwise intersection, so
π₁(X) ≅ ∗α π₁(Aα) / N (Theorem 1.20, page 43). The section first develops
free products of groups and closes with applications to cell complexes,
including π₁ of a wedge of circles and of a two-dimensional CW complex
presented by generators and relations.
The public theorem retains Hatcher's shared-basepoint group statement. Mathlib supplies indexed free products, normal closures, quotient groups, and an initial unit-square subdivision lemma, but not the topological theorem or Hatcher's required threefold-incidence refinement. A groupoid proof may be useful internally; it does not replace the source-facing result.
The cover presentation
The algebraic target is the indexed free product of the groups of the cover members, modulo the normal closure of the relations coming from pairwise intersections.
Fix an indexed family of subsets U i ⊆ X containing a common basepoint
x₀. Let G i = π₁(U i, x₀) and let
P = Monoid.CoprodI G be their indexed free product. The inclusions
U i ↪ X induce a canonical homomorphism
Φ : P →* π₁(X, x₀).
For each pair i,j and each loop class ω in U i ∩ U j, the two inclusion
maps give elements of G i and G j. Define the overlap relation
of_i(ω in U i) * of_j(ω in U j)⁻¹
in P, and let N be the normal closure of all such relations. The main
artifact is Hatcher.VanKampen.relationSubgroup; the same file should define
the supporting map Hatcher.VanKampen.coverMap.
This is the algebraic object occurring in Hatcher's Theorem 1.20. The general
cover cannot be represented by Monoid.PushoutI, which has only one common
amalgamating group.
Formalized in Hatcher/VanKampen/CoverGroupPresentation.lean. The same file
exports Hatcher.VanKampen.coverMap, the two overlap homomorphisms, and the
explicit overlap relators before taking their normal closure.
Dependencies
For Hatcher's open-cover presentation, every generator of the overlap-relation subgroup maps to the identity under the canonical cover map. Therefore
relationSubgroup ≤ MonoidHom.ker coverMap,
and coverMap descends to a homomorphism from the quotient free product to
π₁(X, x₀).
The main artifact is Hatcher.VanKampen.relationSubgroup_le_ker; the same file
should define the supporting map Hatcher.VanKampen.quotientCoverMap.
This is the formal-algebra inclusion in the kernel calculation. It should use
the universal properties of Monoid.CoprodI, Subgroup.normalClosure, and
QuotientGroup, without topological subdivision arguments.
Formalized in Hatcher/VanKampen/CoverMapRelations.lean. The file also proves
the individual relator calculation and exports the descended homomorphism
Hatcher.VanKampen.quotientCoverMap.
Hatcher's first clause is already geometrically available: the completed Lemma 1.15 node factors every loop into finitely many loops subordinate to the cover.
Hatcher, Theorem 1.20, first clause (page 43). Let X be the union of an
arbitrary indexed family of path-connected open sets U i, all containing
the basepoint x₀. If every pairwise intersection is path-connected, then the
canonical map
Φ : (∗ i, π₁(U i, x₀)) →* π₁(X, x₀)
is surjective.
Intended artifact: Hatcher.VanKampen.coverMap_surjective.
The proof should reuse the completed Lemma 1.15 node: split a loop into a
finite concatenation of loops lying in cover members, then take the
corresponding finite word in Monoid.CoprodI.
Formalized in Hatcher/VanKampen/CoverMapSurjective.lean. The proof represents
each factor loop in its cover member and inducts over the finite concatenation,
accounting for the reversed multiplication convention in the fundamental
group.
The kernel calculation
The difficult direction compares different cover factorizations of homotopic loops. The factorization data and elementary moves are kept explicit. A separate geometric node records Hatcher's perturbation of the initial grid so that no vertex requires a fourfold-intersection hypothesis.
Package Hatcher's factorization of a based loop as finite data: a finite sequence of cover indices, based loops whose ranges lie in the corresponding sets, and a path homotopy from their concatenation to the original loop. Its evaluation is the associated word in the indexed free product.
The main artifact is Hatcher.VanKampen.Factorization. Keeping the
factorization data explicit makes the elementary moves and the homotopy-grid
argument reviewable without hiding them behind choice functions.
Formalized in Hatcher/VanKampen/CoverFactorization.lean. Each factor is a
loop in the relevant cover-member subtype, so its support condition is encoded
in its type. Hatcher.VanKampen.Factorization.word evaluates the finite list
of factors in the indexed free product.
The list is multiplied in reverse order, matching Mathlib's composition
convention for FundamentalGroup.
The theorem Hatcher.VanKampen.Factorization.exists_of_word proves the
converse algebraic fact needed by the kernel calculation: every word in the
indexed free product is represented by some cover factorization.
Hatcher.VanKampen.Factorization.boundaryHomotopy chooses the endpoint-fixed
homotopy between the ambient concatenations of two factorizations representing
homotopic loops; this is the square decomposed by the later sweep argument.
Hatcher uses two elementary moves: combine adjacent factors lying in one
cover member, or reinterpret a factor lying in U i ∩ U j through the other
inclusion. Prove that each move preserves the image of the factorization word
in the quotient by the overlap-relation subgroup.
Intended artifact: Hatcher.VanKampen.factorization_quotient_eq_of_move.
The reflexive-transitive closure is packaged as
Hatcher.VanKampen.Factorization.Sweep; the theorem
Hatcher.VanKampen.factorization_quotient_eq_of_sweep proves quotient
invariance for an arbitrary finite sweep without requiring intermediate entry
lists to be realized by paths.
The move toolkit is closed under arbitrary list contexts, combines or splits
same-cover blocks in reverse-product order, and performs lists of
overlap-certified cover changes pointwise.
Formalized in Hatcher/VanKampen/FactorizationMoves.lean. Elementary moves
act on the geometric-order list of indexed factor classes. Combining adjacent
factors uses the reversed multiplication convention of FundamentalGroup,
while changing a cover label is killed by the corresponding overlap relator.
Let H be an endpoint-fixed homotopy of paths, and let an arbitrary indexed
family of open sets cover X. Given finite labeled subdivisions on the bottom
and top edges whose cells already map into their labels, subdivide the square
into finitely many labeled rectangles such that:
- each region maps under
Hinto its label's cover member; - the bottom and top rows are exactly the prescribed subdivisions; and
- at most three labeled regions meet at any vertex.
The construction is Hatcher.VanKampen.exists_coverDecomposition_atMostThree.
The explicit incidence bound is
Hatcher.VanKampen.StaggeredCoverGrid.interfaceIncidentCellCount_le_three;
Hatcher.VanKampen.IntervalSubdivision.card_incidentCells_le_two gives the
corresponding bound of two on the outer boundary.
For cover factorizations, Hatcher.VanKampen.Factorization.exists_staggeredCoverGrid
instantiates the boundary rows with the canonical factor lists.
A Lebesgue number gives uniformly small middle rectangles. Compactness gives collars on the prescribed bottom and top cells. Two fine horizontal meshes are then chosen to avoid the boundary vertices and each other, and alternated between the boundary rows. Adjacent rows therefore have disjoint interior vertex sets, which gives the three-region incidence bound. The separate sweep node turns this geometric grid into factorization moves.
Dependencies
Let an arbitrary indexed family of open subsets cover X, contain a shared
basepoint, and have path-connected members, pairwise intersections, and triple
intersections. If two cover factorizations represent homotopic based loops,
then their words have the same class modulo the overlap-relation subgroup.
Intended artifact: Hatcher.VanKampen.factorization_quotient_eq_of_homotopic.
Follow Hatcher's sweep argument using a cover-subordinate decomposition in which at most three regions meet at each vertex. Choose connector paths at vertices in the resulting double or triple intersections, then compare successive cuts by the elementary moves. A plain product grid is insufficient: four labels can meet at an interior vertex, which would add a hypothesis absent from Theorem 1.20.
Hatcher, Theorem 1.20, kernel clause (page 43). Under the full hypotheses,
including path-connected triple intersections, the kernel of the canonical
cover map Φ is exactly the normal subgroup generated by the pairwise-overlap
relations.
Intended artifact: Hatcher.VanKampen.ker_coverMap.
One inclusion is formal algebra: every overlap relation maps to the identity. For the reverse inclusion, compare a factorization of a nullhomotopic loop with the empty factorization using the homotopy-grid theorem.
Hatcher, Theorem 1.20 (page 43). Under the full open-cover hypotheses, the canonical map induces an isomorphism
((∗ i, π₁(U i, x₀)) / N) ≃* π₁(X, x₀),
with the orientation chosen consistently in Lean. Here N is the normal
closure of the overlap relations.
Intended artifact: Hatcher.VanKampen.quotientEquivFundamentalGroup.
The final proof is the group first isomorphism theorem after surjectivity and the kernel calculation. The public statement remains Hatcher's based-group theorem even if groupoid machinery is useful internally.
Sources
Let path-connected open subsets A and B cover X, contain the shared
basepoint x₀, and have path-connected intersection. The two inclusion maps
from π₁(A ∩ B, x₀) exhibit π₁(X, x₀) as the corresponding group pushout,
represented by Monoid.PushoutI over a two-element index type.
Intended artifact: Hatcher.VanKampen.pushoutEquivFundamentalGroup.
This is the two-set specialization stated immediately after Example 1.22. Its
proof identifies Mathlib's Monoid.PushoutI with the free-product quotient in
Theorem 1.20. It is not the representation of the arbitrary-cover theorem,
where each pair of cover members has its own intersection group.
Formalized in Hatcher/VanKampen/BinaryVanKampen.lean for a cover indexed by
Fin 2. The equivalence is proved to have the canonical pushout map as its
underlying homomorphism.
Draft Mathlib PR #41603 proves a broader groupoid/cosheaf theorem and is useful implementation prior art. It is generated, unreviewed, absent from the pinned revision, and not treated as Mathlib coverage here.
Wedges and cell complexes
The first application is the free-product formula for arbitrary well-pointed wedge sums.
Define the wedge of an arbitrary family of pointed spaces as the quotient of
Option (Σ i, X i) by the smallest equivalence relation identifying none
with every some ⟨i, x₀ i⟩, with the quotient topology and the class of none
as basepoint. Supply the inclusions of each summand and their continuity
lemmas. This convention makes the wedge of an empty family a one-point space.
Intended artifact: Hatcher.PointedWedge.
This project-authored representation follows Hatcher's Chapter 0 definition. Mathlib has no topological wedge construction in the pinned revision.
Formalized in Hatcher/VanKampen/PointedWedge.lean. The file also exports the
common basepoint, the canonical summand inclusions, their continuity, and the
basepoint-identification simp lemma.
Dependencies
Define Hatcher.WellPointedAt x₀ to mean that x₀ lies in an open subset
N equipped with a contraction to x₀ that fixes x₀ throughout. Express
the contraction on the subtype N using ContinuousMap.HomotopyRel, relative
to the singleton containing the chosen basepoint. This is the formal version
of Hatcher's hypothesis that the basepoint is a deformation retract of an open
neighborhood.
For a nonempty family of path-connected spaces X i with well-pointed
basepoints x₀ i, construct the standard cover W i of
Hatcher.PointedWedge X x₀. If q is the quotient map and N j is the chosen
neighborhood in the jth summand, require
q ⁻¹' W i = {none} ∪ {some ⟨j, x⟩ | j = i ∨ x ∈ N j}.
Prove that every W i is open, all contain the wedge point, and their union is
the whole wedge. Each W i must deformation retract onto the image of X i,
with a basepoint-preserving homotopy equivalence compatible with the canonical
summand inclusion. For i ≠ j, prove that W i ∩ W j deformation retracts to
the wedge point. Deduce the member, pairwise-intersection, and
triple-intersection path-connectivity hypotheses required by van Kampen.
Intended artifact: Hatcher.PointedWedge.exists_vanKampenCover.
The same development should handle the empty-family boundary case separately by
showing that Hatcher.PointedWedge X x₀ is a one-point, hence contractible,
space when the index type is empty. The cover theorem itself is scoped to a
nonempty index type, since an empty indexed family cannot cover the wedge
point.
This node owns the quotient-space elimination and continuity lemmas needed to define the cover and its simultaneous deformation homotopies. The final wedge fundamental-group theorem should consume this package rather than reconstruct the point-set topology.
Formalized across Hatcher/VanKampen/WellPointedWedgeCover.lean,
WellPointedWedgeNeckContraction.lean, and
WellPointedWedgeMemberDeformation.lean.
Sources
Hatcher, Example 1.21 (page 43). For an arbitrary family of path-connected pointed spaces whose basepoints are deformation retracts of open neighborhoods, the inclusions of the summands induce an isomorphism from the indexed free product of their fundamental groups to the fundamental group of their wedge.
Intended artifact: Hatcher.fundamentalGroupEquivPointedWedge.
Do not restrict the family to a finite index type. The well-pointed hypothesis is part of Hatcher's statement and makes the standard open cover of the wedge available to van Kampen.
Formalized in Hatcher/VanKampen/WedgeFundamentalGroup.lean, including the
empty-family case and the canonical formula on each free-product factor.
Sources
For an arbitrary index type ι, the fundamental group of the pointed wedge
of ι copies of the circle is the free group on ι:
π₁(∨ᵢ S¹) ≃* FreeGroup ι.
The equivalence is formalized as
Hatcher.fundamentalGroupEquivWedgeCircles. It specializes Hatcher's
well-pointed wedge calculation, uses the winding-number equivalence for each
circle, and identifies the resulting indexed coproduct of infinite cyclic
groups with FreeGroup ι.
The companion theorem
Hatcher.fundamentalGroupEquivWedgeCircles_inclusion_loopOfInt checks the
generators: the winding-n loop included from the ith circle maps to
FreeGroup.of i ^ n.
Mathlib supplies the abstract coproduct-and-pushout data in
HomotopicalAlgebra.AttachCells. This project now compares that data with an
explicit indexed cone quotient and formalizes Hatcher's strip-enlarged space,
binary cover, deformation retractions, and overlap cover. Together with the
binary-cover algebra, these interfaces prove both the 2-cell and higher-cell
clauses of Proposition 1.26. These are local formalizations, not existing
Mathlib coverage.
Let c : HomotopicalAlgebra.AttachCells.{u}
(TopCat.RelativeCWComplex.basicCell n) f, where X is path-connected, the
cell-index type is nonempty, and 1 < n. For a basepoint x₀ : X, a chosen
point s₀ : TopCat.diskBoundary n, and paths from x₀ to every attaching
point, construct Hatcher's auxiliary cover package for c.
Intended artifact: Hatcher.VanKampen.exists_cellAttachmentCover.
The result returns Nonempty (CellAttachmentCover c x₀ s₀ γ). This package
contains the strip-enlarged space Z, its strong deformation retraction onto
the indexed model of the target, the open cover A ∪ B, the strong deformation
retraction A → X, a contraction of B, and the pointed indexed cover of
A ∩ B by pieces homotopy equivalent to the disk boundary. It also records the
spine path from the overlap basepoint to the image of x₀ and the exact
basepoint-change equations induced by the lower retraction.
State the input using HomotopicalAlgebra.AttachCells for
TopCat.RelativeCWComplex.basicCell n. This node is the final integrator of the
geometric work shared by Proposition 1.26(a) and (b); it does not calculate
π₁(A ∩ B) or assert either final fundamental-group result. The empty-index
case is intentionally handled by a separate isomorphism rather than by adding
a dummy cell to the connected cover.
Dependencies
For Hatcher's auxiliary cover of an n-cell attachment, the path-connected
space A ∩ B is covered by open pieces indexed by the attached cells. Each
piece deformation retracts onto the corresponding attaching
(n-1)-sphere, and the maps from their fundamental groups jointly generate
π₁(A ∩ B).
Intended artifact:
Hatcher.VanKampen.attachmentIntersection_coverMap_surjective.
The two attachment nodes specialize this surjectivity statement. For n = 2,
they identify generators using the circle computation. For n > 2, they use
Proposition 1.14 to show that every source group, and hence the intersection
group, is trivial.
Hatcher, Proposition 1.26(a) (page 50). If Y is obtained from a
path-connected space X by attaching an arbitrary family of 2-cells, then
π₁(X) → π₁(Y) is surjective and its kernel is the normal closure of the
attaching loops, transported to the common basepoint. Hence π₁(Y) is the
corresponding quotient of π₁(X).
Intended artifact: Hatcher.fundamentalGroup_quotient_of_attachTwoCells.
The statement must expose the chosen basepoint paths but prove that the normal subgroup is independent of those choices, as Hatcher notes after the proposition.
Dependencies
Hatcher, Proposition 1.26(b) (pages 50–51). If Y is obtained from a
path-connected space X by attaching cells of one fixed dimension n > 2,
then inclusion induces an isomorphism π₁(X, x₀) ≃* π₁(Y, x₀).
Intended artifact: Hatcher.fundamentalGroupEquiv_of_attachCells_of_two_lt.
The same two-set model as in part (a) applies. The cover pieces of its
intersection now deformation retract onto (n-1)-spheres, whose fundamental
groups are trivial.
Dependencies
For every finite m ≥ 2, compose the equivalences induced by the successive
classical skeleton inclusions to identify the fundamental group of the
2-skeleton with that of the m-skeleton.
Intended main artifact:
noncomputable def Hatcher.ClassicalCW.fundamentalGroupEquiv_twoSkeleton_skeleton
{X : Type u} [TopologicalSpace X] [T2Space X]
(C : Set X) [Topology.CWComplex C] [PathConnectedSpace C]
(m : ℕ) (hm : 2 ≤ m)
(x₀ : Topology.CWComplex.skeleton C (2 : ℕ∞)) :
FundamentalGroup (Topology.CWComplex.skeleton C (2 : ℕ∞)) x₀ ≃*
FundamentalGroup (Topology.CWComplex.skeleton C (m : ℕ∞))
⟨x₀.1, Topology.CWComplex.skeleton_mono
(C := C) (Nat.cast_le.mpr hm) x₀.2⟩
Also prove an application lemma identifying this equivalence with
FundamentalGroup.map for the direct subtype inclusion. Induct from dimension
two. At each successor, use the standard-cell attachment supplied by the
classical bridge, apply the higher-cell fundamental-group equivalence, and
propagate path-connectedness to the next skeleton. The base case is the
identity equivalence, and all basepoint transports must be explicit.
Sources
Dependencies
Hatcher, Proposition 1.26(c) (pages 50–51). For a path-connected CW
complex X, inclusion of the 2-skeleton induces an isomorphism
π₁(X², x₀) ≃* π₁(X, x₀).
Intended artifact: Hatcher.fundamentalGroupEquiv_twoSkeleton.
State this using Mathlib's classical Topology.CWComplex and
CWComplex.skeleton. The induced homomorphism is an isomorphism because it is
both surjective and injective. For surjectivity, put the compact image of a
representative loop inside a bounded skeleton and use the finite-stage
equivalence. For injectivity, do the same with the compact image of a null
homotopy and use the finite-stage equivalence's application lemma. This is the
two-use compactness argument in Hatcher's proof.
Do not silently assume that the 2-skeleton is path-connected. That instance is an explicit prerequisite, and each finite-stage comparison transports the basepoint along the actual subtype inclusion.
The 2-skeleton argument uses Mathlib's classical CW-complex API, while the
attachment theorem uses its categorical API. The bridge between them is
supplied by a bounded Appendix support chain:
it compares the two cell shapes, proves the successor-skeleton quotient, and
packages the inclusion as AttachCells. Separate connectivity and
finite-stage nodes discharge the path-connectedness hypotheses needed during
the induction rather than assuming them silently.
The presentation-complex branch is complete. Its support roadmap separates the formalized pointed-wedge mapping and connectivity interfaces, zero- and one-cell models, arbitrary relator family, quotient calculation, and finite CW-sequence assembly. The cyclic quotient calculation and concrete single-two-cell example are formalized as well.
For every group G, produce a generator type, a family of relators in the free
group on those generators, and a multiplicative equivalence from the resulting
PresentedGroup to G.
Formalized as Hatcher.exists_presentedGroup_equiv in
Hatcher/VanKampen/PresentedGroup.lean. The theorem chooses G itself as the
generator type and the kernel of free-group evaluation as the relator set.
Hatcher takes all elements of G as generators and a generating family for
the kernel of the evaluation map as relators. Mathlib supplies
PresentedGroup, but the required arbitrary-group equivalence is a theorem to
prove rather than an existing declaration.
Dependencies
Hatcher, Corollary 1.28 (page 52). For every group G, there is a
two-dimensional cell complex X_G with π₁(X_G) ≃* G.
Intended artifact: Hatcher.exists_twoDimensionalCWComplex_fundamentalGroupEquiv.
The source-facing Lean statement should be equivalent to:
theorem exists_twoDimensionalCWComplex_fundamentalGroupEquiv
(G : Type u) [Group G] :
∃ (X : TopCat.{u}) (x₀ : X) (c : TopCat.CWComplex X),
(∀ γ : HomotopicalAlgebra.RelativeCellComplex.Cells c, γ.j ≤ 2) ∧
Nonempty (FundamentalGroup X x₀ ≃* G)
Use the generator type of a presentation of G to form a wedge of circles,
then attach one 2-cell for each relator. The statement is for arbitrary groups,
not only finitely presented groups.
This corollary is algebraic once the presentation-complex realization theorem
is available: choose the presentation supplied by
Hatcher.exists_presentedGroup_equiv, realize it geometrically, and compose
the two group equivalences. It should not reconstruct the wedge or attachment
geometry itself.
Sources
Examples 1.22–1.25, Corollary 1.27, and the geometric claims in Example 1.29 are deferred. They require graph, knot-complement, wild-space, or surface models beyond the selected van Kampen spine.