Chapter 1. The Fundamental Group
FC07 — Hatcher, Algebraic Topology.
This chapter contains 21 definitions, 9 theorems, 21 propositions, 3 lemmas, 4 corollaries, 29 examples, 6 constructions and 1 other statements.
Of the 94 statements checked against Lean, 44 are formalized somewhere and 50 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 50 | 53% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 28 | 30% | Mathlib states and proves it. |
| in another Lean project | 16 | 17% | Some other Lean development has it; using it means porting that code. |
| checked in total | 94 |
- Canonical source block: FC07 Hatcher, Chapter 1,
FC07-C01-U001–FC07-C01-U094, exactly 94 contiguous rows extracted from FC07 — Hatcher, Algebraic Topology throughagent-memory. - Search order followed the corpus plan: project source first at
A=3b2239e161592472b34e02ad3b7da308f9ce7280, then pinned MathlibP=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean 4.33.0), current upstream MathlibH=633b366493a76df88a2bff099ed0cbf711a59ec9(Apache-2.0, Lean 4.34.0-rc2), current/open work and indexed searches, Reservoir/packages, broad GitHub/discoverable Lean, and local reference mirrors. Noproject-existingC01 owner was found. - Every explicit Mathlib path/declaration cited by the C01 table was rechecked in the project checkout at exact pin
P; all 39 distinctMathlib/...lean::declarationreferences resolve there, and a batch Lean#checkof the credited pinned declarations succeeds under that checkout. The TauCeti and sphere-six target paths were likewise rechecked atT=2db3a983be93975cbf1d54bcc7d6ae1b97830856andR=895c0a0661501581c34d42fea3c553d4f0ee43b1. - The previously promoted FC02 Munkres fundamental-group, covering-classification, and graph audits were retrieved through
agent-memoryand reused where their source statements coincide. Their declaration/path checks were refreshed only where FC07’s unit is stricter or TauCeti has since acquired a sharper owner. - TauCeti was refreshed to upstream
T=2db3a983be93975cbf1d54bcc7d6ae1b97830856(Apache-2.0, Lean 4.34.0-rc2, Mathlib5fcc6656691ed31965746c369f41fa75e567ac9d). It supplies source-shaped product/sphere π₁, universal-cover classification, subgroup realization, monodromy/index, deck/regular-cover, and quotient-action results. Because its Mathlib/toolchain are post-pin, every credited TauCeti route isreference-port. deancureton/sphere-six-complex@895c0a0661501581c34d42fea3c553d4f0ee43b1(Apache-2.0, Lean 4.34.0-rc1) is reused for deformation-retract/homotopy-equivalence data in U026 and remainsreference-port.harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838(MIT, Lean/Mathlib 4.32.0, Mathlib81a5d257c8e410db227a6665ed08f64fea08e997) supplies Brouwer fixed point for U017 as a stronger theorem, hencereference-port. Broad searches still found no completed Borsuk–Ulam owner for U018/U019.Arthur742Ramos/ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645is MIT, Lean 4.33.0, and pins exactlyP; its targeted circle module builds at that revision. It proves anAddCirclewinding classification, but U013 names Hatcher’s literal Euclidean cos/sin loop and no checked bridge to that exact generator was found, so U013 remains unmatched despite package compatibility. Its computational-path Bass–Serre API is also not conflated with Hatcher’s topological KΓ construction.finite-graph-fundamental-group@dd57e3ab8bc5a7042fcc5498e778b008d87ac032andGraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250care Apache-2.0, Lean/Mathlib 4.32.0 reference ports whose targeted builds were already verified in FC02. They give finite graph realization/tree contraction/free-basis/Schreier results. Hatcher’s graph rows are stated for arbitrary 1-dimensional CW graphs; finite specializations are therefore retained as adjacent evidence rather than promoted unless the whole source row is owned.- Pinned Mathlib’s
FreeGroupBasisplusEquiv.ofFreeGroupEquivis sufficient for U031: any two basis index types of the same free group are equivalent, so rank is well-defined. PinnedsubgroupIsFreeOfIsFreeowns Nielsen–Schreier U077 directly. - U032 is not promoted from the open van-Kampen work or ComputationalPaths pushout SVK: Hatcher’s row is the full arbitrary-cover/triple-intersection theorem and must be owned as a bundle. The same rule blocks U033/U038 and the KΓ rows when only their algebraic pushout/HNN ingredients are formalized.
- U043–U061 are checked against the current TauCeti connected-cover stack. In particular, U046 combines pinned covering-map injectivity with TauCeti’s monodromy stabilizer/range theorem; U047 is
card_fiber_eq_index; U052–U054 are the subgroup-cover and pointed/unpointed classification equivalences; U058 is normality plus the normalizer/deck quotient; U061 combines Mathlib’s quotient-covering fundamental-group equivalence with TauCeti regularity and full-deck-group identification. - U062 remains unmatched deliberately: Mathlib’s standalone
ProperlyDiscontinuousSMulis a stronger compact-set notion under local compactness/T2 assumptions, whileIsQuotientCoveringMap.disjointbakes in quotient-map/orbit data. Neither declaration is exactly Hatcher’s bare local pairwise-disjoint-translate definition together with the free-action definition. - U078–U087 remain unmatched under source semantics. TauCeti defines K(G,1) through asphericity/higher homotopy and proves universal covers weakly contractible; Hatcher’s catalogue row explicitly requires a contractible universal cover. No checked Whitehead/CW bridge was found that turns those APIs into the complete source bundle, and concrete RP∞/lens/surface/knot/EG examples are not credited from generic ingredients.
- U092/U093 record Mathlib’s exact algebraic amalgamated-product/HNN constructions only as adjacent evidence: the units assert topological π₁(KΓ) computations, and no checked KΓ bridge was found.
N=2026-09-06denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics are applied uniformly.
Definition — path and homotopy of paths
A path in X is a continuous f:I→X. Two paths f_0,f_1 with the same endpoints are homotopic rel {0,1} when joined by a homotopy fixing both endpoints.
Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopy, Path.Homotopic — Homotopy rel endpoints is exactly Mathlib path homotopy; the endpoint constraints are built into the dependent path types.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 1.1
Linear Homotopies. Any two paths f_{0} and f_{1} in ℝ^{n} having the same endpoints x_{0} and x_{1} are homotopic via the homotopy f_{t} (s) = (1 - t) f_{0} (s) + t f_{1} (s). Continuity of the homotopy f_{t} as a map I × I → ℝ^{n} follows from continuity of f_{0} and f_{1} since the algebraic operations of vector addition and scalar multiplication in the formula for f_{t} are continuous.
Formalized. Mathlib/Topology/Homotopy/Affine.lean::ContinuousMap.Homotopy.affine — The affine homotopy is the straight-line homotopy between maps into a convex set, giving the stated linear path homotopy in Euclidean space.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.2
The relation of homotopy on paths with fixed endpoints in any space is an equivalence relation.
Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.equivalence — Mathlib proves path homotopy is an equivalence relation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/notation — homotopy class of a path
The homotopy class of a path f under endpoint-preserving path homotopy is denoted [f].
Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient, Path.Homotopic.Quotient.mk — The quotient type is exactly the set of path-homotopy classes and mk is the class map.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — product of paths
If f(1)=g(0), the product path f·g traverses f on the first half of I and g on the second half.
Formalized. Mathlib/Topology/Path.lean::Path.trans; Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient.trans — Path concatenation and the induced operation on homotopy classes are both native.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — loop, basepoint, and π₁ set
A loop at x_0 is a path with f(0)=f(1)=x_0; π₁(X,x_0) is the set of endpoint-preserving homotopy classes of loops at x_0.
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup, FundamentalGroup.fromPath, FundamentalGroup.toPath — The fundamental group is the loop-homotopy-class endomorphism group at the chosen basepoint.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.3
π_{1} (X, x_{0}) is a group with respect to the product [ f ] [ g ] = [ f · g ]
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.mul_def — The group law is induced by path concatenation (with Mathlib’s categorical composition order); identity and inverse are the constant loop and path reversal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — reparametrization of a path
A reparametrization of f is f∘φ for continuous φ:I→I with φ(0)=0 and φ(1)=1; it has the same homotopy class as f.
Formalized. Mathlib/Topology/Homotopy/Path.lean::Path.Homotopy.reparam — Every continuous endpoint-fixing reparameterization is explicitly homotopic rel endpoints to the original path.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — inverse path
For f from x_0 to x_1, the inverse path is f̄(s)=f(1−s), running from x_1 to x_0.
Formalized. Mathlib/Topology/Path.lean::Path.symm; Mathlib/Topology/Homotopy/Path.lean::Path.Homotopic.Quotient.symm — Path reversal and inverse on path classes are native and implement the inverse loop class.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 1.4
For a convex set X in ℝ^{n} with basepoint x_{0} ∈ X we have π_{1} (X, x_{0}) = 0, the trivial group, since any two loops f_{0} and f_{1} based at x_{0} are homotopic via the linear homotopy f_{t} (s) = (1 - t) f_{0} (s) + t f_{1} (s), as described in Example 1.1.
Formalized. Mathlib/Analysis/Convex/Contractible.lean::Convex.contractibleSpace; Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace.ofContractible — A nonempty convex subset of a real topological vector space is contractible, hence simply connected and has trivial fundamental group; this is stronger than the Euclidean convex example.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.5
The map β_{h}: π_{1} (X, x_{1}) → π_{1} (X, x_{0}) is an isomorphism.
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::fundamentalGroupMulEquivOfPath — A path between basepoints induces the standard conjugation/basepoint-change group isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.6
A space X is simply-connected iff there is a unique homotopy class of paths connecting any two points in X.
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::simply_connected_iff_unique_homotopic, simply_connected_iff_paths_homotopic — These are exactly the characterization by uniqueness of path-homotopy classes between any two points.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.7
π_{1} (S^{1}) is an infinite cyclic group generated by the homotopy class of the loop ω (s) = (cos 2 π s, sin 2 π s) based at (1, 0).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: π_{1} (S^{1}) is an infinite cyclic group generated by the homotopy class of the loop ω (s) = (cos 2 π s, sin 2 π s) based at (1, 0). Arthur742Ramos/ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645 (MIT, Lean/Mathlib exactly 4.33.0/P) proves topologicalPiOneEquivInt for Mathlib AddCircle and winding of its standard loop, but no checked bridge identifies Hatcher’s literal Euclidean cos/sin loop with that generator; the whole row is therefore not promoted. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — covering space
A covering space of X consists of a space X̃ and a map p:X̃→X such that for each x∈X there is an open neighborhood U for which p^{-1}(U) is a union of disjoint open sets, each mapped homeomorphically onto U by p.
Formalized. Mathlib/Topology/Covering/Basic.lean::IsCoveringMap — Mathlib’s covering-map structure gives local trivializations over discrete fibers, equivalent to evenly covered neighborhoods/sheets in the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — evenly covered neighborhood
For a covering map p:X̃→X, an open neighborhood U of x satisfying the covering-space decomposition condition is called evenly covered.
Formalized. Mathlib/Topology/Covering/Basic.lean::IsEvenlyCovered — The predicate explicitly records a neighborhood whose inverse image splits into disjoint sheets each mapped homeomorphically to the neighborhood.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.8
Every nonconstant polynomial with coefficients in ℂ has a root in ℂ
Formalized. Mathlib/Analysis/Complex/Polynomial/Basic.lean::Complex.exists_root — This is the fundamental theorem of algebra in the exact nonconstant-polynomial form needed.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.9
Every continuous map h: D^{2} → D^{2} has a fixed point, that is, a point x ∈ D^{2} with h (x) = x.
Formalized. harfe/fixed-point-theorems-lean4::FixedPointTheorems/brouwer.lean::brouwer_fixed_point — The external theorem proves Brouwer fixed point for every nonempty compact convex subset of a finite-dimensional real normed space, so the disk is an immediate specialization.
Searched: B=770940ddf9878cf61952ed53d910b92bca841838; MIT; Lean/Mathlib 4.32.0 (Mathlib 81a5d257c8e410db227a6665ed08f64fea08e997)
Theorem 1.10
For every continuous map f: S^{2} → {ℝ }^{2} there exists a pair of antipodal points x and - x in S^{2} with f (x) = f (- x).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every continuous map f: S^{2} → {ℝ }^{2} there exists a pair of antipodal points x and - x in S^{2} with f (x) = f (- x). Broad GitHub/Reservoir searches found only theorem statements/placeholders for Borsuk–Ulam, not a completed proof. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 1.11
Whenever S^{2} is expressed as the union of three closed sets A_{1}, A_{2}, and A_{3}, then at least one of these sets must contain a pair of antipodal points {x, - x }.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Whenever S^{2} is expressed as the union of three closed sets A_{1}, A_{2}, and A_{3}, then at least one of these sets must contain a pair of antipodal points {x, - x }. This corollary depends on the missing Borsuk–Ulam theorem; no separate checked owner was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1.12
π_{1} (X × Y) is isomorphic to π_{1} (X) × π_{1} (Y) if X and Y are path-connected.
Formalized. TauCeti/AlgebraicTopology/FundamentalGroup/Product.lean::FundamentalGroup.prodMulEquiv — Direct group isomorphism π₁(X×Y,(x,y)) ≃ π₁(X,x)×π₁(Y,y).
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Example 1.13
The Torus. By the proposition we have an isomorphism π_{1} (S^{1} {× } S^{1}) ≅ ℤ × ℤ. More generally, the n-dimensional torus, which is the product of n circles, has fundamental group isomorphic to the product of n copies of ℤ.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Torus/FundamentalGroup.lean::AddCircle.piFundamentalGroupMulEquiv — For an indexed product of additive circles, the theorem computes the fundamental group as the product of copies of ℤ; finite index gives ℤⁿ for the n-torus.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Construction — induced homomorphism on π₁
A map φ:(X,x_0)→(Y,y_0) induces φ_*:π₁(X,x_0)→π₁(Y,y_0) by [f]↦[φ∘f].
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map, FundamentalGroup.mapOfEq — A continuous based map induces the fundamental-group homomorphism, with mapOfEq transporting an explicitly identified target basepoint.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.14
π_{1} (S^{n}) = 0 if n ≥ 2.
Formalized. TauCeti/AlgebraicTopology/Sphere/SimplyConnected.lean::TauCeti.simplyConnectedSpace_sphere_euclideanSpace; pinned Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup, Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean::SimplyConnectedSpace — TauCeti proves Euclidean n-spheres simply connected for n≥2; the pinned simply-connected/fundamental-group equivalence gives the stated trivial π₁.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d; P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.34.0-rc2
Lemma 1.15
If a space X is the union of a collection of path-connected open sets A_{α} each containing the basepoint x_{0} ∈ X and if each intersection A_{α} ∩ A_{β} is path-connected, then every loop in X at x_{0} is homotopic to a product of loops each of which is contained in a single A_{α}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If a space X is the union of a collection of path-connected open sets A_{α} each containing the basepoint x_{0} ∈ X and if each intersection A_{α} ∩ A_{β} is path-connected, then every loop in X at x_{0} is homotopic to a product of loops each of which is contained in a single A_{α}. The open Mathlib van-Kampen work and existing groupoid APIs supply nearby generation machinery, but no checked theorem owns the source arbitrary open-cover loop-generation statement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 1.16
ℝ^{2} is not homeomorphic to ℝ^{n} for n ≠ 2
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: ℝ^{2} is not homeomorphic to ℝ^{n} for n ≠ 2 No searched declaration proves the dimension-distinguishing nonhomeomorphism argument as stated; sphere/fundamental-group ingredients cover only special cases. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1.17
If a space X retracts onto a subspace A, then the homomorphism i_{}: π_{1} (A, x_{0}) → π_{1} (X, x_{0}) induced by the inclusion i: A ↪ X is injective. If A is a deformation retract of X, then i_{} is an isomorphism.
Formalized. deancureton/sphere-six-complex::SphereSixComplex/Topology/EstablishedStrongDeformationRetracts.lean::SphereSixComplex.StrongDeformationRetraction, StrongDeformationRetraction.toHomotopyEquiv; pinned Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map — A retraction gives a left inverse on induced π₁ maps and hence injectivity. A deformation retraction supplies a homotopy equivalence, whose induced fundamental-group map is an isomorphism.
Searched: R=895c0a0661501581c34d42fea3c553d4f0ee43b1; P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.34.0-rc1
Comparison — group retractions and semidirect products
A group retraction ρ:G→H is a homomorphism onto H restricting to the identity on H; if H is normal then G is the direct product of H and kerρ, while otherwise the corresponding decomposition is called a semidirect product.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A group retraction ρ:G→H is a homomorphism onto H restricting to the identity on H; if H is normal then G is the direct product of H and kerρ, while otherwise the corresponding decomposition is called a semidirect product. Mathlib has semidirect-product and group-extension APIs, but no checked theorem packages the source retraction decomposition and the normal-subgroup direct-product refinement. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1.18
If φ: X → Y is a homotopy equivalence, then the induced homomorphism φ_{*}: π_{1} (X, x_{0}) → π_{1} { (Y, φ (x_{0})) } is an isomorphism for all x_{0} ∈ X.
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::FundamentalGroupoidFunctor.equivOfHomotopyEquiv; Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map — The fundamental-groupoid equivalence is built from the given homotopy equivalence and restricts at the basepoint to the induced π₁ isomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Lemma 1.19
If φ_{t}: X → Y is a homotopy and h is the path φ_{t} (x_{0}) formed by the images of a basepoint x_{0} ∈ X, then the three maps in the diagram at the right satisfy φ_{0 } = β_{h} φ_{1 }.
Formalized. Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean::FundamentalGroupoidFunctor.homotopicMapsNatIso, Path.Homotopic.map_trans_evalAt — A homotopy between maps gives the natural isomorphism whose basepoint component is the track of the basepoint; this is exactly conjugacy of the induced homomorphisms by that path.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/construction — free product of groups
The free product *αG_α consists of reduced finite words in nonidentity letters from the factors, adjacent letters coming from different factors; multiplication is concatenation followed by reduction.
Formalized. Mathlib/GroupTheory/Coprod/Basic.lean::Monoid.Coprod; Mathlib/GroupTheory/CoprodI.lean::Monoid.CoprodI.Word — The free product is represented by the coproduct of groups together with its alternating-word normal-form machinery.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — free group, basis, and rank
A free group is a free product of copies of ℤ. Its standard generators form a basis, every element has a unique reduced-word expression in their powers, and the cardinality of a basis is the rank; the rank is independent of the chosen basis.
Formalized. Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean::FreeGroupBasis, FreeGroupBasis.lift; Mathlib/GroupTheory/FreeGroup/GeneratorEquiv.lean::Equiv.ofFreeGroupEquiv — FreeGroupBasis gives the universal-property/basis representation; free-group words give reduced representatives; Equiv.ofFreeGroupEquiv proves isomorphic free groups have equivalent generator types, hence basis cardinality (rank) is intrinsic.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 1.20
If X is the union of path-connected open sets A_{α} each containing the basepoint x_{0} ∈ X and if each intersection A_{α} ∩ A_{β} is path-connected, then the homomorphism Φ: *{α} π{1} (A_{α}) → π_{1} (X) is surjective. If in addition each intersection A_{α} ∩ A_{β} ∩ A_{γ} is path-connected, then the kernel of Φ is the normal subgroup N generated by all elements of the form i_{α β} (ω) i_{β α} (ω)^{- 1} for ω ∈ π_{1} (A_{α} ∩ A_{β}), and hence Φ induces an isomorphism {π }_{1} (X) ≅ *{α} {π }{1} (A_{α}) / N.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If X is the union of path-connected open sets A_{α} each containing the basepoint x_{0} ∈ X and if each intersection A_{α} ∩ A_{β} is path-connected, then the homomorphism Φ: {α} π{1} (A_{α}) → π_{1} (X) is surjective. If in addition each intersection A_{α} ∩ A_{β} ∩ A_{γ} is path-connected, then the kernel of Φ is the normal subgroup N generated by all elements of the form i_{α β} (ω) i_{β α} (ω)^{- 1} for ω ∈ π_{1} (A_{α} ∩ A_{β}), and hence Φ induces an isomorphism {π }{1} (X) ≅ {α} {π }{1} (A{α}) / N. Open Mathlib PR #41603 contains a genuine groupoid van Kampen theorem, and ComputationalPaths has pushout SVK developments, but neither checked route owns Hatcher’s full arbitrary-cover/triple-intersection kernel theorem. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.21
Wedge Sums. In Chapter 0 we defined the wedge sum ∨{α} X{α} of a collection of spaces X_{α} with basepoints x_{α} ∈ X_{α} to be the quotient space of the disjoint union ∐{α} X{α} in which all the basepoints x_{α} are identified to a single point. Van Kampen’s theorem then implies that Φ: *{α} π{1} (X_{α}) → π_{1} (∨{α} X{α}) is an isomorphism, assuming that each X_{α} is path-connected, hence also each A_{α}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Wedge Sums. In Chapter 0 we defined the wedge sum ∨{α} X{α} of a collection of spaces X_{α} with basepoints x_{α} ∈ X_{α} to be the quotient space of the disjoint union ∐{α} X{α} in which all the basepoints x_{α} are identified to a single point. Van Kampen’s theorem then implies that Φ: **{α} π{1} (X_{α}) → π_{1} (∨{α} X*{α}) is an isomorphism, assuming that each X_{α} is path-connected, hence also each A_{α}. ComputationalPaths contains pushout/wedge-flavored SVK machinery, but no checked native topological wedge theorem realizes this exact source corollary. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.22
Let X be the graph shown in the figure, consisting of the twelve edges of a cube. The seven heavily shaded edges form a maximal tree T ⊂ X, a contractible subgraph containing all the vertices of X. Each A_{α} deformation retracts onto a circle, so π_{1} (X) is free on five generators, as claimed.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X be the graph shown in the figure, consisting of the twelve edges of a cube. The seven heavily shaded edges form a maximal tree T ⊂ X, a contractible subgraph containing all the vertices of X. Each A_{α} deformation retracts onto a circle, so π_{1} (X) is free on five generators, as claimed. GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c and finite-graph-fundamental-group@dd57e3ab8bc5a7042fcc5498e778b008d87ac032 compute free bases/ranks for finite graph realizations, but no declaration instantiates Hatcher’s specific cube graph and its five named independent cycles. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.23
For complements in ℝ^3: one circle has homotopy type S1∨S2 and fundamental group ℤ; two unlinked circles have fundamental group ℤ*ℤ; two linked circles have homotopy type S2∨(S1×S^1) and fundamental group ℤ×ℤ.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For complements in ℝ^3: one circle has homotopy type S1∨S2 and fundamental group ℤ; two unlinked circles have fundamental group ℤ*ℤ; two linked circles have homotopy type S2∨(S1×S^1) and fundamental group ℤ×ℤ. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.24
For coprime m,n>0, the torus knot K_{m,n} is z↦(zm,zn) on the standard torus. Its complement deformation retracts onto X_{m,n}, the union of the mapping cylinders of z↦z^m and z↦z^n, and π₁(ℝ3−K_{m,n})≅⟨a,b∣am=b^n⟩.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For coprime m,n>0, the torus knot K_{m,n} is z↦(zm,zn) on the standard torus. Its complement deformation retracts onto X_{m,n}, the union of the mapping cylinders of z↦z^m and z↦z^n, and π₁(ℝ3−K_{m,n})≅⟨a,b∣am=b^n⟩. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.25
The Shrinking Wedge of Circles. Consider the subspace X ⊂ ℝ^{2} that is the union of the circles C_{n} of radius ^ 1 /{n} and center (imath { /{n} }, 0) for n = 1, 2, …. For one thing, it is nonabelian, since the retraction X {→ } C{1} ∪ … ∪ C_{n} that collapses all the circles smaller than C_{n} to the basepoint induces a surjection from π_{1} (X) to a free group on n generators.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The Shrinking Wedge of Circles. Consider the subspace X ⊂ ℝ^{2} that is the union of the circles C_{n} of radius ^ 1 /{n} and center (imath _ { /{n} }, 0) for n = 1, 2, …. For one thing, it is nonabelian, since the retraction X {→ } C_{1} ∪ … ∪ C_{n} that collapses all the circles smaller than C_{n} to the basepoint induces a surjection from π_{1} (X) to a free group on n generators. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1.26
Let Y be obtained from path-connected X by attaching cells. (a) For attached 2-cells with normal subgroup N generated by the conjugated attaching loops, π₁(X,x₀)→π₁(Y,x₀) is surjective with kernel N, so π₁(Y)≅π₁(X)/N. (b) Attaching n-cells for fixed n>2 induces π₁(X,x₀)≅π₁(Y,x₀). (c) For a path-connected CW complex X, X²↪X induces π₁(X²,x₀)≅π₁(X,x₀).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let Y be obtained from path-connected X by attaching cells. (a) For attached 2-cells with normal subgroup N generated by the conjugated attaching loops, π₁(X,x₀)→π₁(Y,x₀) is surjective with kernel N, so π₁(Y)≅π₁(X)/N. (b) Attaching n-cells for fixed n>2 induces π₁(X,x₀)≅π₁(Y,x₀). (c) For a path-connected CW complex X, X²↪X induces π₁(X²,x₀)≅π₁(X,x₀). Cell-attachment/pushout infrastructure exists, but no checked theorem supplies the complete π₁ quotient/free-generator effect of attaching 1- and ≥2-cells. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 1.27
The surface M_{g} is not homeomorphic, or even homotopy equivalent, to M_{h} if g ≠ h.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The surface M_{g} is not homeomorphic, or even homotopy equivalent, to M_{h} if g ≠ h. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 1.28
For every group G there is a 2 dimensional cell complex X_{G} with 1 π_{1} (X_{G}) ≅ G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For every group G there is a 2 dimensional cell complex X_{G} with 1 π_{1} (X_{G}) ≅ G. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.29
For G=ℤ_n=⟨a∣a^n⟩, the presentation complex X_G is S^1 with a 2-cell attached by z↦z^n. For n=2 this is ℝP^2; for n>2 it is not a surface, since n sheets of the 2-cell meet along the circle.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For G=ℤ_n=⟨a∣a^n⟩, the presentation complex X_G is S^1 with a 2-cell attached by z↦z^n. For n=2 this is ℝP^2; for n>2 it is not a surface, since n sheets of the 2-cell meet along the circle. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — sheets of a covering space
For an evenly covered U, the disjoint open subsets of X̃ mapped homeomorphically onto U are the sheets of X̃ over U. If U is connected they are the components of p^{-1}(U); the number of sheets is the fiber cardinality and is locally constant.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For an evenly covered U, the disjoint open subsets of X̃ mapped homeomorphically onto U are the sheets of X̃ over U. If U is connected they are the components of p^{-1}(U); the number of sheets is the fiber cardinality and is locally constant. IsEvenlyCovered gives local sheets and fiber trivializations; no checked theorem packages the source global sheet-number constancy/cardinality bundle in full. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — universal cover
A simply-connected covering space of X is called the universal cover; it covers every other connected covering space of X.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Basic.lean::UniversalCover; TauCeti/AlgebraicTopology/UniversalCover/Classification/Intermediate.lean::UniversalCover.exists_isCoveringMap_comp_eq_proj — TauCeti’s universal cover is simply connected, and the intermediate-cover theorem factors it through every connected covering, exactly the source universal-cover characterization.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Definition — lift
For f:Y→X and p:X̃→X, a lift is f̃:Y→X̃ with p∘f̃=f.
Formalized. Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.existsUnique_continuousMap_lifts, IsCoveringMap.eq_liftPath_iff — The library uses the standard definition: a lift is a continuous map whose composite with the covering map equals the original map; its lifting theorems expose precisely this equation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.30
Given a covering space p: {tilde(X) } → X, a homotopy f_{t}: Y → X, and a map tilde(f){0} {: } Y {→ } tilde(X) lifting f{0}, then there exists a unique homotopy tilde(f){t} {: } Y {→ } tilde(X) of tilde(f){0} that lifts f_{t}.
Formalized. Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff, eq_liftHomotopy_iff' — The homotopy lifting construction and uniqueness lemmas give the exact unique lifted homotopy with prescribed initial lift.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.31
The map p_{}: π_{1} (tilde(X), tilde(x){0}) → π{1} (X, x_{0}) induced by a covering space p: (tilde(X), tilde(x){0}) (X, x{0}) is injective. The image subgroup p_{} (π_{1} (tilde(X), tilde(x){0})) in π{1} (X, x_{0}) consists of the homotopy classes of loops in X based at x_{0} whose lifts to tilde(X) starting at tilde(x)_{0} are loops.
Formalized. pinned Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.injective_path_homotopic_map; TauCeti/Topology/Homotopy/Monodromy/Basic.lean::IsCoveringMap.monodromy_eq_self_iff_mem_range, stabilizer_eq_range — Coverings induce injective π₁ maps; monodromy fixes a fiber point exactly when the loop class lies in the induced subgroup, i.e. exactly when the lifted loop closes.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d; P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.34.0-rc2
Proposition 1.32
The number of sheets of a covering space p: (tilde(X), tilde(x){0}) (X, x{0}) with X and tilde(X) path-connected equals the index of p_{*} (π_{1} (tilde(X), tilde(x){0})) in π{1} (X, x_{0}).
Formalized. TauCeti/Topology/Homotopy/Monodromy/Basic.lean::IsCoveringMap.card_fiber_eq_index — The theorem identifies the cardinality of the covering fiber with the index of the induced fundamental-group subgroup.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Proposition 1.33
Suppose given a covering space p: (tilde(X), tilde(x){0}) {→ } (X, x{0}) and a map f: (Y, y_{0}) → (X, x_{0}) with Y path-connected and locally path-connected. Then a lift tilde(f): (Y, y_{0}) (tilde(X), tilde(x){0}) of f exists iff f{} (π_{1} (Y, y_{0})) ⊂ p_{} (π_{1} (tilde(X), tilde(x)_{0})).
Formalized. Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le; Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean::FundamentalGroup.map — The existence/uniqueness theorem gives the subgroup-containment ⇒ lift direction, while functoriality of an existing lift gives the converse containment, yielding the standard lifting criterion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.34
Given a covering space p: {tilde(X) } → X and a map f: Y {→ } X, if two lifts {tilde(f) }{1}, {tilde(f) }{2}: Y → {tilde(X) } of f agree at one point of Y and Y is connected, then tilde(f){1} and {tilde(f) }{2} agree on all of Y.
Formalized. Mathlib/Topology/Covering/Basic.lean::IsCoveringMap.eq_of_comp_eq — Two lifts over a preconnected domain agreeing at one point are equal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — semilocally simply-connected
X is semilocally simply-connected if every x has a neighborhood U for which π₁(U,x)→π₁(X,x) induced by inclusion is trivial.
Formalized. TauCeti/AlgebraicTopology/SemilocallySimplyConnected/On.lean::SemilocallySimplyConnectedAt, semilocallySimplyConnectedAt_iff — This is the exact local condition that sufficiently small loops die in the ambient fundamental group.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Example 1.35
For m,n≥2, X_{m,n} is the union of the mapping cylinders of z↦z^m and z↦z^n along their common boundary circle. Its universal cover is T_{m,n}×ℝ, where the infinite graph T_{m,n} is contractible; hence the universal cover is contractible and simply-connected.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For m,n≥2, X_{m,n} is the union of the mapping cylinders of z↦z^m and z↦z^n along their common boundary circle. Its universal cover is T_{m,n}×ℝ, where the infinite graph T_{m,n} is contractible; hence the universal cover is contractible and simply-connected. No searched topology development formalizes Hatcher’s specific torus-knot 2-complex universal cover and its contractibility. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1.36
Suppose X is path-connected, locally path-connected, and semilocally simply-connected. Then for every subgroup H ⊂ π_{1} (X, x_{0}) there is a covering space p: X_{H} → X such that p_{*} (π_{1} (X_{H}, tilde(x){0})) = H for a suitably chosen basepoint 1 {tilde(x) }{0} ∈ X_{H}.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Classification/Existence.lean::UniversalCover.subgroupCover; TauCeti/AlgebraicTopology/UniversalCover/Classification/RecoveredSubgroup.lean::range_mapOfEq_subgroupQuotientProj — Every subgroup of π₁ is realized by the constructed connected covering, and the recovered subgroup theorem identifies its induced π₁ image with the prescribed subgroup.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Proposition 1.37
If X is path-connected and locally path-connected, then two path-connected covering spaces p_{1} {: } tilde(X){1} {→ } X and p{2} {: } tilde(X){2} → X are isomorphic via an isomorphism f {: tilde(X){1} {→ } tilde(X){2} } taking a basepoint tilde(x){1} ∈ p_{1}^{- 1} (x_{0}) to a basepoint tilde(x){2} ∈ p{2}^{- 1} (x_{0}) iff p_{1 } (π_{1} (tilde(X){1}, tilde(x){1})) = p_{2 } (π_{1} (tilde(X){2}, tilde(x){2})).
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Classification/Pointed.lean::IsCoveringMap.exists_homeomorph_comp_eq_iff_range_eq — For pointed connected covers, equality of induced subgroups is equivalent to existence of a covering isomorphism preserving the chosen fiber points.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Theorem 1.38
Let X be path-connected, locally path-connected, and semilocally simply-connected. Then there is a bijection between the set of basepoint-preserving isomorphism classes of path-connected covering spaces p: (tilde(X), tilde(x){0}) (X, x{0}) and the set of subgroups of π_{1} (X, x_{0}), obtained by associating the subgroup p_{*} (π_{1} (tilde(X), tilde(x){0})) to the covering space (tilde(X), tilde(x){0}). If basepoints are ignored, this correspondence gives a bijection between isomorphism classes of path-connected covering spaces p: {tilde(X) } → X and conjugacy classes of subgroups of π_{1} (X, x_{0}).
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Classification/Bijection.lean::UniversalCover.existsUnique_subgroup_homeomorph_subgroupQuotient, UniversalCover.exists_homeomorph_subgroupQuotient_comp_eq_iff_eq, UniversalCover.exists_homeomorph_subgroupQuotient_comp_eq_iff_exists_eq_map_conj — These are the pointed subgroup classification and unpointed conjugacy-class classification of connected covering spaces; the source file explicitly identifies the result with Hatcher Theorem 1.38.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Construction — action of π₁ on a covering fiber
For a covering p:X̃→X and a loop γ at x₀, path lifting gives a permutation L_γ of the fiber p^{-1}(x₀), depending only on [γ]; with the inverse convention used in the source, [γ]↦L_γ is a homomorphism π₁(X,x₀)→Perm(p^{-1}(x₀)), the action of π₁ on the fiber.
Formalized. Mathlib/Topology/Homotopy/Lifting.lean::IsCoveringMap.monodromy, fundamentalGroupMulAction, monodromyPerm — Path lifting defines the endpoint permutation of each fiber; homotopy invariance and multiplication give exactly the π₁ action/permutation representation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — deck transformation
A deck (covering) transformation of p:X̃→X is a covering-space automorphism X̃→X̃; these form a group G(X̃) under composition.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Deck/Basic.lean::TauCeti.Deck — A deck transformation is represented exactly as a homeomorphism of the total space commuting with the projection; these form the deck group.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Definition — normal covering
A covering is normal if any two lifts of the same point are related by a deck transformation.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Deck/Regular/Basic.lean::Deck.IsRegular — Regularity is defined by transitivity of deck transformations on each fiber, exactly the source normal-cover condition.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Proposition 1.39
Let p:(X_tilde,x_tilde0)→(X,x0) be a path-connected covering of a path-connected, locally path-connected space and H=p_*π1(X_tilde,x_tilde0). Then the covering is normal iff H is normal in π1(X,x0), and its deck group is N(H)/H. Hence for a normal covering the deck group is π1(X,x0)/H.
Formalized. TauCeti/AlgebraicTopology/UniversalCover/Classification/Regular.lean::IsCoveringMap.isRegular_iff_normal_range; TauCeti/AlgebraicTopology/UniversalCover/Classification/DeckGroup.lean::UniversalCover.deckSubgroupQuotientProjEquiv, deckSubgroupQuotientProjEquivOfNormal — Regularity is equivalent to normality of the induced subgroup, and the deck group is identified with the normalizer quotient, specializing to π₁/H when H is normal.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Apache-2.0; Lean 4.34.0-rc2; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d
Definition — group action on a space
An action of G on Y is a homomorphism G→Homeo(Y); equivalently g₁(g₂y)=(g₁g₂)y.
Formalized. Mathlib/Topology/Algebra/ConstMulAction.lean::Homeomorph.smul, ContinuousConstSMul; MulAction — A MulAction G Y is the action law, and continuous scalar multiplication makes each group element act by a homeomorphism (Homeomorph.smul), exactly a homomorphism into Homeo(Y).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — orbit space
For a G-action on Y, the orbit space Y/G identifies points in the same orbit Gy.
Formalized. Mathlib/GroupTheory/GroupAction/Defs.lean::MulAction.orbitRel; MulAction.orbitRel.Quotient — The quotient by the orbit equivalence relation is exactly the orbit space Y/G.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 1.40
If a group G acts on Y with the covering-space-action condition that every y has a neighborhood U whose distinct G-translates are disjoint, then Y→Y/G is a normal covering. If Y is path-connected, G is its full deck group; if Y is also locally path-connected, G≅π1(Y/G)/p_*π1(Y).
Formalized. pinned Mathlib/Topology/Covering/Quotient.lean::IsQuotientCoveringMap; Mathlib/Topology/Homotopy/Lifting.lean::IsQuotientCoveringMap.fundamentalGroupEquiv; TauCeti/AlgebraicTopology/UniversalCover/Deck/Quotient/Covering.lean::Deck.IsQuotientCoveringMap.isRegular; TauCeti/AlgebraicTopology/UniversalCover/Deck/Quotient/ActingGroup.lean::Deck.IsQuotientCoveringMap.deckMulEquiv — The quotient-action interface gives the normal covering; TauCeti proves regularity and identifies the acting group with the full deck group on a connected total space; the fundamental-group quotient equivalence supplies the final π₁ quotient statement.
Searched: T=2db3a983be93975cbf1d54bcc7d6ae1b97830856; Mathlib 5fcc6656691ed31965746c369f41fa75e567ac9d; P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.34.0-rc2
Definition — covering-space action and free action
A covering-space action is one in which each y has a neighborhood U whose translates g(U) are pairwise disjoint. An action is free when only the identity fixes a point.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A covering-space action is one in which each y has a neighborhood U whose translates g(U) are pairwise disjoint. An action is free when only the identity fixes a point. Pinned Mathlib has IsQuotientCoveringMap.disjoint, IsCancelSMul, and ProperlyDiscontinuousSMul.exists_nhds_disjoint_image, but the latter is a stronger compact-action class and the former bakes in quotient-map data; neither is exactly the standalone pair of source definitions. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.41
The order-5 rotational action on the closed orientable genus-11 surface gives a 5-sheeted normal covering M_{11}→M_3, so π₁(M_{11}) is a normal index-5 subgroup of π₁(M_3) with quotient ℤ_5. More generally there are coverings M_{mn+1}→M_{m+1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The order-5 rotational action on the closed orientable genus-11 surface gives a 5-sheeted normal covering M_{11}→M_3, so π₁(M_{11}) is a normal index-5 subgroup of π₁(M_3) with quotient ℤ_5. More generally there are coverings M_{mn+1}→M_{m+1}. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.42
Consider the grid in ℝ^{2} formed by the horizontal and vertical lines through points in ℤ^{2}. Thus we see that the fundamental groups of the torus and the Klein bottle are the symmetry groups G in the two cases.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Consider the grid in ℝ^{2} formed by the horizontal and vertical lines through points in ℤ^{2}. Thus we see that the fundamental groups of the torus and the Klein bottle are the symmetry groups G in the two cases. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.43
ℝP^{n}. The antipodal map of S^{n}, x ↦ - x, generates an action of ℤ_{2} on S^{n} with orbit space ℝP^{n}, real projective n space, as defined in Example 0.4. A generator for π_{1} (ℝP^{n}) is any loop obtained by projecting a path in S^{n} connecting two antipodal points.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: ℝP^{n}. The antipodal map of S^{n}, x ↦ - x, generates an action of ℤ_{2} on S^{n} with orbit space ℝP^{n}, real projective n space, as defined in Example 0.4. A generator for π_{1} (ℝP^{n}) is any loop obtained by projecting a path in S^{n} connecting two antipodal points. TauCeti proves the antipodal quotient covering, deck group, regularity and π₁(ℝPⁿ)≃ℤ₂ for n≥2, but no checked theorem identifies every projected antipodal-joining path with the generator; strict whole-row semantics reject the partial match. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.44
In Example 1.35 we constructed a contractible 2 complex tilde(X){m, n} ~ = T{m, n} × ℝ as the universal cover of a finite 2 complex X_{m, n} that was the union of the mapping cylinders of the two maps S^{1} → S^{1}, z ↦ z^{m} and z ↦ z^{n}. The group of deck transformations of this covering space is therefore the fundamental group π_{1} (X_{m, n}).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: In Example 1.35 we constructed a contractible 2 complex tilde(X){m, n} ~ = T{m, n} × ℝ as the universal cover of a finite 2 complex X_{m, n} that was the union of the mapping cylinders of the two maps S^{1} → S^{1}, z ↦ z^{m} and z ↦ z^{n}. The group of deck transformations of this covering space is therefore the fundamental group π_{1} (X_{m, n}). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — Cayley graph and Cayley complex
From a presentation G=⟨g_α | r_β⟩, the universal cover of the presentation 2-complex has vertices indexed by G, edges for multiplication by generators, and 2-cells for relators; its 1-skeleton is the Cayley graph and the full complex the Cayley complex.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: From a presentation G=⟨g_α | r_β⟩, the universal cover of the presentation 2-complex has vertices indexed by G, edges for multiplication by generators, and 2-cells for relators; its 1-skeleton is the Cayley graph and the full complex the Cayley complex. Group-presentation, Cayley-graph, and quotient APIs exist algebraically, but no checked source constructs the full universal-cover presentation 2-complex/Cayley complex bundle. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.45
When G is the free group on two generators a and ^ b, X_{G} is S^{1} ∨ S^{1} and tilde(X)_{G} is the Cayley graph of ℤ * ℤ pictured at the right. The action of a on this graph is a rightward shift along the central horizontal axis, while ^ b acts by an upward shift along the central vertical axis. The composition ab of these two shifts then takes the vertex e to the vertex ab. Similarly, the action of any w ∈ ℤ * ℤ takes e to the vertex w.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: When G is the free group on two generators a and ^ b, X_{G} is S^{1} ∨ S^{1} and tilde(X)_{G} is the Cayley graph of ℤ * ℤ pictured at the right. The action of a on this graph is a rightward shift along the central horizontal axis, while ^ b acts by an upward shift along the central vertical axis. The composition ab of these two shifts then takes the vertex e to the vertex ab. Similarly, the action of any w ∈ ℤ * ℤ takes e to the vertex w. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.46
The group G = ℤ × ℤ with presentation ⟨ x, y | x y x^{- 1} y^{- 1} ⟩ has X_{G} the torus S^{1} {× } S^{1}, and tilde(X)_{G} is ℝ^{2} with vertices the integer lattice ℤ^{2} ⊂ ℝ^{2} and edges the horizontal and vertical segments between these lattice points. The action of G is by translations (x, y) ↦ (x + m, y + n).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The group G = ℤ × ℤ with presentation ⟨ x, y | x y x^{- 1} y^{- 1} ⟩ has X_{G} the torus S^{1} {× } S^{1}, and tilde(X)_{G} is ℝ^{2} with vertices the integer lattice ℤ^{2} ⊂ ℝ^{2} and edges the horizontal and vertical segments between these lattice points. The action of G is by translations (x, y) ↦ (x + m, y + n). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.47
For G = ℤ_{2} = . x | x^{2}., X_{G} is ℝP^{2} and tilde(X){G} = S^{2}. More generally, for ℤ{n} = . x | x^{n}., X_{G} is S^{1} with a disk attached by the map z ↦ z^{n} and tilde(X){G} consists of n disks D{1}, …, D_{n} with their boundary circles identified. A generator of ℤ_{n} acts on this union of disks by sending D_{i} to D_{i + 1} via a 2 π / n rotation, the subscript i being taken mod n. The common boundary circle of the disks is rotated by 2 π / n.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For G = ℤ_{2} = . x | x^{2}., X_{G} is ℝP^{2} and tilde(X){G} = S^{2}. More generally, for ℤ{n} = . x | x^{n}., X_{G} is S^{1} with a disk attached by the map z ↦ z^{n} and tilde(X){G} consists of n disks D{1}, …, D_{n} with their boundary circles identified. A generator of ℤ_{n} acts on this union of disks by sending D_{i} to D_{i + 1} via a 2 π / n rotation, the subscript i being taken mod n. The common boundary circle of the disks is rotated by 2 π / n. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1.48
If G = ℤ_{2} * ℤ_{2} = ⟨ a, b | a^{2}, b^{2} ⟩ then the Cayley graph is a union of an infinite sequence of circles each tangent to its two neighbors. We obtain tilde(X)_{G} from this graph by making each circle the equator of a 2 sphere, yielding an infinite sequence of tangent 2 spheres.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If G = ℤ_{2} * ℤ_{2} = ⟨ a, b | a^{2}, b^{2} ⟩ then the Cayley graph is a union of an infinite sequence of circles each tangent to its two neighbors. We obtain tilde(X)_{G} from this graph by making each circle the equator of a 2 sphere, yielding an infinite sequence of tangent 2 spheres. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — graph
A graph is a 1-dimensional CW complex: a discrete vertex set X^0 with 1-cells attached by their endpoints.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A graph is a 1-dimensional CW complex: a discrete vertex set X^0 with 1-cells attached by their endpoints. finite-graph-fundamental-group@dd57e3ab8bc5a7042fcc5498e778b008d87ac032 gives a finite topological graph-realization model, while Mathlib has CWComplex.OneSkeletonGraph; neither checked bridge identifies arbitrary Hatcher 1-dimensional CW complexes with this graph model. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — subgraph, tree, maximal tree
A subgraph is a closed union of vertices and edges. A tree is a contractible graph; a tree in X is maximal when it contains every vertex of X.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A subgraph is a closed union of vertices and edges. A tree is a contractible graph; a tree in X is maximal when it contains every vertex of X. Pinned combinatorial tree/subgraph predicates and dd57e3ab8bc5a7042fcc5498e778b008d87ac032 tree-contractibility cover components of the row, but the source bundles topological graph/subgraph definitions, tree contractibility, and maximal-tree terminology for arbitrary CW graphs. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1A.1
Every connected graph contains a maximal tree, and in fact any tree in the graph is contained in a maximal tree.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every connected graph contains a maximal tree, and in fact any tree in the graph is contained in a maximal tree. Pinned Mathlib proves every acyclic subgraph of a connected simple graph extends to a spanning tree, but Hatcher’s CW graphs may have loops/multiple edges and no checked bridge turns the topological statement into this simple-graph theorem. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1A.2
For a connected graph X with maximal tree T, π_{1} (X) is a free group with basis the classes [ f_{α} ] corresponding to the edges e_{α} of X - T.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a connected graph X with maximal tree T, π_{1} (X) is a free group with basis the classes [ f_{α} ] corresponding to the edges e_{α} of X - T. GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c has spanningTreeBasis, graphCombinatorialToTopologicalEquiv, and graphFundamentalGroupBasis for finite graph realizations. Hatcher states the result for arbitrary connected graphs, so the finite specialization is not promoted. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 1A.3
Every covering space of a graph is also a graph, with vertices and edges the lifts of the vertices and edges in the base graph.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Every covering space of a graph is also a graph, with vertices and edges the lifts of the vertices and edges in the base graph. GraphCoveringTheory@c918a72c5170503c98fd66a0f3116b7bfcd1250c constructs topological covers from combinatorial graph covers, but no checked converse says every covering of an arbitrary Hatcher graph inherits a graph structure. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 1A.4
Every subgroup of a free group is free.
Formalized. Mathlib/GroupTheory/FreeGroup/NielsenSchreier.lean::subgroupIsFreeOfIsFree — This is Nielsen–Schreier directly: every subgroup of a free group is free.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — K(G,1) space
A K(G,1) is a path-connected space with π₁≅G and contractible universal cover; these are the n=1 Eilenberg–Mac Lane spaces.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A K(G,1) is a path-connected space with π₁≅G and contractible universal cover; these are the n=1 Eilenberg–Mac Lane spaces. TauCeti formalizes the standard equivalent aspherical/higher-homotopy definition of K(G,1), and proves universal covers weakly contractible. No checked Whitehead/CW bridge upgrades this to the source’s explicit “contractible universal cover” definition in the stated generality. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.1
S^{1} is a K (ℤ, 1). More generally, a connected graph is a K (G, 1) with G a free group, since by the results of S 1. A its universal cover is a tree, hence contractible.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: S^{1} is a K (ℤ, 1). More generally, a connected graph is a K (G, 1) with G a free group, since by the results of S 1. A its universal cover is a tree, hence contractible. TauCeti proves AddCircle.isEilenbergMacLaneSpaceOne; finite graph developments prove tree-contractible universal covers in specialized models. The bundled arbitrary connected-graph assertion is not owned in full. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.2
Closed surfaces with infinite π_{1}, in other words, closed surfaces other than S^{2} and ℝP^{2}, are K (G, 1) ’s. This will be shown in Example 1B.14 below. It also follows from the theorem in surface theory that the only simply-connected surfaces without boundary are S^{2} and ℝ^{2}, so the universal cover of a closed surface with infinite fundamental group must be ℝ^{2} since it is noncompact. Nonclosed surfaces deformation retract onto graphs, so such surfaces are K (G, 1) ’s with G free.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Closed surfaces with infinite π_{1}, in other words, closed surfaces other than S^{2} and ℝP^{2}, are K (G, 1) ’s. This will be shown in Example 1B.14 below. It also follows from the theorem in surface theory that the only simply-connected surfaces without boundary are S^{2} and ℝ^{2}, so the universal cover of a closed surface with infinite fundamental group must be ℝ^{2} since it is noncompact. Nonclosed surfaces deformation retract onto graphs, so such surfaces are K (G, 1) ’s with G free. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.3
ℝP^∞ is a K(ℤ_2,1): its universal cover S^∞ is contractible. An explicit contraction is obtained by first shifting coordinates (x₁,x₂,…)↦(0,x₁,x₂,…) and then homotoping this shifted sphere to the first basis vector.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: ℝP^∞ is a K(ℤ_2,1): its universal cover S^∞ is contractible. An explicit contraction is obtained by first shifting coordinates (x₁,x₂,…)↦(0,x₁,x₂,…) and then homotoping this shifted sphere to the first basis vector. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.4
Generalizing the preceding example, we can construct a K (ℤ_{m}, 1) as an infinite-dimensional lens space S^{∞} / ℤ_{m}, where ℤ_{m} acts on S^{∞}, regarded as the unit sphere in ℂ^{∞}, by scalar multiplication by m^{t h} roots of unity, a generator of this action being the map (z_{1}, z_{2}, …) ↦ e^{2 π i / m} (z_{1}, z_{2}, …). It is not hard to check that this is a covering space action.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Generalizing the preceding example, we can construct a K (ℤ_{m}, 1) as an infinite-dimensional lens space S^{∞} / ℤ_{m}, where ℤ_{m} acts on S^{∞}, regarded as the unit sphere in ℂ^{∞}, by scalar multiplication by m^{t h} roots of unity, a generator of this action being the map (z_{1}, z_{2}, …) ↦ e^{2 π i / m} (z_{1}, z_{2}, …). It is not hard to check that this is a covering space action. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.5
A product K (G, 1) × K (H, 1) is a K (G × H, 1) since its universal cover is the product of the universal covers of K (G, 1) and K (H, 1). By taking products of circles and infinite-dimensional lens spaces we therefore get K (G, 1) ’s for arbitrary finitely generated abelian groups G. For example the n dimensional torus T^{n}, the product of n circles, is a K (ℤ^{n}, 1).
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A product K (G, 1) × K (H, 1) is a K (G × H, 1) since its universal cover is the product of the universal covers of K (G, 1) and K (H, 1). By taking products of circles and infinite-dimensional lens spaces we therefore get K (G, 1) ’s for arbitrary finitely generated abelian groups G. For example the n dimensional torus T^{n}, the product of n circles, is a K (ℤ^{n}, 1). TauCeti proves products of its aspherical K(G,1) spaces and the torus case, but the source row also constructs arbitrary finitely generated abelian examples using infinite-dimensional lens spaces, which are not formalized. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.6
For a closed connected subspace K of S^{3} that is nonempty, the complement S^{3} - K is a K (G, 1). The homotopy lifting property then implies that the universal cover of S^{3} - K is homotopy equivalent to the universal cover of X_{m, n}, hence is also contractible.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a closed connected subspace K of S^{3} that is nonempty, the complement S^{3} - K is a K (G, 1). The homotopy lifting property then implies that the universal cover of S^{3} - K is homotopy equivalent to the universal cover of X_{m, n}, hence is also contractible. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.7
It is not hard to construct a K (G, 1) for an arbitrary group G, using the notion of a Δ-complex defined in S 2. (The notation hat(g){i} means that this vertex is deleted.) The complex E G is contractible by the homotopy h{t} that slides each point x ∈ [ g_{0}, …, g_{n} ] along the line segment in [ e, g_{0}, …, g_{n} ] from x to the vertex [ e ], where e is the identity element of G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: It is not hard to construct a K (G, 1) for an arbitrary group G, using the notion of a Δ-complex defined in S 2. (The notation hat(g){i} means that this vertex is deleted.) The complex E G is contractible by the homotopy h{t} that slides each point x ∈ [ g_{0}, …, g_{n} ] along the line segment in [ e, g_{0}, …, g_{n} ] from x to the vertex [ e ], where e is the identity element of G. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 1B.8
The homotopy type of a CW complex K (G, 1) is uniquely determined parallel by G.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: The homotopy type of a CW complex K (G, 1) is uniquely determined parallel by G. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 1B.9
Let X be a connected CW complex and let Y be a K (G, 1). Then every homomorphism π_{1} (X, x_{0}) → π_{1} (Y, y_{0}) is induced by a map (X, x_{0}) (Y, y_{0}) that is unique up to homotopy fixing x_{0}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Let X be a connected CW complex and let Y be a K (G, 1). Then every homomorphism π_{1} (X, x_{0}) → π_{1} (Y, y_{0}) is induced by a map (X, x_{0}) (Y, y_{0}) that is unique up to homotopy fixing x_{0}. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — graph of groups
A graph of groups is an oriented connected graph with a group at each vertex and a homomorphism from the tail group to the head group along each oriented edge.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: A graph of groups is an oriented connected graph with a group at each vertex and a homomorphism from the tail group to the head group along each oriented edge. ComputationalPathsLean@f90943eecdde516817fbc33863486b681a0a9645::ComputationalPaths/Path/Algebra/BassSerrePaths.lean::BSGraphOfGroups is adjacent Bass–Serre data with edge groups and two inclusions, not Hatcher’s stated oriented-edge homomorphism-from-tail-group formulation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.10
Suppose Γ consists of one central vertex with a number of edges radiating out from it, and the group G_{ν} at this central vertex is trivial, hence also all the edge homomorphisms. Then van Kampen’s theorem implies that π_{1} (K Γ) is the free product of the groups at all the outer vertices.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Suppose Γ consists of one central vertex with a number of edges radiating out from it, and the group G_{ν} at this central vertex is trivial, hence also all the edge homomorphisms. Then van Kampen’s theorem implies that π_{1} (K Γ) is the free product of the groups at all the outer vertices. Free-product APIs and graph-of-groups algebra are available, but no checked KΓ construction instantiates the source star graph and proves its π₁ free-product calculation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — graph product
For a graph of groups Γ, its graph product is π₁(KΓ), also called the fundamental group of the graph of groups.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: For a graph of groups Γ, its graph product is π₁(KΓ), also called the fundamental group of the graph of groups. ComputationalPaths defines an algebraic Bass–Serre fundamental group, but no checked topological KΓ object identifies its π₁ with Hatcher’s graph product as defined here. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 1B.11
If all the edge homomorphisms φ_{e} are injective, then K is a K (G, 1) and the inclusions K (G_{ν}, 1) ↪ K Γ induce injective maps on π_{1}.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: If all the edge homomorphisms φ_{e} are injective, then K is a K (G, 1) and the inclusions K (G_{ν}, 1) ↪ K Γ induce injective maps on π_{1}. Mathlib proves injectivity of vertex maps into amalgamated pushouts and HNN extensions under injective edge maps, but no checked KΓ construction proves the source K(G,1) theorem and induced vertex π₁ injections. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.12
Free Products with Amalgamation. Suppose the graph of groups is A . Applying van Kampen’s theorem to the decomposition of K Γ into its two mapping cylinders, we see that π_{1} (K Γ) is the quotient of A * B obtained by identifying the subgroup C ⊂ A with the subgroup C ⊂ B.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Free Products with Amalgamation. Suppose the graph of groups is A . Applying van Kampen’s theorem to the decomposition of K Γ into its two mapping cylinders, we see that π_{1} (K Γ) is the quotient of A * B obtained by identifying the subgroup C ⊂ A with the subgroup C ⊂ B. Mathlib/GroupTheory/PushoutI.lean::Monoid.PushoutI, of_injective, and normal-form theorems exactly formalize the amalgamated free product algebra, but the source row is a topological π₁(KΓ) computation via two mapping cylinders; that bridge is absent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.13
HNN Extensions. Consider a graph of groups C {→ } A with φ and psi both monomorphisms. Using a K (C, 1) with a single 0 cell, we see that K Γ can be obtained from K (A, 1) ∨ S^{1} by attaching cells of dimension two and greater, so π_{1} (K Γ) is a quotient of A * ℤ, and it is not hard to figure out that the relations defining this quotient are of the form t φ (c) t^{- 1} = psi (c) where t is a generator of the Z factor and c ranges over C, or a set of generators for C.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: HNN Extensions. Consider a graph of groups C {→ } A with φ and psi both monomorphisms. Using a K (C, 1) with a single 0 cell, we see that K Γ can be obtained from K (A, 1) ∨ S^{1} by attaching cells of dimension two and greater, so π_{1} (K Γ) is a quotient of A * ℤ, and it is not hard to figure out that the relations defining this quotient are of the form t φ (c) t^{- 1} = psi (c) where t is a generator of the Z factor and c ranges over C, or a set of generators for C. Mathlib/GroupTheory/HNNExtension.lean::HNNExtension, HNNExtension.of, t, equiv_eq_conj, of_injective exactly formalize the HNN algebra, but no checked KΓ/topological π₁ bridge owns the whole source example. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 1B.14
Closed Surfaces. A closed orientable surface M of genus two or greater can be cut along a circle into two compact surfaces M_{1} and M_{2} such that the closed surfaces obtained from M_{1} and M_{2} by filling in their boundary circle with a disk have smaller genus than M. Thus we have realized the original surface M as K Γ for Γ a graph of groups of the form F_{1} ← ℤ → F_{2} with F_{1} and F_{2} free and the two maps injective.
Not formalized. none; no complete checked declaration under strict bundle semantics — No checked project/P/H/open/external/indexed Lean declaration realizes the whole source row: Closed Surfaces. A closed orientable surface M of genus two or greater can be cut along a circle into two compact surfaces M_{1} and M_{2} such that the closed surfaces obtained from M_{1} and M_{2} by filling in their boundary circle with a disk have smaller genus than M. Thus we have realized the original surface M as K Γ for Γ a graph of groups of the form F_{1} ← ℤ → F_{2} with F_{1} and F_{2} free and the two maps injective. No searched declaration formalizes the genus≥2 surface decomposition as the stated graph of free groups with injective ℤ edge maps. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.