Chapter 2. Homology
FC07 — Hatcher, Algebraic Topology.
This chapter contains 25 definitions, 15 theorems, 14 propositions, 4 lemmas, 7 corollaries, 25 examples, 7 constructions and 1 convention.
Of the 98 statements checked against Lean, 20 are formalized somewhere and 78 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 78 | 80% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 20 | 20% | Mathlib states and proves it. |
| checked in total | 98 |
- Canonical source block: FC07 Hatcher, Chapter 2,
FC07-C02-U001–FC07-C02-U098, exactly 98 contiguous rows retrieved from FC07 — Hatcher, Algebraic Topology throughagent-memory. - Search order followed the mapping 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/package discovery, broad GitHub/discoverable Lean, and local mirrors. Noproject-existingC02 owner was found. - Every promoted Mathlib declaration/path was compiled through the project toolchain at the exact pin
P; exact source files were also checked in the pinned git object. C02 therefore uses onlymathlibandunmatchedroutes: 20 pinned positive rows and 78 dated unmatched rows. - The pinned singular-homology stack supplies
TopCat.toSSetObjEquiv,singularChainComplexFunctor,singularHomologyFunctor, the H₀/path-component theorem, and topological homotopy invariance. Generic homological algebra supplies chain complexes/homology maps, chain-homotopy invariance, exact/short-exact complexes, connecting morphisms, and the three exactness pieces of the long exact homology sequence. These are credited only where they own the entire Hatcher unit. - Current Mathlib
HaddsMathlib/AlgebraicTopology/SimplicialSet/Homology/Relative.lean:SSetPair.chainComplex,SSetPair.homology,SSetPair.homologyFunctor,SSetPair.homologyδ, andhomology_exact₁/₂/₃. This is relative homology of simplicial-set monomorphisms. No checked functor/bridge fromTopPairor singular topological pairs toSSetPairwas found, so it is adjacent post-pin evidence rather than areference-portowner for U026/U031–U033/U037/U039/U042/U071. Mathlib/AlgebraicTopology/EilenbergSteenrod.leanat P/H definesTopPair.HomologyPretheory(absolute/relative functors plus boundary transformations) and separatelyIsHomotopyInvariant; it does not package the exactness, suspension, wedge/additivity, and dimension axioms required by Hatcher U075, hence U075–U077 remain unmatched.Mathlib/Algebra/Homology/EulerCharacteristic.leanat P/H defines algebraicHomologicalComplex.eulerCharandhomologyEulerChar, but contains no theorem identifying them and no CW-cell-count/singular-homology bridge. It therefore does not own U064/U065. Sheaf-cohomology Mayer–Vietoris files likewise are not singular-homology routes for U067–U070.harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838(MIT; Lean 4.32.0; Mathlib81a5d257c8e410db227a6665ed08f64fea08e997) proves Brouwer fixed point on every nonempty compact convex subset of a finite-dimensional real normed space. It covers the fixed-point clause of U025, but the row also asserts arbitrary-dimensional disk no-retraction, and no checked declaration in that package supplies it; strict bundle semantics therefore leave U025 unmatched.mccorvie/classification-of-surfaces@e3c7230fe78d7b056a415d9ecae6f77887046b32(Apache-2.0; Lean 4.32.0; Mathlib81a5d257c8e410db227a6665ed08f64fea08e997) proves planar disk no-retraction/Brouwer and hasinvariance_of_domain_open_mapconditional on aBrouwerFixedPoint Einstance. The repository discharges that instance for its Euclidean plane; it does not own Hatcher’s arbitrary-dimensional U041/U085/U086, nor the arbitrary-dimensional no-retraction clause of U025.- TauCeti was checked at
T=2db3a983be93975cbf1d54bcc7d6ae1b97830856(Apache-2.0; Lean 4.34.0-rc2; Mathlib5fcc6656691ed31965746c369f41fa75e567ac9d). Its topology stack imports singular-homology/fundamental-group infrastructure but no checked declaration was found for Hurewicz H₁, sphere homology/degree, cellular homology, singular Mayer–Vietoris, Alexander duality, Borsuk–Ulam, simplicial approximation, or Lefschetz fixed point. - Broad web/GitHub searches on 2026-09-07 found the complete Lean-4 Brouwer package above, but no completed Lean-4 owner for Hurewicz H₁, singular-homology Mayer–Vietoris/cellular homology, Borsuk–Ulam, simplicial approximation, or Lefschetz fixed point. Older Lean-3 sphere-homology/Brouwer developments and theorem statements/placeholders are not credited.
- U087 is deliberately positive:
Real.nonempty_algEquiv_orproves every algebraic real field extension is ℝ or ℂ. A finite-dimensional commutative unital real division algebra is an algebraic field extension, so the source theorem is a direct specialization of this stronger pinned theorem. N=2026-09-07denotes a dated unmatched result after the prescribed search layers. Strict whole-row semantics are applied uniformly: specializations, adjacent algebra, isolated clauses/examples, and unbridged alternative representations do not count.
Definition — Δ-complex structure
A Δ-complex structure on X consists of characteristic maps σ_α:Δ^n→X whose open simplices map injectively and partition X, whose face restrictions are other characteristic maps, and whose topology is generated by these maps.
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 Δ-complex structure on X consists of characteristic maps σ_α:Δ^n→X whose open simplices map injectively and partition X, whose face restrictions are other characteristic maps, and whose topology is generated by these maps. Pinned/current Mathlib has abstract simplicial-complex and simplicial-set APIs but no Δ-complex structure with Hatcher’s face-identification topology. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — simplicial chain complex and simplicial homology
For a Δ-complex X, Δ_n(X) is the free abelian group on oriented n-simplices; the alternating face boundary makes Δ_*(X) a chain complex, and its homology is simplicial homology.
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 Δ-complex X, Δ_n(X) is the free abelian group on oriented n-simplices; the alternating face boundary makes Δ_*(X) a chain complex, and its homology is simplicial homology. SSet.chainComplex is a simplicial-set chain complex, not the simplicial chain complex of a Hatcher Δ-complex; no checked Δ-complex↔︎simplicial-set bridge was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 2.1
For the simplicial boundary operators, ∂_{n-1}∂_n=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: For the simplicial boundary operators, ∂_{n-1}∂_n=0. SSet.ιChainComplex_d and HomologicalComplex.d_comp_d prove the analogous square-zero statement after one already has a simplicial-set/chain-complex model, but no checked Hatcher Δ-complex bridge owns this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — chain complex, cycles, boundaries, and homology classes
A sequence …→C_{n+1}→^{∂_{n+1}}C_n→^{∂n}C{n−1}→… with ∂n∂{n+1}=0 is a chain complex. Its n-th homology is H_n=ker∂n/im∂{n+1}; elements of ker∂n are cycles, elements of im∂{n+1} are boundaries, and cycles representing the same class are homologous.
Formalized. Mathlib/Algebra/Homology/HomologicalComplex.lean::HomologicalComplex, HomologicalComplex.d_comp_d; Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.cycles, HomologicalComplex.homology — Mathlib’s homological-complex object is a sequence with square-zero differential; in an abelian category its cycles are kernels and its homology object is the usual cycles modulo boundaries, exactly the source chain-complex/homology interface.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 2.2
For the simplicial circle with one vertex and one edge, the boundary map is zero. Hence H_nΔ(S1)≅ℤ for n=0,1 and H_nΔ(S1)=0 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: For the simplicial circle with one vertex and one edge, the boundary map is zero. Hence H_nΔ(S1)≅ℤ for n=0,1 and H_nΔ(S1)=0 for n≥2. No checked declaration computes the simplicial homology of Hatcher’s displayed one-vertex circle Δ-complex. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.3
For the standard Δ-complex structure on the torus T, H_1^Δ(T)≅ℤ⊕ℤ with basis [a],[b], H_0Δ(T)≅H_2Δ(T)≅ℤ, and H_n^Δ(T)=0 for n≥3.
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 the standard Δ-complex structure on the torus T, H_1^Δ(T)≅ℤ⊕ℤ with basis [a],[b], H_0Δ(T)≅H_2Δ(T)≅ℤ, and H_n^Δ(T)=0 for n≥3. No checked declaration computes the simplicial homology of Hatcher’s displayed torus Δ-complex. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.4
X = ℝP^{2}, as pictured earlier, with two vertices ν and w, three edges a, b, and c, and two 2 simplices U and L. Thus H_{1}^{Δ} (X) ≅ ℤ_{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: X = ℝP^{2}, as pictured earlier, with two vertices ν and w, three edges a, b, and c, and two 2 simplices U and L. Thus H_{1}^{Δ} (X) ≅ ℤ_{2}. No checked declaration computes H₁ of Hatcher’s displayed projective-plane Δ-complex as ℤ/2. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.5
We can obtain a Δ-complex structure on S^{n} by taking two copies of Δ^{n} and identifying their boundaries via the identity map. Labeling these two n-simplices U and L, then it is obvious that ker ∂{n} is infinite cyclic generated by U - L. Thus H{n}^{Δ} (S^{n}) ≅ ℤ for this Δ-complex structure on S^{n}. Computing the other homology groups would be more difficult.
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: We can obtain a Δ-complex structure on S^{n} by taking two copies of Δ^{n} and identifying their boundaries via the identity map. Labeling these two n-simplices U and L, then it is obvious that ker ∂{n} is infinite cyclic generated by U - L. Thus H{n}^{Δ} (S^{n}) ≅ ℤ for this Δ-complex structure on S^{n}. Computing the other homology groups would be more difficult. No checked declaration computes the simplicial homology of the two-n-simplex Δ-complex model of Sⁿ. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — simplicial complex
A simplicial complex is a Δ-complex whose simplices are uniquely determined by their vertices: each n-simplex has n+1 distinct vertices, no other n-simplex has the same vertex set, and every nonempty subset of a simplex’s vertices spans a simplex.
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 simplicial complex is a Δ-complex whose simplices are uniquely determined by their vertices: each n-simplex has n+1 distinct vertices, no other n-simplex has the same vertex set, and every nonempty subset of a simplex’s vertices spans a simplex. AbstractSimplicialComplex records downward-closed finite vertex sets, but it does not itself supply Hatcher’s Δ-complex/topological realization structure; no checked equivalence bridge was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — singular simplex and singular chains
A singular n-simplex in X is a continuous σ:Δ^n→X. C_n(X) is the free abelian group on singular n-simplices, whose elements are singular n-chains.
Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::TopCat.toSSetObjEquiv; Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.chainComplex, SSet.ιChainComplex — The singular simplicial set has n-simplices exactly the continuous maps from the standard n-simplex to X. With coefficient object ℤ in Ab, the simplicial chain group is the coproduct of copies of ℤ indexed by these simplices, i.e. the free abelian group of singular n-chains.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — singular homology
The alternating face maps give the singular chain complex C_*(X); its homology H_n(X)=ker∂n/im∂{n+1} is singular homology.
Formalized. Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor, AlgebraicTopology.singularHomologyFunctor; Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.ιChainComplex_d — The singular chain complex is the simplicial chain complex of the singular simplicial set; ιChainComplex_d gives the alternating face differential and singularHomologyFunctor takes its homology.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 2.6
Corresponding to the decomposition of a space X into its pathcomponents X_{α} there is an isomorphism of H_{n} (X) with the direct sum { ⊕{α} H{n} (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: Corresponding to the decomposition of a space X into its pathcomponents X_{α} there is an isomorphism of H_{n} (X) with the direct sum { ⊕{α} H{n} (X_{α}) }. The pinned H₀ theorem decomposes degree zero by path components, but no checked theorem decomposes every singular Hₙ over arbitrary path components as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.7
If X is nonempty and path-connected, then H_{0} (X) ≅ ℤ. Hence for any space X, H_{0} (X) is a direct sum of ℤ^{′} s,, one for each path-component of X.
Formalized. Mathlib/AlgebraicTopology/SingularHomology/HomologyZero.lean::TopCat.singularHomology₀Iso, TopCat.singularHomology₀ε — The degree-zero singular homology object is isomorphic to the coproduct of one coefficient object for each ZerothHomotopy class, i.e. each path component. For a nonempty path-connected space the augmentation is an isomorphism, yielding ℤ with integral coefficients.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 2.8
If X is a point, then H_{n} (X) = 0 for n > 0 and H_{0} (X) ≅ ℤ
Formalized. Mathlib/AlgebraicTopology/SingularHomology/HomologyZero.lean::TopCat.singularHomology₀Iso; Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace — Specializing the H₀ coproduct formula to the one-point space gives one copy of ℤ. A point is totally disconnected, and the second theorem makes every positive-degree singular-homology object zero.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — induced singular chain map
A map f:X→Y induces f_♯:C_n(X)→C_n(Y) by sending each singular simplex σ to f∘σ and extending linearly; these maps satisfy f_♯∂=∂f_♯ and hence form a chain map.
Formalized. Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor; Mathlib/AlgebraicTopology/SimplicialSet/Homology/Basic.lean::SSet.chainComplexMap, SSet.ι_chainComplexMap_f — Functoriality gives the induced singular chain map. On each simplex generator ι_chainComplexMap_f sends the generator to its image under the simplicial-set map, which for the singular functor is postcomposition by the continuous map; as a chain-complex morphism it commutes with the differential.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — commutative diagram
A diagram is commutative when any two composable paths in the diagram with the same starting and ending points have equal composites.
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 diagram is commutative when any two composable paths in the diagram with the same starting and ending points have equal composites. Mathlib has commutative-square structures and functorial diagrams, but no checked predicate states Hatcher’s unrestricted “all directed paths with common endpoints have equal composites” diagram definition. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.9
A chain map between chain complexes induces homomorphisms between the homology groups of the two complexes.
Formalized. Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.homologyMap, HomologicalComplex.homologyFunctor — A chain-complex morphism induces the canonical morphism on each homology object, functorially.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 2.10
If two maps f, g: X {→ } Y are homotopic, then they induce the same homomorphism f_{} = g_{}: H_{n} (X) → H_{n} (Y).
Formalized. Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean::TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor — This theorem states exactly that homotopic maps of spaces induce equal maps on singular homology in every degree.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Corollary 2.11
The maps f_{*}: H_{n} (X) {→ } H_{n} (Y) induced by a homotopy equivalence 1 f: X {→ } Y are isomorphisms for all n.
Formalized. Mathlib/Topology/Homotopy/Equiv.lean::ContinuousMap.HomotopyEquiv; Mathlib/AlgebraicTopology/SingularHomology/HomotopyInvariance.lean::TopCat.Homotopy.congr_homologyMap_singularChainComplexFunctor; Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean::HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap_id — A homotopy equivalence supplies a continuous inverse and homotopies of both composites to the identities. Homotopy invariance plus functoriality makes the two induced homology maps inverse, hence isomorphisms in every degree.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 2.12
Chain-homotopic chain maps induce the same homomorphism on homology.
Formalized. Mathlib/Algebra/Homology/Homotopy.lean::Homotopy.homologyMap_eq — This is the generic chain-homotopy theorem: homotopic morphisms of homological complexes induce the same homology map.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — exact sequence
A sequence …→A_{n+1}→{α_{n+1}}A_n→{α_n}A_{n−1}→… is exact when ker α_n=im α_{n+1} for every n.
Formalized. Mathlib/Algebra/Exact/Basic.lean::Function.Exact — Function.Exact f g is defined by range(f)=preimage(g,{0}); for homomorphisms this is exactly im(f)=ker(g), the source exactness condition at every term.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — short exact sequence
An exact sequence 0→A→B→C→0 is called a short exact sequence.
Formalized. Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean::CategoryTheory.ShortComplex.ShortExact — A ShortExact short complex is exact with first map monic and second map epic, equivalent in abelian groups to an exact sequence 0→A→B→C→0.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 2.13
If (X,A) is a good pair with A nonempty, there is a natural long exact reduced homology sequence …→H̃_n(A)→H̃n(X)→H_n(X,A)→H̃{n-1}(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 (X,A) is a good pair with A nonempty, there is a natural long exact reduced homology sequence …→H̃_n(A)→H̃n(X)→H_n(X,A)→H̃{n-1}(A)→…. Pinned Mathlib has generic long exact homology for short exact chain complexes, but no relative singular homology of topological pairs/reduced-good-pair sequence is connected to it. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2.14
H̃{n} (S^{n}) ≅ ℤ and H̃{i} (S^{n}) = 0 for i ≠ 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: H̃{n} (S^{n}) ≅ ℤ and H̃{i} (S^{n}) = 0 for i ≠ n Neither pinned nor current Mathlib computes reduced singular homology of spheres in all degrees; searched Lean-4 external work did not supply a checked owner. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2.15
∂ D^{n} is not a retract of D^{n}. Hence every map f: D^{n} → D^{n} has a fixed 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: ∂ D^{n} is not a retract of D^{n}. Hence every map f: D^{n} → D^{n} has a fixed point. harfe/fixed-point-theorems-lean4@770940ddf9878cf61952ed53d910b92bca841838 proves Brouwer fixed point in finite-dimensional compact convex sets, but no checked arbitrary-dimensional no-retraction theorem accompanies it. e3c7230fe78d7b056a415d9ecae6f77887046b32 proves no-retraction/Brouwer only for the plane. The bundled row is therefore not promoted. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — relative homology
For A⊂X, the relative chain groups are C_n(X,A)=C_n(X)/C_n(A); the induced quotient boundary maps form the relative chain complex C_*(X,A), and H_n(X,A) is its homology.
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⊂X, the relative chain groups are C_n(X,A)=C_n(X)/C_n(A); the induced quotient boundary maps form the relative chain complex C_*(X,A), and H_n(X,A) is its homology. Current Mathlib H adds SSetPair.chainComplex/SSetPair.homology as quotient-relative simplicial-set homology, but no checked TopPair/singular bridge identifies this with Cₙ(X)/Cₙ(A). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — short exact sequence of chain complexes
A commutative diagram whose rows are chain complexes and whose columns 0→A_n→B_n→C_n→0 are exact is a short exact sequence 0→A→B→C→0 of chain complexes.
Formalized. Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean::HomologicalComplex.shortExact_iff_degreewise_shortExact; Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean::CategoryTheory.ShortComplex.ShortExact — Mathlib proves a short complex of chain complexes is short exact iff it is short exact in every degree, exactly the source commutative degreewise short-exact diagram.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — connecting homomorphism in homology
For a short exact sequence 0→A→B→C→0 of chain complexes, a cycle c∈C_n is lifted to b∈B_n, one writes ∂b=i(a), and the connecting map sends [c] to [a]∈H_{n−1}(A).
Formalized. Mathlib/Algebra/Homology/HomologySequence.lean::CategoryTheory.ShortComplex.ShortExact.δ — The connecting morphism of a short exact sequence of homological complexes is constructed by the snake-lemma lift/boundary procedure, the categorical form of Hatcher’s cycle-lift construction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 2.16
For every short exact sequence 0→A→B→C→0 of chain complexes, the associated sequence …→H_n(A)→H_n(B)→H_n(C)→H_{n-1}(A)→… is exact.
Formalized. Mathlib/Algebra/Homology/HomologySequence.lean::CategoryTheory.ShortComplex.ShortExact.homology_exact₁, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, CategoryTheory.ShortComplex.ShortExact.homology_exact₃ — These three exactness theorems are the consecutive pieces of the long exact homology sequence attached to every short exact sequence of homological complexes.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 2.17
For the pair (Dn,∂Dn), H_i(Dn,∂Dn)≅H̃_{i-1}(S^{n-1}); hence it is ℤ for i=n and 0 otherwise.
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 the pair (Dn,∂Dn), H_i(Dn,∂Dn)≅H̃_{i-1}(S^{n-1}); hence it is ℤ for i=n and 0 otherwise. The generic long exact sequence machinery is present, but no checked relative singular-homology computation of (Dⁿ,∂Dⁿ) and sphere bridge owns this example. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.18
Applying the long exact sequence of reduced homology groups to a pair (X, x_{0}) with x_{0} ∈ X yields isomorphisms H_{n} (X, x_{0}) ≅ H̃{n} (X) for all n since H̃{n} (x_{0}) = 0 for all 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: Applying the long exact sequence of reduced homology groups to a pair (X, x_{0}) with x_{0} ∈ X yields isomorphisms H_{n} (X, x_{0}) ≅ H̃{n} (X) for all n since H̃{n} (x_{0}) = 0 for all n. Current relative simplicial-set homology is not connected to topological pairs, and no checked theorem identifies Hₙ(X,x₀) with reduced singular homology. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.19
If two maps f, g: (X, A) → (Y, B) are homotopic through maps of pairs (X, A) → (Y, B), then f_{} = g_{}: H_{n} (X, A) {→ } H_{n} (Y, 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: If two maps f, g: (X, A) → (Y, B) are homotopic through maps of pairs (X, A) → (Y, B), then f_{} = g_{}: H_{n} (X, A) {→ } H_{n} (Y, B). Current SSetPair.homology has functorial maps, but no checked TopPair/singular bridge or relative topological homotopy-invariance theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2.20
Given subspaces Z ⊂ A ⊂ X such that the closure of Z is contained in the interior of A, then the inclusion (X - Z, A - Z) ↪ (X, A) induces isomorphisms H_{n} (X - Z, A - Z) {→ } H_{n} (X, A) for all n. Equivalently, for subspaces A, B ⊂ X whose interiors cover X, the inclusion (B, A ∩ B) ↪ (X, A) induces isomorphisms H_{n} (B, A ∩ B) {→ } H_{n} (X, A) for all 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: Given subspaces Z ⊂ A ⊂ X such that the closure of Z is contained in the interior of A, then the inclusion (X - Z, A - Z) ↪ (X, A) induces isomorphisms H_{n} (X - Z, A - Z) {→ } H_{n} (X, A) for all n. Equivalently, for subspaces A, B ⊂ X whose interiors cover X, the inclusion (B, A ∩ B) ↪ (X, A) induces isomorphisms H_{n} (B, A ∩ B) {→ } H_{n} (X, A) for all n. No checked Lean declaration proves singular-homology excision for topological pairs; the current SSetPair package does not include the required topological excision bridge. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.21
The inclusion ι: C_{n}^{U} (X) ↪ C_{n} (X) is a chain homotopy equivalence, that is, there is a chain map ρ: C_{n} (X) {→ } C_{n}^{U} (X) such that ι ρ and ρι are chain homotopic to the identity. Hence ι induces isomorphisms H_{n} ^ { {U } } (X) ≅ H_{n} (X) for all 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 inclusion ι: C_{n}^{U} (X) ↪ C_{n} (X) is a chain homotopy equivalence, that is, there is a chain map ρ: C_{n} (X) {→ } C_{n}^{U} (X) such that ι ρ and ρι are chain homotopic to the identity. Hence ι induces isomorphisms H_{n} ^ { {U } } (X) ≅ H_{n} (X) for all n. Generic chain-homotopy-equivalence APIs exist, but Hatcher’s small-singular-chain subcomplex and subdivision operator are not formalized. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — barycentric subdivision of a simplex
The barycenter of [v₀,…,v_n] is the point with all barycentric coordinates 1/(n+1). Its barycentric subdivision is obtained inductively by coning the barycentric subdivisions of the boundary faces to this barycenter.
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 barycenter of [v₀,…,v_n] is the point with all barycentric coordinates 1/(n+1). Its barycentric subdivision is obtained inductively by coning the barycentric subdivisions of the boundary faces to this barycenter. Simplicial geometry contains barycenters in other interfaces, but no checked Hatcher singular-simplex barycentric subdivision construction owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — barycentric subdivision chain map
The barycentric subdivision homomorphism S on singular chains is defined inductively by coning the subdivided boundary of a simplex to its barycenter; it is a chain map and is chain-homotopic to the identity.
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 barycentric subdivision homomorphism S on singular chains is defined inductively by coning the subdivided boundary of a simplex to its barycenter; it is a chain map and is chain-homotopic to the identity. No checked singular-chain barycentric subdivision map and chain homotopy to the identity was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.22
For a good pair (X,A), the quotient map q:(X,A)→(X/A,A/A) induces isomorphisms q_*:H_n(X,A)→H_n(X/A,A/A)≅H̃_n(X/A) for all 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 a good pair (X,A), the quotient map q:(X,A)→(X/A,A/A) induces isomorphisms q_*:H_n(X,A)→H_n(X/A,A/A)≅H̃_n(X/A) for all n. No checked good-pair quotient theorem for relative singular homology was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.23
The identity singular simplex i_n:Δn→Δn represents a generator of H_n(Δn,∂Δn), compatibly under the boundary isomorphism with ±i_{n-1}. Viewing S^n as two n-simplices glued along their boundaries, Δ_1n−Δ_2n represents a generator of H̃_n(S^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 identity singular simplex i_n:Δn→Δn represents a generator of H_n(Δn,∂Δn), compatibly under the boundary isomorphism with ±i_{n-1}. Viewing S^n as two n-simplices glued along their boundaries, Δ_1n−Δ_2n represents a generator of H̃_n(S^n). No checked relative singular-homology generator theorem for simplices/spheres was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2.24
If the CW complex X is the union of subcomplexes A and B, then the inclusion (B, A ∩ B) ↪ (X, A) induces isomorphisms H_{n} (B, A ∩ B) → H_{n} (X, A) for all 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 the CW complex X is the union of subcomplexes A and B, then the inclusion (B, A ∩ B) ↪ (X, A) induces isomorphisms H_{n} (B, A ∩ B) → H_{n} (X, A) for all n. CW-complex and generic homology infrastructure exist, but there is no checked singular excision theorem to instantiate the subcomplex corollary. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2.25
For a wedge sum ∨{α} X{α}, the inclusions i_{α} {: } X_{α} {↪ } ∨{α} X{α} induce an isomorphism { ⊕{α} i{α *}: ⊕{α} H̃{n} (X_{α}) → H̃{n} (∨{α} X_{α}) }, provided that the wedge sum is formed at basepoints x_{α} ∈ X_{α} such that the pairs (X_{α}, x_{α}) are good.
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 wedge sum ∨{α} X{α}, the inclusions i_{α} {: } X_{α} {↪ } ∨{α} X{α} induce an isomorphism { ⊕{α} i{α }: ⊕{α} H̃*{n} (X_{α}) → H̃{n} (∨{α} X{α}) }, provided that the wedge sum is formed at basepoints x{α} ∈ X_{α} such that the pairs (X_{α}, x_{α}) are good. No checked reduced-singular-homology wedge/additivity theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2.26
If nonempty open sets U ⊂ ℝ^{m} and V ⊂ ℝ^{n} are homeomorphic, then 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: If nonempty open sets U ⊂ ℝ^{m} and V ⊂ ℝ^{n} are homeomorphic, then m = n. Current Mathlib has no invariance-of-domain theorem. e3c7230fe78d7b056a415d9ecae6f77887046b32 exposes an invariance-of-domain theorem conditional on a BrouwerFixedPoint E instance and discharges that condition only in its planar development, so it does not own arbitrary m,n. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — local homology at a point
The local homology groups of X at x are H_n(X,X−{x}); by excision they depend only on the local topology of X near x (when points are closed).
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 local homology groups of X at x are H_n(X,X−{x}); by excision they depend only on the local topology of X near x (when points are closed). No checked local singular-homology object Hₙ(X,X−{x}) or excision/locality theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/convention — naturality
Naturality means that a map of the underlying spaces or pairs induces a commutative diagram between the associated homological constructions.
Formalized. Mathlib/CategoryTheory/NatTrans.lean::CategoryTheory.NatTrans.naturality — Naturality is represented exactly by the commuting naturality square for every morphism; applying this to homology functors gives the source convention for maps of spaces or pairs.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 2.27
The homomorphisms H_{n}^{Δ} (X, A) {→ } H_{n} (X, A) are isomorphisms for all n and all Δ-complex pairs (X, 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: The homomorphisms H_{n}^{Δ} (X, A) {→ } H_{n} (X, A) are isomorphisms for all n and all Δ-complex pairs (X, A). Mathlib has simplicial-set and singular homology separately, but no checked theorem identifies Hatcher Δ-complex (relative) simplicial homology with singular homology. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Betti numbers and torsion coefficients
When H_n(X) is finitely generated and written as a direct sum of cyclic groups, the number of ℤ summands is the n-th Betti number, and the orders of the finite cyclic summands are the torsion coefficients.
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 H_n(X) is finitely generated and written as a direct sum of cyclic groups, the number of ℤ summands is the n-th Betti number, and the orders of the finite cyclic summands are the torsion coefficients. Pinned finitely-generated-abelian-group structure theory and free-rank/torsion APIs are adjacent, but no checked invariant-factor/torsion-coefficient interface matches Hatcher’s exact definitions for homology groups. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — degree of a map Sⁿ→Sⁿ
For f:Sn→Sn with n>0, f_* on H_n(S^n)≅ℤ is multiplication by a unique integer d; this integer is the degree deg f.
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 f:Sn→Sn with n>0, f_* on H_n(S^n)≅ℤ is multiplication by a unique integer d; this integer is the degree deg f. No checked degree-of-sphere-map definition through top singular homology was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2.28
S^{n} has a continuous field of nonzero tangent vectors iff n is odd.
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^{n} has a continuous field of nonzero tangent vectors iff n is odd. No checked theorem classifies nowhere-zero continuous tangent vector fields on spheres by parity. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.29
ℤ_{2} is the only nontrivial group that can act freely on S^{n} if n is even.
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 the only nontrivial group that can act freely on S^{n} if n is even. No checked theorem classifies free group actions on even-dimensional spheres as stated. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.30
If f:Sn→Sn, n>0, and y has finite preimage {x_1,…,x_m} with local degrees defined as above, then deg f=Σ_i deg(f at x_i).
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 f:Sn→Sn, n>0, and y has finite preimage {x_1,…,x_m} with local degrees defined as above, then deg f=Σ_i deg(f at x_i). No checked local-degree theory and global degree-sum theorem for sphere maps was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.31
We can use this result to construct a map S^{n} → S^{n} of any given degree, for each n ≥ 1. Thus we can produce a map S^{n} → S^{n} of degree ± k.
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: We can use this result to construct a map S^{n} → S^{n} of any given degree, for each n ≥ 1. Thus we can produce a map S^{n} → S^{n} of degree ± k. No checked sphere-degree theory exists from which to construct maps of arbitrary prescribed degree. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.32
For f:S1→S1, f(z)=z^k, one has deg f=k for every integer k. For k>0 each regular value has k preimages, each of local degree +1; negative k follows by composing with the degree −1 reflection z↦z^{-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: For f:S1→S1, f(z)=z^k, one has deg f=k for every integer k. For k>0 each regular value has k preimages, each of local degree +1; negative k follows by composing with the degree −1 reflection z↦z^{-1}. Covering/power maps of the circle exist, but no checked homological degree theorem identifies z↦zᵏ with degree k. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.33
deg S f = deg f, where S f: S^{n + 1} {→ } S^{n + 1} is the suspension of the map f: S^{n} {→ } S^{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: deg S f = deg f, where S f: S^{n + 1} {→ } S^{n + 1} is the suspension of the map f: S^{n} {→ } S^{n}. No checked suspension-of-sphere-map degree theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 2.34
For a CW complex X: (a) H_k(Xn,X{n-1}) is 0 for k≠n and is free abelian on the n-cells for k=n; (b) H_k(X^n)=0 for k>n, so H_k(X)=0 above dim X when X is finite-dimensional; (c) H_k(X^n)→H_k(X) is an isomorphism for k<n and surjective for k=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 a CW complex X: (a) H_k(Xn,X{n-1}) is 0 for k≠n and is free abelian on the n-cells for k=n; (b) H_k(X^n)=0 for k>n, so H_k(X)=0 above dim X when X is finite-dimensional; (c) H_k(X^n)→H_k(X) is an isomorphism for k<n and surjective for k=n. CW-complex skeleta are formalized, but no checked relative singular/cellular homology theorem proves the bundled skeletal vanishing and stabilization statements. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cellular chain complex and cellular homology
The groups H_n(Xn,X{n−1}) with connecting maps from the skeletal long exact sequences form the cellular chain complex; its homology is cellular homology.
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 groups H_n(Xn,X{n−1}) with connecting maps from the skeletal long exact sequences form the cellular chain complex; its homology is cellular homology. No checked cellular chain complex constructed from Hₙ(Xⁿ,Xⁿ⁻¹) exists. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2.35
H_{n}^{CW} (X) ≅ H_{n} (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: H_{n}^{CW} (X) ≅ H_{n} (X) No checked cellular-homology≅singular-homology theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.36
For the closed orientable genus-g surface M_g with one 0-cell, 2g 1-cells, and one 2-cell, the cellular chain complex is 0→ℤ→ℤ^{2g}→ℤ→0 and both differentials vanish. Thus H_0(M_g)≅H_2(M_g)≅ℤ and H_1(M_g)≅ℤ^{2g}.
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 the closed orientable genus-g surface M_g with one 0-cell, 2g 1-cells, and one 2-cell, the cellular chain complex is 0→ℤ→ℤ^{2g}→ℤ→0 and both differentials vanish. Thus H_0(M_g)≅H_2(M_g)≅ℤ and H_1(M_g)≅ℤ^{2g}. No checked cellular/singular homology computation of closed orientable surfaces was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.37
The closed nonorientable surface N_{g} of genus g has a cell structure with one 0 cell, g 1-cells, and one 2 cell attached by the word a_{1}^{2} a_{2}^{2} … a_{g}^{2}. If we change the basis for ℤ^{g} by replacing the last standard basis element (0, …, 0, 1) by (1, …, 1), we see that H_{1} (N_{g}) ≅ ℤ^{g - 1} ⊕ ℤ_{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: The closed nonorientable surface N_{g} of genus g has a cell structure with one 0 cell, g 1-cells, and one 2 cell attached by the word a_{1}^{2} a_{2}^{2} … a_{g}^{2}. If we change the basis for ℤ^{g} by replacing the last standard basis element (0, …, 0, 1) by (1, …, 1), we see that H_{1} (N_{g}) ≅ ℤ^{g - 1} ⊕ ℤ_{2}. No checked cellular/singular homology computation of closed nonorientable surfaces was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.38
An Acyclic Space. Let X be obtained from S^{1} ∨ S^{1} by attaching two 2 cells by the words a^{5} b^{- 3} and b^{3} (a b)^{- 2}. Then d_{2}: ℤ^{2} → ℤ^{2} has matrix binom {5 - 2 } {- 3 }, with the two columns coming from abelianizing a^{5} b^{- 3} and b^{3} (a b)^{- 2} to 5 a - 3 b and - 2 a + b, in additive notation. The matrix has determinant^{- 1}, so d_{2} is an isomorphism and H̃_{i} (X) = 0 for all i. Such a space X is called acyclic.
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: An Acyclic Space. Let X be obtained from S^{1} ∨ S^{1} by attaching two 2 cells by the words a^{5} b^{- 3} and b^{3} (a b)^{- 2}. Then d_{2}: ℤ^{2} → ℤ^{2} has matrix binom {5 - 2 } {- 3 }, with the two columns coming from abelianizing a^{5} b^{- 3} and b^{3} (a b)^{- 2} to 5 a - 3 b and - 2 a + b, in additive notation. The matrix has determinant^{- 1}, so d_{2} is an isomorphism and H̃_{i} (X) = 0 for all i. Such a space X is called acyclic. No checked implementation owns Hatcher’s specific acyclic 2-complex example and determinant computation. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.39
A 3 dimensional torus T^{3} = S^{1} {× } S^{1} {× } S^{1} can be constructed from a cube by identifying each pair of opposite square faces as in the first of the two figures. Since the cellular boundary maps are all zero, we deduce that H_{i} (T^{3}) is ℤ for i = 0, 3, ℤ^{3} for i = 1, 2, and 0 for i > 3.
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 3 dimensional torus T^{3} = S^{1} {× } S^{1} {× } S^{1} can be constructed from a cube by identifying each pair of opposite square faces as in the first of the two figures. Since the cellular boundary maps are all zero, we deduce that H_{i} (T^{3}) is ℤ for i = 0, 3, ℤ^{3} for i = 1, 2, and 0 for i > 3. No checked singular/cellular homology computation of T³ was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.40
Moore Spaces. Given an abelian group G and an integer n ≥ 1, we will construct a CW complex X such that H_{n} (X) ≅ G and H̃_{i} (X) = 0 for i ≠ n. Such a space is called a Moore space, commonly written M (G, n) to indicate the dependence on G and n. It is probably best for the definition of a Moore space to include the condition that M (G, n) be simply-connected if n > 1. The spaces we construct will have this property.
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: Moore Spaces. Given an abelian group G and an integer n ≥ 1, we will construct a CW complex X such that H_{n} (X) ≅ G and H̃_{i} (X) = 0 for i ≠ n. Such a space is called a Moore space, commonly written M (G, n) to indicate the dependence on G and n. It is probably best for the definition of a Moore space to include the condition that M (G, n) be simply-connected if n > 1. The spaces we construct will have this property. No checked Moore-space construction with prescribed homology and simple connectivity was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.41
By taking a wedge sum of the Moore spaces constructed in the preceding example for varying n we obtain a connected CW complex with any prescribed sequence of homology groups in dimensions 1, 2, 3, ….
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: By taking a wedge sum of the Moore spaces constructed in the preceding example for varying n we obtain a connected CW complex with any prescribed sequence of homology groups in dimensions 1, 2, 3, …. No checked wedge-of-Moore-spaces realization theorem for arbitrary positive homology sequences was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.42
ℝP^n has one cell in each dimension 0≤k≤n, with cellular differential d_k multiplication by 1+(−1)^k: zero for k odd and multiplication by 2 for k even. Thus H_0≅ℤ; H_k≅ℤ_2 for odd 0<k<n; H_n≅ℤ when n is odd; all other H_k vanish.
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 has one cell in each dimension 0≤k≤n, with cellular differential d_k multiplication by 1+(−1)^k: zero for k odd and multiplication by 2 for k even. Thus H_0≅ℤ; H_k≅ℤ_2 for odd 0<k<n; H_n≅ℤ when n is odd; all other H_k vanish. No checked integral cellular-homology computation of ℝPⁿ was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.43
For L=L_m(ℓ₁,…,ℓ_n)=S^{2n−1}/ℤ_m, the free action gives a CW structure with one cell in each dimension 0,…,2n−1 and cellular differentials alternating 0 and multiplication by m. Hence H_0≅H_{2n−1}≅ℤ, H_k≅ℤ_m for odd 0<k<2n−1, and H_k=0 otherwise.
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 L=L_m(ℓ₁,…,ℓ_n)=S^{2n−1}/ℤ_m, the free action gives a CW structure with one cell in each dimension 0,…,2n−1 and cellular differentials alternating 0 and multiplication by m. Hence H_0≅H_{2n−1}≅ℤ, H_k≅ℤ_m for odd 0<k<2n−1, and H_k=0 otherwise. No checked cellular-homology computation of lens spaces was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Euler characteristic
For a finite CW complex X with c_n n-cells, χ(X)=Σ_n(−1)^n c_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 a finite CW complex X with c_n n-cells, χ(X)=Σ_n(−1)^n c_n. HomologicalComplex.eulerChar defines an alternating rank sum for an algebraic complex, but no checked CW-cell-count Euler-characteristic definition/bridge realizes this source row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2.44
{ χ (X) = ∑{n} (- 1)^{n} r a n k H{n} (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: { χ (X) = ∑{n} (- 1)^{n} r a n k H{n} (X). } Pinned/current HomologicalComplex.homologyEulerChar gives the alternating rank sum of homology objects, but no checked theorem identifies it with CW cell-count Euler characteristic (indeed the generic file has no eulerChar=homologyEulerChar theorem). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2.45
If a finite-dimensional CW complex X is a K (G, 1), then the group G = π_{1} (X) must be torsionfree.
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 finite-dimensional CW complex X is a K (G, 1), then the group G = π_{1} (X) must be torsionfree. No checked theorem proves that a finite-dimensional CW K(G,1) has torsion-free fundamental group. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — Mayer–Vietoris sequence
If X is the union of the interiors of A and B, homology has the long exact Mayer–Vietoris sequence linking A∩B, A⊕B, and 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: If X is the union of the interiors of A and B, homology has the long exact Mayer–Vietoris sequence linking A∩B, A⊕B, and X. Mathlib’s Mayer–Vietoris developments are for sheaf cohomology, not singular homology; no checked singular-homology sequence was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.46
Take X = S^{n} with A and B the northern and southern hemispheres, so that A ∩ B = S^{n - 1}. Then in the reduced Mayer–Vietoris sequence the terms H̃{i} (A) ⊕ H̃{i} (B) are zero, so we obtain isomorphisms H̃{i} (S^{n}) ≅ H̃{i - 1} (S^{n - 1}). This gives another way of calculating the homology groups of S^{n} by induction.
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: Take X = S^{n} with A and B the northern and southern hemispheres, so that A ∩ B = S^{n - 1}. Then in the reduced Mayer–Vietoris sequence the terms H̃{i} (A) ⊕ H̃{i} (B) are zero, so we obtain isomorphisms H̃{i} (S^{n}) ≅ H̃{i - 1} (S^{n - 1}). This gives another way of calculating the homology groups of S^{n} by induction. The sphere computation via Mayer–Vietoris is unavailable because the required singular-homology Mayer–Vietoris sequence is not formalized. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.47
Writing the Klein bottle K as two Möbius bands glued along their boundary, Mayer–Vietoris has map ℤ→ℤ⊕ℤ, 1↦(2,−2). Hence H_2(K)=0, H_1(K)≅ℤ⊕ℤ_2, and H_k(K)=0 for k>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: Writing the Klein bottle K as two Möbius bands glued along their boundary, Mayer–Vietoris has map ℤ→ℤ⊕ℤ, 1↦(2,−2). Hence H_2(K)=0, H_1(K)≅ℤ⊕ℤ_2, and H_k(K)=0 for k>2. No checked Klein-bottle singular-homology/Mayer–Vietoris computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.48
For maps f,g:X→Y, let Z be obtained from X×I⊔Y by (x,0)∼f(x), (x,1)∼g(x). There is a long exact sequence …→H_n(X)→{f_−g_}H_n(Y)→H_n(Z)→H_{n−1}(X)→{f_−g_}H_{n−1}(Y)→…. When f=id, Z is the mapping torus 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: For maps f,g:X→Y, let Z be obtained from X×I⊔Y by (x,0)∼f(x), (x,1)∼g(x). There is a long exact sequence …→H_n(X)→{f_−g_}H_n(Y)→H_n(Z)→H_{n−1}(X)→{f_−g_}H_{n−1}(Y)→…. When f=id, Z is the mapping torus of g. No checked mapping-cylinder/mapping-torus singular-homology exact sequence with f_−g_ was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — homology with coefficients
For an abelian group G, singular chains C_n(X;G) use coefficients in G; the same boundary defines H_n(X;G), with analogous relative and reduced 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 an abelian group G, singular chains C_n(X;G) use coefficients in G; the same boundary defines H_n(X;G), with analogous relative and reduced groups. singularChainComplexFunctor accepts arbitrary coefficient objects, but the row also requires analogous relative and reduced groups. Current H has relative simplicial-set coefficients only and lacks the topological-pair bridge, so the bundle is not promoted. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 2.49
If f: S^{k} {→ } S^{k} has degree m, then f_{*}: H_{k} (S^{k}; G) {→ } H_{k} (S^{k}; G) is multiplication by m.
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 f: S^{k} {→ } S^{k} has degree m, then f_{*}: H_{k} (S^{k}; G) {→ } H_{k} (S^{k}; G) is multiplication by m. No checked degree theory with coefficients proves multiplication by degree on Hₖ(Sᵏ;G). Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.50
For ℝP^n with coefficients in a field F, the cellular differentials alternate between 0 and multiplication by 2. If char F=2 then H_k(ℝP^n;F)≅F for 0≤k≤n; if char F≠2, only H_0 and, when n is odd, H_n are F.
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 ℝP^n with coefficients in a field F, the cellular differentials alternate between 0 and multiplication by 2. If char F=2 then H_k(ℝP^n;F)≅F for 0≤k≤n; if char F≠2, only H_0 and, when n is odd, H_n are F. No checked coefficient-homology computation of ℝPⁿ over fields was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2.51
For the Moore space X=M(ℤ_m,n)=S^n∪m e^{n+1}, the quotient f:X→X/Sn=S{n+1} induces zero on reduced integral homology, but with ℤ_m coefficients f*:H_{n+1}(X;ℤ_m)→H_{n+1}(S^{n+1};ℤ_m) is injective (indeed an isomorphism), so f is not nullhomotopic.
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 the Moore space X=M(ℤ_m,n)=S^n∪*m e^{n+1}, the quotient f:X→X/Sn=S{n+1} induces zero on reduced integral homology, but with ℤ_m coefficients f**:H_{n+1}(X;ℤ_m)→H_{n+1}(S^{n+1};ℤ_m) is injective (indeed an isomorphism), so f is not nullhomotopic. No checked Moore-space coefficient-homology example or non-nullhomotopy consequence was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — reduced homology theory
A reduced homology theory on based CW complexes is a sequence of covariant functors satisfying homotopy invariance, exactness, suspension, wedge/additivity, and the dimension axiom as stated in §2.3.
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 reduced homology theory on based CW complexes is a sequence of covariant functors satisfying homotopy invariance, exactness, suspension, wedge/additivity, and the dimension axiom as stated in §2.3. TopPair.HomologyPretheory packages relative/absolute functors and boundary maps, and IsHomotopyInvariant one axiom, but exactness, suspension, wedge/additivity, and dimension axioms are not packaged; the full reduced-homology-theory row is absent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Convention — negative homological degrees
Negative homological subscripts are allowed in the axiomatic formalism; ordinary singular homology is zero in negative dimensions by definition.
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: Negative homological subscripts are allowed in the axiomatic formalism; ordinary singular homology is zero in negative dimensions by definition. Pinned singular homology is indexed by ℕ rather than by all integers with explicit zero objects in negative degrees, so the stated negative-degree convention is not represented exactly. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — coefficients of a homology theory
For a homology theory h and its reduced version h̃, the groups h_n(x₀)≅h̃_n(S⁰) are called the coefficients of the theory.
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 homology theory h and its reduced version h̃, the groups h_n(x₀)≅h̃_n(S⁰) are called the coefficients of the theory. Without the full reduced-homology-theory interface, no checked declaration identifies coefficients as hₙ(point)≅h̃ₙ(S⁰) in the source axiomatic setting. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — category
A category has objects, sets Mor(X,Y), associative composition, and identity morphisms for every object.
Formalized. Mathlib/CategoryTheory/Category/Basic.lean::CategoryTheory.Category — The category structure supplies morphism types, identities, associative composition, and the identity laws, matching the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — functor
A functor F:C→D maps objects and morphisms, preserving identities and composition; contravariant functors reverse morphisms.
Formalized. Mathlib/CategoryTheory/Functor/Basic.lean::CategoryTheory.Functor; Mathlib/CategoryTheory/Opposites.lean::CategoryTheory.Functor.leftOp — A Functor maps objects and morphisms and preserves identities and composition. Opposite-category functors encode contravariance and reverse morphism direction.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — natural transformation
For functors F,G:C→D, a natural transformation T:F⇒G assigns T_X:F(X)→G(X) so every morphism f:X→Y gives G(f)T_X=T_YF(f).
Formalized. Mathlib/CategoryTheory/NatTrans.lean::CategoryTheory.NatTrans, CategoryTheory.NatTrans.naturality — A natural transformation consists of one component morphism at each object together with exactly the source naturality equation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Theorem 2A.1
By regarding loops as singular 1 cycles, we obtain a homomorphism h {: π_{1} (X, x_{0}) } {→ } H_{1} (X). If X is path-connected, then h is surjective and has kernel the commutator subgroup of π_{1} (X), so h induces an isomorphism from the abelianization of π_{1} (X) onto H_{1} (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: By regarding loops as singular 1 cycles, we obtain a homomorphism h {: π_{1} (X, x_{0}) } {→ } H_{1} (X). If X is path-connected, then h is surjective and has kernel the commutator subgroup of π_{1} (X), so h induces an isomorphism from the abelianization of π_{1} (X) onto H_{1} (X). No checked Hurewicz degree-one theorem identifies singular H₁ of a path-connected space with the abelianization of π₁. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2A.2
For the closed orientable surface M of genus g, the abelianization of π_{1} (M) is ℤ^{2 g}, the product of 2 g copies of ℤ, and a basis for H_{1} (M) consists of the 1 cycles represented by the 1 cells of M in its standard CW structure. The loop α_{i}^{′} represents the same homology class as α_{i} since the region between γ_{i} and α_{i} ∪ α_{i}^{′} provides a homotopy between γ_{i} and a product of two loops homotopic to α_{i} and the inverse of α_{i}^{′}, so α_{i} - α_{i}^{′} ∼ γ_{i} ∼ 0, hence α_{i} ∼ α_{i}^{′}.
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 the closed orientable surface M of genus g, the abelianization of π_{1} (M) is ℤ^{2 g}, the product of 2 g copies of ℤ, and a basis for H_{1} (M) consists of the 1 cycles represented by the 1 cells of M in its standard CW structure. The loop α_{i}^{′} represents the same homology class as α_{i} since the region between γ_{i} and α_{i} ∪ α_{i}^{′} provides a homotopy between γ_{i} and a product of two loops homotopic to α_{i} and the inverse of α_{i}^{′}, so α_{i} - α_{i}^{′} ∼ γ_{i} ∼ 0, hence α_{i} ∼ α_{i}^{′}. No checked singular-homology/abelianization computation of an orientable surface with the named cellular cycles was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 2B.1
- For an embedding h {: } D^{k} {→ } S^{n}, H̃{i} (S^{n} - h (D^{k})) = 0 for all i. (b) For an embedding h: S^{k} {→ } S^{n} with k < n, H̃{i} {(} S^{n} - h (S^{k}) {) } is ℤ for i = n - k - 1 and 0 otherwise.
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) For an embedding h {: } D^{k} {→ } S^{n}, H̃{i} (S^{n} - h (D^{k})) = 0 for all i. (b) For an embedding h: S^{k} {→ } S^{n} with k < n, H̃{i} {(} S^{n} - h (S^{k}) {) } is ℤ for i = n - k - 1 and 0 otherwise. No checked Alexander-duality/complement-homology theorem for embedded disks or spheres was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2B.2
The Alexander Horned Sphere. This is a subspace S ⊂ ℝ^{3} homeomorphic to S^{2} such that the unbounded component of ℝ^{3} - S is not simply-connected as it is for the standard S^{2} ⊂ ℝ^{3}. We will construct S by defining a sequence of compact subspaces X_{0} ⊃ X_{1} ⊃ … of ℝ^{3} whose intersection is homeomorphic to a ball, and then S will be the boundary sphere of this ball.
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 Alexander Horned Sphere. This is a subspace S ⊂ ℝ^{3} homeomorphic to S^{2} such that the unbounded component of ℝ^{3} - S is not simply-connected as it is for the standard S^{2} ⊂ ℝ^{3}. We will construct S by defining a sequence of compact subspaces X_{0} ⊃ X_{1} ⊃ … of ℝ^{3} whose intersection is homeomorphic to a ball, and then S will be the boundary sphere of this ball. No checked construction of the Alexander horned sphere with the stated complement property was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2B.3
If U is an open set in ℝ^{n} and h: U → ℝ^{n} is an embedding, or more generally just a continuous injection, then the image h (U) is an open set in ℝ^{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 U is an open set in ℝ^{n} and h: U → ℝ^{n} is an embedding, or more generally just a continuous injection, then the image h (U) is an open set in ℝ^{n}. Current Mathlib issue/search state still lacks invariance of domain; e3c7230fe78d7b056a415d9ecae6f77887046b32 proves a conditional finite-dimensional inner-product-space form but only has the required Brouwer instance in dimension two. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2B.4
If M is a compact n manifold and N is a connected n manifold, then an embedding h: M → N must be surjective, hence a homeomorphism.
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 M is a compact n manifold and N is a connected n manifold, then an embedding h: M → N must be surjective, hence a homeomorphism. No checked arbitrary-dimensional manifold corollary of invariance of domain was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2B.5
R and ℂ are the only finite-dimensional division algebras over R which are commutative and have an identity.
Formalized. Mathlib/RingTheory/Algebraic/Integral.lean::Algebra.IsAlgebraic.of_finite; Mathlib/Analysis/Complex/Polynomial/Basic.lean::Real.nonempty_algEquiv_or — Algebra.IsAlgebraic.of_finite makes every module-finite algebra algebraic. Thus a finite-dimensional commutative unital real division algebra is an algebraic field extension of ℝ, and Real.nonempty_algEquiv_or classifies it as ℝ or ℂ.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Proposition 2B.6
An odd map f: S^{n} {→ } S^{n}, satisfying f (- x) = - f (x) for all x, must have odd degree.
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: An odd map f: S^{n} {→ } S^{n}, satisfying f (- x) = - f (x) for all x, must have odd degree. No checked sphere degree theory proves that every antipode-equivariant self-map has odd degree. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — two-sheeted transfer chain map
For a two-sheeted covering p:X̃→X with ℤ₂ coefficients, τ:C_n(X;ℤ₂)→C_n(X̃;ℤ₂) sends each singular simplex to the sum of its two lifts; 0→C_n(X;ℤ₂)→^τ C_n(X̃;ℤ₂)→^{p_♯}C_n(X;ℤ₂)→0 is a short exact sequence of chain complexes.
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 two-sheeted covering p:X̃→X with ℤ₂ coefficients, τ:C_n(X;ℤ₂)→C_n(X̃;ℤ₂) sends each singular simplex to the sum of its two lifts; 0→C_n(X;ℤ₂)→^τ C_n(X̃;ℤ₂)→^{p_♯}C_n(X;ℤ₂)→0 is a short exact sequence of chain complexes. Covering-space lifting exists, but no checked two-sheeted transfer singular-chain map with ℤ₂ coefficients and short-exactness theorem was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — transfer sequence for a double cover
The long exact homology sequence induced by the two-sheeted transfer short exact sequence is called the transfer sequence; its first map is the induced transfer homomorphism τ_*.
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 long exact homology sequence induced by the two-sheeted transfer short exact sequence is called the transfer sequence; its first map is the induced transfer homomorphism τ_*. The generic long exact sequence of a short exact chain complex is formalized, but the required transfer short exact sequence is not, so the transfer sequence itself has no complete owner. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 2B.7
For every map g: S^{n} {→ } ℝ^{n} there exists a point x ∈ S^{n} with g (x) = 1 g (- 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 map g: S^{n} {→ } ℝ^{n} there exists a point x ∈ S^{n} with g (x) = 1 g (- x). Broad searches found no completed Lean-4 Borsuk–Ulam theorem; Brouwer fixed-point results do not supply this source theorem as a checked declaration. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — simplicial map and simplicial approximation
A map of simplicial complexes is simplicial when it is linear on each simplex and sends vertices to vertices. A simplicial map g:K→L is a simplicial approximation to f when each f(star(v)) lies in star(g(v)).
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 map of simplicial complexes is simplicial when it is linear on each simplex and sends vertices to vertices. A simplicial map g:K→L is a simplicial approximation to f when each f(star(v)) lies in star(g(v)). Mathlib has abstract simplicial-complex/simplicial-set maps, but no checked Hatcher geometric simplicial-map plus star-based simplicial-approximation definition in one interface. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2C.1
If K is a finite simplicial complex and L is an arbitrary simplicial complex, then any map f {: } K {→ } L is homotopic to a map that is simplicial with respect to some iterated barycentric subdivision of K.
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 K is a finite simplicial complex and L is an arbitrary simplicial complex, then any map f {: } K {→ } L is homotopic to a map that is simplicial with respect to some iterated barycentric subdivision of K. No checked simplicial approximation theorem after iterated barycentric subdivision was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 2C.2
For vertices ν_{1}, …, ν_{n} of a simplicial complex X, the intersection s t ν_{1} ∩ … ∩ s t ν_{n} is empty unless ν_{1}, …, ν_{n} are the vertices of a simplex σ of X, in which case st ν_{1} ∩ … ∩ st ν_{n} = s 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 vertices ν_{1}, …, ν_{n} of a simplicial complex X, the intersection s t ν_{1} ∩ … ∩ s t ν_{n} is empty unless ν_{1}, …, ν_{n} are the vertices of a simplex σ of X, in which case st ν_{1} ∩ … ∩ st ν_{n} = s t σ. No checked star-intersection lemma in Hatcher’s simplicial-complex realization interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Lefschetz number
For f:X→X with finitely generated homology vanishing in high degrees, τ(f)=Σ_n(−1)^n tr(f_*:H_n(X)→H_n(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 f:X→X with finitely generated homology vanishing in high degrees, τ(f)=Σ_n(−1)^n tr(f_*:H_n(X)→H_n(X)). Trace and homology APIs exist separately, but no checked Lefschetz-number definition for topological self-maps/homology is packaged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2C.3
If X is a finite simplicial complex, or more generally a retract of a finite simplicial complex, and f: X {→ } X is a map with τ (f) ≠ 0, then f has a fixed 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: If X is a finite simplicial complex, or more generally a retract of a finite simplicial complex, and f: X {→ } X is a map with τ (f) ≠ 0, then f has a fixed point. No checked Lefschetz fixed-point theorem for finite simplicial complexes/retracts was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 2C.4
For the fixed-point-free 180° rotation f of the closed orientable genus-3 surface, the traces on H_0,H_1,H_2 are 1,2,1 respectively. Thus the alternating Lefschetz contributions are 1,−2,1 and τ(f)=0, as required by the Lefschetz theorem.
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 the fixed-point-free 180° rotation f of the closed orientable genus-3 surface, the traces on H_0,H_1,H_2 are 1,2,1 respectively. Thus the alternating Lefschetz contributions are 1,−2,1 and τ(f)=0, as required by the Lefschetz theorem. No checked genus-3 rotation homology-trace/Lefschetz computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 2C.5
Every CW complex X is homotopy equivalent to a simplicial complex, which can be chosen to be of the same dimension as X, finite if X is finite, and countable if X is countable.
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 CW complex X is homotopy equivalent to a simplicial complex, which can be chosen to be of the same dimension as X, finite if X is finite, and countable if X is countable. CW complexes and simplicial complexes are both present, and e3c7230fe78d7b056a415d9ecae6f77887046b32 triangulates surfaces, but no checked theorem turns every CW complex into a homotopy-equivalent simplicial complex with the same dimension and finiteness/countability refinements. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.