Basic constructions
Hatcher §1.1 (pages 25–38). This is the project's first completed section. Its twenty-two explicit roadmap nodes comprise eighteen local formalizations and four pinned Mathlib-backed nodes.
Paths and homotopy
Paths in a space X with fixed endpoints, taken up to homotopy, compose; loops
at a basepoint x₀ therefore form a group π₁(X, x₀), and a path between
basepoints induces an isomorphism between the groups it joins. Each opening
result now has its own node, including the local wrappers needed to match
Hatcher's affine formula and path-concatenation convention.
Hatcher, Example 1.1 (page 25). Two paths in ℝⁿ with the same endpoints
are homotopic relative to those endpoints by the straight-line homotopy
(1 - t) • p(s) + t • q(s).
The local definition Hatcher.affinePathHomotopy proves the more general
statement for paths in any real topological vector space. Its endpoint
conditions are part of Path.Homotopy, so the result is relative to the two
endpoints exactly as Hatcher requires.
Hatcher, Proposition 1.2 (page 26). Homotopy of paths relative to their endpoints is an equivalence relation.
This is exactly the pinned theorem Path.Homotopic.equivalence:
Equivalence (@Path.Homotopic X _ x₀ x₁). Mathlib also installs the resulting
IsEquiv instance, which makes endpoint-preserving homotopy classes available
as Path.Homotopic.Quotient x₀ x₁.
Hatcher, Proposition 1.3 (page 26). The path-homotopy classes of loops at
x₀ form a group with multiplication [p][q] = [p · q], where p · q
traverses p first and then q.
Mathlib defines FundamentalGroup X x as the endomorphism group of x in the
fundamental groupoid and installs its Group instance in
Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean.
Categorical composition uses the convention opposite to Hatcher's displayed
product, so the local abbreviation Hatcher.PathConcatenationGroup takes the
opposite group. The theorem
Hatcher.PathConcatenationGroup.fromPath_trans then states exactly
fromPath (p.trans q) = fromPath p * fromPath q.
Dependencies
Hatcher, Example 1.4 (page 27). A nonempty convex subset of ℝⁿ has
trivial fundamental group.
The pinned protected theorem Convex.contractibleSpace says that a nonempty
convex set in a real topological vector space is a ContractibleSpace.
Mathlib's instance SimplyConnectedSpace.ofContractible then makes it simply
connected, and the Subsingleton (FundamentalGroup X x) instance in
Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean makes
every based loop class equal to the identity.
The frontmatter tracks the exact contractibility theorem. Pinned Mathlib has no single named declaration whose statement is Hatcher's final group-theoretic sentence; the result is the checked composition of these declarations and instances.
Dependencies
Hatcher, Proposition 1.5 (page 28). A path h from x₀ to x₁ induces
an isomorphism βₕ : π₁(X, x₁) ≃* π₁(X, x₀) by conjugating a loop with h
and its reverse.
The pinned definition FundamentalGroup.fundamentalGroupMulEquivOfPath sends
a path h : Path x₀ x₁ to an equivalence
FundamentalGroup X x₀ ≃* FundamentalGroup X x₁. Hatcher's displayed
orientation is therefore represented by applying the definition to h.symm,
or equivalently by taking the inverse of the equivalence associated to h.
Dependencies
Hatcher, Proposition 1.6 (page 28). A space is simply connected if and only if every pair of points is joined by a unique path-homotopy class.
This is exactly the pinned theorem simply_connected_iff_unique_homotopic:
SimplyConnectedSpace X ↔ Nonempty X ∧
∀ x y : X, Nonempty (Unique (Path.Homotopic.Quotient x y)).
The explicit Nonempty X conjunct prevents the uniqueness condition from
holding vacuously. Mathlib also provides
simply_connected_iff_paths_homotopic', the equivalent formulation with an
explicit PathConnectedSpace X hypothesis and a proof that every two paths
with common endpoints are homotopic.
Dependencies
The circle
The section's real content is the computation π₁(S¹) ≅ ℤ. Hatcher compares
loops in S¹ with paths in ℝ along p(s) = (cos 2πs, sin 2πs), and needs
only that this map is a covering.
Hatcher's proof of Theorem 1.7 runs along p : ℝ → S¹,
p(s) = (cos 2πs, sin 2πs), and needs only that p is a covering map. He
verifies this directly (page 29): every open arc of S¹ is evenly covered.
This node supplies the same fact for Mathlib's Circle, the unit circle in ℂ.
Mathlib already has AddCircle.isCoveringMap_coe, that the quotient
ℝ → AddCircle T is a covering map, and AddCircle.homeomorphCircle', a
homeomorphism AddCircle (2 * π) ≃ₜ Circle. Composing a covering map with a
homeomorphism is again a covering map, so the work is assembling the two and
fixing the resulting map's normalization so that the generator of the deck
group is the loop of degree one.
Hatcher does not state this as a numbered result; it is the bridge from his
concrete p to the Mathlib formulation, which is why its origin is bridged
rather than cited.
Formalized in Hatcher/Circle/Covering.lean as
Hatcher.Circle.isCoveringMap_expMap, with Hatcher.Circle.expMap the
period-one map itself. The file also proves Hatcher.Circle.expMap_eq_one,
that the fibre over the basepoint is exactly ℤ. That is the normalization
this node promised: a loop lifting to a path from 0 to n has winding number
n with no factor of 2 * π to divide out, which is what
winding number consumes.
Every loop then lifts to a path in ℝ starting at 0 and ending at an
integer, and that integer is unchanged by path homotopy because homotopies lift
too. Mathlib supplies both lifting facts as IsCoveringMap.liftPath and
IsCoveringMap.liftHomotopy with monodromy_theorem, so the invariant can be
defined directly.
Given a loop f in S¹ based at 1, lift it to the unique path f̃ in ℝ
starting at 0. Since p(f̃(1)) = f(1) = 1, the endpoint f̃(1) is an integer.
That integer is the winding number of f.
It is well defined on homotopy classes: a path homotopy between loops lifts to
a path homotopy between their lifts, and the endpoint of a path homotopy is
constant, so homotopic loops have equal winding numbers. Mathlib supplies both
halves — IsCoveringMap.liftPath with its uniqueness, and
IsCoveringMap.liftHomotopy together with monodromy_theorem — so this node
is the descent of the endpoint map to π₁, not a lifting argument from
scratch.
The result is a group homomorphism π₁(S¹, 1) →* Multiplicative ℤ, or
equivalently an additive map after unfolding π₁; the exact Lean spelling is
part of this node. Hatcher works with the uniqueness of n rather than naming
a map, so this construction is bridged.
Formalized in Hatcher/Circle/WindingNumber.lean as
Hatcher.Circle.windingNumber, a MonoidHom into Multiplicative ℤ.
Mathlib's IsCoveringMap.monodromy supplied more than expected: it is already
defined on homotopy classes, so no well-definedness argument was needed. The
remaining additivity step is formalized using
Hatcher.Circle.monodromy_translate: moving the starting lift by a point of
the fibre moves the endpoint by the same amount. That theorem follows from
uniqueness of lifts, using that s ↦ s + n is a deck transformation of
expMap.
Dependencies
The loop ωₙ(s) = (cos 2πns, sin 2πns) realizes each integer, and comparing an
arbitrary lift with the linear path s ↦ ns shows the winding number is
faithful. That is the theorem.
Hatcher, Theorem 1.7 (page 29). π₁(S¹) is infinite cyclic, generated by
the class of the loop ω(s) = (cos 2πs, sin 2πs) based at (1, 0).
Equivalently, the winding number is an isomorphism
π₁(S¹, 1) ≅ ℤ. Both directions are short once lifting is available.
Surjectivity: the path ω̃ₙ(s) = ns in ℝ runs from 0 to n and projects to
the loop ωₙ(s) = (cos 2πns, sin 2πns), so ωₙ has winding number n.
Injectivity: if f has winding number n, then f̃ and ω̃ₙ are paths in ℝ
with the same endpoints, hence homotopic by the linear homotopy
(1 − t)f̃ + t ω̃ₙ; composing that homotopy with p shows f ≃ ωₙ. So the
class of f is determined by its winding number.
This is the project's main target. Nothing in the pinned Mathlib computes
π₁ of the circle, although every ingredient above is present.
Formalized in Hatcher/Circle/FundamentalGroup.lean. The node's named
declaration is Hatcher.Circle.isCyclic_fundamentalGroup, which asserts
Hatcher's actual proposition, that the group is cyclic; the companion
infinite_fundamentalGroup supplies "infinite". Both are read off
Hatcher.Circle.fundamentalGroupEquivInt, the MulEquiv from
FundamentalGroup Circle 1 onto Multiplicative ℤ, which is the data
witnessing the theorem. Hatcher's generator is Hatcher.Circle.loopOfInt 1,
and windingNumberFun_loopOfInt_one records that its winding number is one.
The split matters for the audit: the isomorphism is a def, so naming it in
lean: while declaring the node a theorem is a kind mismatch. The
proposition is what the source states, so the proposition is what the node
names.
Surjectivity is Hatcher's ω̃ₙ verbatim: the path s ↦ ns in ℝ is its own
lift, so ωₙ has winding number n. Injectivity uses that ℝ is
contractible, hence simply connected, via Mathlib's
SimplyConnectedSpace.ofContractible, so two lifts sharing both endpoints are
homotopic; projecting that homotopy down identifies the loops.
One wrinkle worth recording for later nodes: projecting a homotopy of lifts
lands in Path (expMap 0) (expMap c), not Path 1 1. Those types differ
because expMap 0 = 1 holds propositionally but not definitionally, so the
final step transports along Path.cast. The same transport will recur wherever
a lift is pushed back down.
Dependencies
Mathlib's product construction for fundamental groupoids, together with the circle computation above, supplies Proposition 1.12 and Example 1.13.
Consequences
The circle computation first rules out a retraction D² → S¹; Brouwer's
theorem is the direct consequence of that obstruction.
There is no continuous r : D² → S¹ restricting to the identity on S¹.
Hatcher's proof is direct. A nontrivial loop in S¹ becomes nullhomotopic
after inclusion into the convex disc. Composing that nullhomotopy with a
putative retraction would make the original loop nullhomotopic in S¹, a
contradiction.
Hatcher gives this argument inside the proof of Theorem 1.9 on page 32 rather
than as a numbered result, so its origin is bridged. Proposition 1.17 on
page 36 later repackages the same obstruction using the injectivity of the
homomorphism induced by a retract. This node keeps the earlier path-level
argument because it is the route Hatcher actually uses for Brouwer.
Mathlib has convexity of the disc and contractibility of convex sets, so
π₁(D²) = 0 is available and does not need its own node.
Formalized in Hatcher/Disc/NoRetraction.lean as
Hatcher.Disc.not_exists_retraction, with D² taken as
Metric.closedBall (0 : ℂ) 1 and the boundary inclusion as
Hatcher.Disc.incl.
The Lean proof follows Hatcher's direct route on path classes: the boundary
loop becomes nullhomotopic once pushed into the disc, and applying the
retraction to that homotopy would make the winding-one loop nullhomotopic in
S¹.
Dependencies
Hatcher, Theorem 1.9 (pages 31–32). Every continuous h : D² → D² has a
fixed point.
If h(x) ≠ x for every x, define r(x) to be the point where the ray from
h(x) through x meets S¹. This is continuous, and it fixes S¹
pointwise, so it is a retraction of D² onto S¹. No such retraction exists,
so h has a fixed point.
The formalization work is almost entirely in the construction of r and its
continuity: the ray-intersection point is given by an explicit formula whose
denominator is nonzero exactly because h(x) ≠ x. The topological content is
already discharged by the no-retraction node.
Brouwer's fixed point theorem is not in the pinned Mathlib in any dimension.
The general case comes from homology in
Corollary 2.15;
this node is only the two-dimensional case Hatcher proves from π₁.
Formalized in Hatcher/Disc/Brouwer.lean as
Hatcher.Disc.exists_fixed_point.
Dependencies
Separately, the nonvanishing of winding number applied to loops traced by a polynomial on circles of growing radius gives a topological proof of a result Mathlib already knows by other means.
Hatcher, Theorem 1.8 (page 31). Every nonconstant polynomial with complex
coefficients has a root in ℂ.
Suppose p(z) = zⁿ + aₙ₋₁zⁿ⁻¹ + ⋯ + a₀ has no root. For each radius r,
normalize by the nonzero value p(r): set
qᵣ(s) = p(r e^{2πis}) / p(r), then take the based loop
s ↦ qᵣ(s) / |qᵣ(s)| in S¹. As r varies these loops are homotopic; at
r = 0 the loop is constant, so every one is nullhomotopic. For r > 1
larger than the sum of the lower coefficients' norms, Hatcher deforms
p(z) to zⁿ through
pₜ(z) = zⁿ + t(aₙ₋₁zⁿ⁻¹ + ⋯ + a₀). The required estimate says pₜ has no
zero on the circle |z| = r, so the associated loop is homotopic to
s ↦ e^{2πins}, whose winding number is n. Hence n = 0 and p is
constant.
This result is already in Mathlib, as Complex.exists_root and the
Complex.isAlgClosed instance in
Analysis/Complex/Polynomial/Basic.lean, proved by Liouville's theorem. This
node formalizes Hatcher's topological proof instead. It is a source target and
a second proof, not new coverage, and the
coverage contract records that. mathlib: true
is deliberately not set because this node promises Hatcher's proof rather than
an alias to the existing Mathlib theorem.
Formalized in Hatcher/Applications/FundamentalTheoremAlgebra.lean as
Hatcher.exists_root_of_degree_pos. The support module
Hatcher/Circle/Normalize.lean packages radial projection and based-loop
homotopies for nonvanishing complex families.
Dependencies
Induced homomorphisms
The closing part of the section turns to maps between spaces. The product formula immediately computes the torus. The higher-sphere calculation rests on a subdivision lemma reused by §1.2 as the surjectivity step in van Kampen.
Hatcher, Proposition 1.12 (page 34). Projection onto the factors gives an
isomorphism
π₁(X × Y, (x, y)) ≃* π₁(X, x) × π₁(Y, y).
Formalized as Hatcher.fundamentalGroupProdEquiv in
Hatcher/FundamentalGroup/Product.lean. Its forward map takes a product loop
to its two coordinate loops, and its inverse forms the pointwise product of
two loops. The Lean statement does not require path-connectedness because it
works at fixed basepoints and is therefore slightly stronger than Hatcher's
ambient hypothesis.
Dependencies
Hatcher, Example 1.13 (page 34). The fundamental group of
S¹ × S¹ is isomorphic to ℤ × ℤ. Under this isomorphism, (m, n)
corresponds to the loop ωₘₙ(s) = (ωₘ(s), ωₙ(s)).
Formalized as Hatcher.torusFundamentalGroupEquiv in
Hatcher/FundamentalGroup/Product.lean. The companion theorems
torusFundamentalGroupEquiv_prod_loopOfInt and
torusFundamentalGroupEquiv_symm_apply record both directions of Hatcher's
loop formula.
Dependencies
Hatcher, Lemma 1.15 (page 35). If X is the union of path-connected open
sets Aα each containing the basepoint x₀, and each intersection Aα ∩ Aβ
is path-connected, then every loop in X at x₀ is homotopic to a product of
loops each contained in a single Aα.
The proof subdivides the interval by a Lebesgue-number argument so that each
subinterval maps into some Aα, then uses path-connectedness of the pairwise
intersections to join each subdivision point back to x₀ inside the
intersection of the two neighbouring sets.
This is the surjectivity argument in the van Kampen theorem. The §1.2 roadmap reuses this statement directly in the cover-map surjectivity node.
Mathlib PR #28246
contains
Path.Homotopic.exists_loops_homotopic_concat_of_open_cover, explicitly
documented as Hatcher's Lemma 1.15. The local proof is adapted from that open
PR for the pinned Mathlib revision and keeps the PR's copyright and Apache 2.0
license notice.
Formalized in Hatcher/Sphere/LoopInOpenCover.lean as
Hatcher.loop_homotopic_prod_of_isOpenCover.
Hatcher, Proposition 1.14 (page 35). π₁(Sⁿ) = 0 for n ≥ 2.
Cover Sⁿ by two open sets A₁ and A₂, each the complement of a point and
so homeomorphic to ℝⁿ. Their intersection is homotopy equivalent to
Sⁿ⁻¹, which is path-connected precisely when n ≥ 2. By the
open cover lemma, every loop is homotopic to a product
of loops each lying in A₁ or in A₂; each of those is nullhomotopic because
ℝⁿ is simply connected. Hence every loop in Sⁿ is nullhomotopic.
The hypothesis n ≥ 2 enters exactly once, at path-connectedness of
A₁ ∩ A₂, and it is sharp: π₁(S¹) ≅ ℤ.
Mathlib has SimplyConnectedSpace and the contractibility of ℝⁿ but no
instance for spheres; the only SimplyConnectedSpace mentions near spheres are
the proof_wanted statements of the Poincaré conjecture in
Geometry/Manifold/PoincareConjecture.lean, which are unrelated.
Mathlib PR #28246
now supplies EuclideanSphere.simplyConnectedSpace and a corresponding
instance, using the same open-cover route. The local proof is adapted from that
open PR for the pinned Mathlib revision and keeps the PR's copyright and Apache
2.0 license notice.
Formalized in Hatcher/Sphere/SimplyConnected.lean as
Hatcher.Sphere.simplyConnectedSpace, together with a matching instance.
Hatcher, Corollary 1.16 (page 36). Euclidean two-space is not
homeomorphic to Euclidean n-space when n ≠ 2.
Formalized as Hatcher.not_nonempty_homeomorph_euclideanTwo in
Hatcher/Euclidean/Dimension.lean. A hypothetical homeomorphism is translated
to fix the origin and then restricted to the punctured spaces. For dimensions
at least three, radial decomposition retracts the punctured spaces onto their
unit spheres; the two-dimensional sphere is a circle with nontrivial
fundamental group, while the higher sphere is simply connected. Dimension one
is separated by path connectedness of the punctured plane and the intermediate
value theorem on the punctured line. Dimension zero is a cardinality edge
case.
Dependencies
Borsuk–Ulam combines both halves of the section: the equator of S² bounds a
disc, so an odd map S² → S¹ restricted to it is simultaneously nullhomotopic
and of odd winding number.
Hatcher, Theorem 1.10 (pages 32–33). For every continuous f : S² → ℝ²
there is a point x ∈ S² with f(x) = f(−x).
Suppose not, and set g(x) = (f(x) − f(−x)) / |f(x) − f(−x)|, a map
S² → S¹ with g(−x) = −g(x). Restrict g to the equator S¹ ⊆ S² and call
the resulting loop η. Because η is odd, its winding number is odd, in
particular nonzero, so η is not nullhomotopic. But the equator bounds a disc
in S², over which η extends, so η is nullhomotopic. Contradiction.
Hatcher obtains the nullhomotopy directly because the equator bounds a
hemisphere disc. The current DAG instead routes this step through
simple connectivity of S². That is a valid but
strictly stronger Lean route, not an attribution to Hatcher's proof. The other
dependency is the circle computation: proving an
odd loop has odd winding number carries the real formalization cost, since its
lift must satisfy η̃(s + 1/2) = η̃(s) + (2k+1)/2.
Borsuk–Ulam is not in the pinned Mathlib in any dimension.
Formalized as Hatcher.Sphere.exists_eq_neg in
Hatcher/Sphere/BorsukUlam.lean. The implementation replaces the coordinate
equator by an arbitrary path from x to -x followed by its antipodal image;
this avoids coordinate bookkeeping while preserving Hatcher's odd-winding
obstruction.
Hatcher, Corollary 1.11 (page 33). If the two-sphere is the union of three closed sets, at least one of those sets contains a pair of antipodal points.
Formalized as Hatcher.Sphere.exists_antipodal_pair_of_three_closed_sets in
Hatcher/Sphere/AntipodalCover.lean. The proof applies Borsuk–Ulam to the map
whose coordinates are the distances to the first two closed sets. Equal
distances at x and -x either put both points in one of those sets, or force
both into the third set by the covering hypothesis.
The distance function is totalized for the empty-set case because Mathlib
defines Metric.infDist x ∅ = 0; the theorem itself retains Hatcher's three
closed-set statement.
Dependencies
The section also records the fundamental group's invariance under homotopy equivalence, beginning with the special case of retracts.
Hatcher, Proposition 1.17 (page 36). If a space X retracts onto A,
the inclusion-induced homomorphism π₁(A, a) →* π₁(X, a) is injective. If
A is a deformation retract of X, that homomorphism is an isomorphism.
Formalized in Hatcher/VanKampen/WedgeFundamentalGroup.lean. The theorem
Hatcher.fundamentalGroupMap_injective_of_retraction proves the first clause
from continuous maps A → X and X → A whose composite on A is the
identity. The definition
Hatcher.fundamentalGroupMulEquivOfDeformationRetract adds a homotopy from
the identity on X to the inclusion followed by the retraction and produces
the equivalence in the second clause. Its companion application theorem
records that the forward homomorphism is induced by inclusion.
Hatcher, Proposition 1.18 (page 37). A homotopy equivalence
e : X ≃ₕ Y induces an isomorphism
π₁(X, x) ≃* π₁(Y, e(x)) at every basepoint x.
Formalized as Hatcher.fundamentalGroupMulEquivOfHomotopyEquiv in
Hatcher/VanKampen/WedgeFundamentalGroup.lean. It is obtained from Mathlib's
equivalence of fundamental groupoids and records that the forward map is
exactly the homomorphism induced by e.toFun.
The companion definition
Hatcher.fundamentalGroupMulEquivOfHomotopyEquivOfEq transports the target
basepoint along a supplied equality, which is the form used by later
deformation-retract arguments.
Hatcher, Lemma 1.19 (page 37). Let H be a homotopy from f : X → Y
to g : X → Y, and let h(t) = H(t, x) be the path traced by a basepoint
x. Then the induced maps satisfy f_* = β_h ∘ g_*, where β_h changes
basepoint from g(x) back to f(x).
Formalized as Hatcher.fundamentalGroupMap_eq_basepointChange_comp in
Hatcher/VanKampen/WedgeFundamentalGroup.lean. The proof specializes
Mathlib's natural isomorphism between the fundamental-groupoid functors of
homotopic maps. The inverse path equivalence in the statement is intentional:
Mathlib's path equivalence follows h from f(x) to g(x), while Hatcher's
β_h goes in the opposite direction.
These twenty-two explicit nodes cover the section's numbered results, named examples, and the intermediate circle and no-retraction constructions used by its proofs. See the coverage contract.