Chapter 4. Homotopy Theory
FC07 — Hatcher, Algebraic Topology.
This chapter contains 38 definitions, 26 theorems, 41 propositions, 13 lemmas, 18 corollaries, 37 examples, 11 constructions, 2 conventions and 2 other statements.
Of the 188 statements checked against Lean, 5 are formalized somewhere and 183 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 183 | 97% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 5 | 3% | Mathlib states and proves it. |
| checked in total | 188 |
- Canonical source block: FC07 Hatcher, Chapter 4,
FC07-C04-U001–FC07-C04-U188, exactly 188 unique 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=80cbd0498ab39e21d24d6730b3f932cec672a702(Apache-2.0, Lean 4.34.0-rc2), current/open work and indexed searches, Reservoir/package discovery, broad discoverable Lean repositories, and local mirrors. Noproject-existingC04 owner was found. - Every promoted Mathlib declaration/path was compiled through the project toolchain at the exact pin
P; every cited source path was also verified withgit cat-fileat the pinned git object. C04 therefore uses onlymathlibandunmatchedroutes: 5 pinned positive rows and 183 dated unmatched rows. - The exact pinned positives are U001 (homotopy groups as boundary-relative cube loops with concatenation group law), U055 (fiber bundles and local trivializations), U069 (complex unitary and quaternionic unitary/symplectic groups), U141 (oriented-graph diagrams of spaces and their amalgamation as a topological colimit), and U150 (pushout as the quotient of a disjoint sum with the final topology).
- U056 is deliberately not promoted:
IsFiberBundle.isCoveringMap/FiberBundle.isCoveringMapestablish only discrete-fiber bundle ⇒ covering map, while the source row states the two-way characterization. U083 is likewise not promoted: covering maps have a checked homotopy-lifting theorem, but no general topological Hurewicz-fibration predicate with HLP for every space was found. - U069 is routed through the actual star-unitary interface, not
Matrix.symplecticGroup.Matrix.unitaryGroupandmem_unitaryGroup_iff'own U(n), while genericunitaryspecializes to quaternionic matrices becauseQuaternioncarries the standard ring and star structures; this is the compact quaternionic unitary group convention denoted Sp(n) by Hatcher. The algebraic standard-alternating-formMatrix.symplecticGroupis a name-adjacent but different object and is not cited. - U141 is an equivalent categorical formalization of Hatcher’s quotient construction, not an abstract-name match:
Prefunctorrecords vertex objects and edge maps,Paths.liftfreely extends an oriented-graph diagram,ColimitTypeis the quotient of the sigma/coproduct of object elements by generated diagram-map identifications, and TopCat supplies the final topology. U147 remains unmatched because its second clause requires a homotopy-colimit/realization interface, which was not found. - U150 is literal at the underlying-set level:
Types.Pushout.Relidentifiesinl (f z)withinr (g z)andTypes.PushoutisQuotby that relation; the TopCat colimit construction supplies the quotient/final topology. - Model-category
Fibration/Cofibrationdeclarations are not credited for Hatcher’s topological HLP/HEP notions (U083, U148–U149). Likewise analytic/ring spectra, spectral sequences, Dold–Kan, and Eilenberg–Steenrod axioms are not algebraic-topological spectra, Dold–Thom, or Steenrod operations. - Current upstream was refreshed on 2026-09-07:
H=80cbd0498ab39e21d24d6730b3f932cec672a702is the newest Mathlib commit returned by the repository commit feed at audit time, and itslean-toolchainis Lean 4.34.0-rc2. Current code search still finds no Steenrod-operation implementation; “Steenrod” reaches onlyMathlib/AlgebraicTopology/EilenbergSteenrod.lean, while “Hurewicz” reaches the covering-space lifting API rather than the Hurewicz theorem. - Broad external Lean-4 discovery did not identify a complete owner for the missing Whitehead/Hurewicz/Blakers–Massey/Postnikov/K(G,n)/Brown-representability/stable-homotopy/Dold–Thom/Steenrod rows. Search results with theorem names in plans, future-work notes, other proof assistants, or semantically unrelated uses were not credited.
- The canonical catalogue has exactly one FC07 block after C04: Appendix
CA,FC07-CA-U001–FC07-CA-U032, 32 unique contiguous rows. No additional numbered Hatcher chapter is present in the catalogue. 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 — homotopy group πₙ
For n≥1, π_n(X,x_0) is the set of homotopy classes rel boundary of maps (In,∂In)→(X,x_0), with group operation by concatenation in one coordinate.
Formalized. Mathlib/Topology/Homotopy/HomotopyGroup.lean::HomotopyGroup, HomotopyGroup.Pi, HomotopyGroup.mul_spec, HomotopyGroup.group, HomotopyGroup.commGroup — HomotopyGroup is the quotient of generalized n-loops by boundary-relative homotopy; Pi n X x is the finite-cube specialization. mul_spec identifies multiplication with concatenation in a chosen coordinate, and the group/commutative-group instances give exactly the source group structure.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Construction — change of basepoint on higher homotopy groups
A path γ from x₀ to x₁ induces an isomorphism β_γ:π_n(X,x₁)→π_n(X,x₀), [f]↦[γf], with inverse β_{bar(γ)}.
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 path γ from x₀ to x₁ induces an isomorphism β_γ:π_n(X,x₁)→π_n(X,x₀), [f]↦[γf], with inverse β_{bar(γ)}. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — action of π₁ on πn
For loops γ at x₀, [γ]↦β_γ defines a homomorphism π₁(X,x₀)→Aut(π_n(X,x₀)), called the action of π₁ on π_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 loops γ at x₀, [γ]↦β_γ defines a homomorphism π₁(X,x₀)→Aut(π_n(X,x₀)), called the action of π₁ on π_n. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — n-simple, simple, and abelian spaces
A space is n-simple when the π₁-action on π_n is trivial, and simple when this holds for all n; Hatcher calls a space abelian when the π₁-action is trivial on all homotopy 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: A space is n-simple when the π₁-action on π_n is trivial, and simple when this holds for all n; Hatcher calls a space abelian when the π₁-action is trivial on all homotopy groups. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.1
A covering space projection p: (tilde(X), tilde(x){0}) (X, x{0}) induces isomorphisms p_{*}: π_{n} (tilde(X), tilde(x){0}) → π{n} (X, x_{0}) for all 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: A covering space projection p: (tilde(X), tilde(x){0}) (X, x{0}) induces isomorphisms p_{}: π_{n} (tilde(X), tilde(x){0}) → π*{n} (X, x_{0}) for all n ≥ 2. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.2
For a product Pi_{α} X_{α} of an arbitrary collection of path-connected spaces X_{α} there are isomorphisms { π_{n} (∏{α} X{α}) ≅ ∏{α} π{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: For a product Pi_{α} X_{α} of an arbitrary collection of path-connected spaces X_{α} there are isomorphisms { π_{n} (∏{α} X{α}) ≅ ∏{α} π{n} (X_{α}) } for all n. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — relative homotopy group
For x_0∈A⊂X, π_n(X,A,x_0) consists of homotopy classes of maps (In,∂In,J^{n−1})→(X,A,x_0), with J^{n−1} the union of all boundary faces except the distinguished one.
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 x_0∈A⊂X, π_n(X,A,x_0) consists of homotopy classes of maps (In,∂In,J^{n−1})→(X,A,x_0), with J^{n−1} the union of all boundary faces except the distinguished one. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — boundary map for relative homotopy
The relative homotopy boundary map ∂:π_n(X,A,x₀)→π_{n−1}(A,x₀) is induced by restricting a representative (Dn,S{n−1},s₀)→(X,A,x₀) to S^{n−1}; it is a homomorphism for 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: The relative homotopy boundary map ∂:π_n(X,A,x₀)→π_{n−1}(A,x₀) is induced by restricting a representative (Dn,S{n−1},s₀)→(X,A,x₀) to S^{n−1}; it is a homomorphism for n>1. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.3
For a based pair (X,A), the relative homotopy sequence …→π_n(A)→π_n(X)→π_n(X,A)→π_{n-1}(A)→… is exact.
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 based pair (X,A), the relative homotopy sequence …→π_n(A)→π_n(X)→π_n(X,A)→π_{n-1}(A)→… is exact. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.4
Let C X be the cone on a path-connected space X, the quotient space of X × I obtained by collapsing X × {0 } to a point. We can view X as the subspace X × {1 } ⊂ C X. Since C X is contractible, the long exact sequence of homotopy groups for the pair (C X, X) gives isomorphisms π_{n} (C X, X, x_{0}) ≅ π_{n - 1} (X, x_{0}) for all n ≥ 1. Taking n = 2, we can thus realize any group G, abelian or not, as a relative π_{2} by choosing X to have π_{1} (X) ≅ 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: Let C X be the cone on a path-connected space X, the quotient space of X × I obtained by collapsing X × {0 } to a point. We can view X as the subspace X × {1 } ⊂ C X. Since C X is contractible, the long exact sequence of homotopy groups for the pair (C X, X) gives isomorphisms π_{n} (C X, X, x_{0}) ≅ π_{n - 1} (X, x_{0}) for all n ≥ 1. Taking n = 2, we can thus realize any group G, abelian or not, as a relative π_{2} by choosing X to have π_{1} (X) ≅ G. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — change of basepoint for relative homotopy groups
A path γ in A from x₀ to x₁ induces an isomorphism β_γ:π_n(X,A,x₁)→π_n(X,A,x₀) by inserting a representative into a smaller cube and using γ along the distinguished face; it has the same basic properties as absolute change of basepoint.
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 path γ in A from x₀ to x₁ induces an isomorphism β_γ:π_n(X,A,x₁)→π_n(X,A,x₀) by inserting a representative into a smaller cube and using γ along the distinguished face; it has the same basic properties as absolute change of basepoint. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — n-connected space
A based space X is n-connected when π_i(X,x₀)=0 for all i≤n; 0-connected means path-connected and 1-connected means 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: A based space X is n-connected when π_i(X,x₀)=0 for all i≤n; 0-connected means path-connected and 1-connected means simply-connected. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — n-connected pair
A pair (X,A) is n-connected when the equivalent extension/nullhomotopy conditions of §4.1 hold through dimension n; equivalently, its relative homotopy groups vanish through that range with the stated π₀ condition.
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 pair (X,A) is n-connected when the equivalent extension/nullhomotopy conditions of §4.1 hold through dimension n; equivalently, its relative homotopy groups vanish through that range with the stated π₀ condition. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.5
If a map f: X {→ } Y between connected CW complexes induces isomorphisms f_{*}: π_{n} (X) → π_{n} (Y) for all n, then f is a homotopy equivalence. In case f is the inclusion of a subcomplex X ↪ Y, the conclusion is stronger: X is a deformation retract of Y.
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 map f: X {→ } Y between connected CW complexes induces isomorphisms f_{*}: π_{n} (X) → π_{n} (Y) for all n, then f is a homotopy equivalence. In case f is the inclusion of a subcomplex X ↪ Y, the conclusion is stronger: X is a deformation retract of Y. Pinned/current Mathlib has absolute HomotopyGroup, generalized loops, and ordinary homotopy machinery, but no checked change-of-basepoint/π₁-action/relative-homotopy/relative exact-sequence package owning the stated row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.6
Let (X, A) be a CW pair and let (Y, B) be any pair with B ≠ ∅. For each n such that X - A has cells of dimension n, assume that π_{n} (Y, B, y_{0}) = 0 for all y_{0} ∈ B. Then every map f: (X, A) → (Y, B) is homotopic rel A to a map X → 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: Let (X, A) be a CW pair and let (Y, B) be any pair with B ≠ ∅. For each n such that X - A has cells of dimension n, assume that π_{n} (Y, B, y_{0}) = 0 for all y_{0} ∈ B. Then every map f: (X, A) → (Y, B) is homotopic rel A to a map X → B. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.7
Given a CW pair (X, A) and a map f: A → Y with Y path-connected, then f can be extended to a map X → Y if π_{n - 1} (Y) = 0 for all n such that X - A has cells of dimension 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 a CW pair (X, A) and a map f: A → Y with Y path-connected, then f can be extended to a map X → Y if π_{n - 1} (Y) = 0 for all n such that X - A has cells of dimension n. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.8
Every map f: X {→ } Y of CW complexes is homotopic to a cellular map. If f is already cellular on a subcomplex A ⊂ X, the homotopy may be taken to be stationary on 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: Every map f: X {→ } Y of CW complexes is homotopic to a cellular map. If f is already cellular on a subcomplex A ⊂ X, the homotopy may be taken to be stationary on A. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.9
π_{n} (S^{k}) = 0 for n < 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: π_{n} (S^{k}) = 0 for n < k CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.10
Let f: I^{n} → Z be a map, where Z is obtained from a subspace W by attaching a cell e^{k}. Then there is a homotopy f_{t}: (I^{n}, f^{- 1} (e^{k})) {→ } (Z, e^{k}) rel f^{- 1} (W) from f = f_{0} to a map f_{1} for which there is a polyhedron K ⊂ I^{n} such that: (a) f_{1} (K) ⊂ e^{k} and f_{1} | K is P L with respect to some identification of e^{k} with ℝ^{k}. (b) K ⊃ f_{1}^{- 1} (U) for some nonempty open set U in e^{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: Let f: I^{n} → Z be a map, where Z is obtained from a subspace W by attaching a cell e^{k}. Then there is a homotopy f_{t}: (I^{n}, f^{- 1} (e^{k})) {→ } (Z, e^{k}) rel f^{- 1} (W) from f = f_{0} to a map f_{1} for which there is a polyhedron K ⊂ I^{n} such that: (a) f_{1} (K) ⊂ e^{k} and f_{1} | K is P L with respect to some identification of e^{k} with ℝ^{k}. (b) K ⊃ f_{1}^{- 1} (U) for some nonempty open set U in e^{k}. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.11
Cellular Approximation for Pairs. Every map f: (X, A) → (Y, B) of CW pairs can be deformed through maps (X, A) → (Y, B) to a cellular map. This follows from the theorem by first deforming the restriction f {: } A {→ } B to be cellular, then extending this to a homotopy of f on all of X, then deforming the resulting map to be cellular staying fixed on A. As a further refinement, the homotopy of f can be taken to be stationary on any subcomplex of X where f is already cellular.
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: Cellular Approximation for Pairs. Every map f: (X, A) → (Y, B) of CW pairs can be deformed through maps (X, A) → (Y, B) to a cellular map. This follows from the theorem by first deforming the restriction f {: } A {→ } B to be cellular, then extending this to a homotopy of f on all of X, then deforming the resulting map to be cellular staying fixed on A. As a further refinement, the homotopy of f can be taken to be stationary on any subcomplex of X where f is already cellular. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.12
A CW pair (X, A) is n connected if all the cells in X - A have dimension greater than n. In particular the pair (X, X^{n}) is n connected, hence the inclusion X^{n} ↪ X induces isomorphisms on π_{i} for i < n and a surjection on π_{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: A CW pair (X, A) is n connected if all the cells in X - A have dimension greater than n. In particular the pair (X, X^{n}) is n connected, hence the inclusion X^{n} ↪ X induces isomorphisms on π_{i} for i < n and a surjection on π_{n}. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — weak homotopy equivalence
A map f:X→Y is a weak homotopy equivalence if it induces isomorphisms on π_n for every n≥0 and every choice of basepoint.
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 f:X→Y is a weak homotopy equivalence if it induces isomorphisms on π_n for every n≥0 and every choice of basepoint. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — CW approximation
A CW approximation to X is a weak homotopy equivalence f:Z→X with Z a CW 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: A CW approximation to X is a weak homotopy equivalence f:Z→X with Z a CW complex. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.13
Every space X has a CW approximation f: Z {→ } X. If X is path-connected, Z can be chosen to have a single 0 cell, with all other cells attached by basepoint-preserving maps. Thus every connected CW complex is homotopy equivalent to a CW complex with these additional properties.
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 space X has a CW approximation f: Z {→ } X. If X is path-connected, Z can be chosen to have a single 0 cell, with all other cells attached by basepoint-preserving maps. Thus every connected CW complex is homotopy equivalent to a CW complex with these additional properties. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.14
One can also apply this technique to produce a CW approximation to a pair (X, X_{0}). First construct a CW approximation f_{0} {: } Z_{0} {→ } X_{0}, then starting with the composition Z_{0} → X_{0} ↪ X, attach cells to Z_{0} to create a weak homotopy equivalence f: Z → X extending f_{0}. By the five-lemma, the map f: (Z, Z_{0}) → (X, X_{0}) induces isomorphisms on relative as well as absolute homotopy 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: One can also apply this technique to produce a CW approximation to a pair (X, X_{0}). First construct a CW approximation f_{0} {: } Z_{0} {→ } X_{0}, then starting with the composition Z_{0} → X_{0} ↪ X, attach cells to Z_{0} to create a weak homotopy equivalence f: Z → X extending f_{0}. By the five-lemma, the map f: (Z, Z_{0}) → (X, X_{0}) induces isomorphisms on relative as well as absolute homotopy groups. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.15
If (X, A) is an n connected CW pair, then there exists a CW pair (Z, A) ≃ (X, A) rel A such that all cells of Z - A have dimension greater than 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, A) is an n connected CW pair, then there exists a CW pair (Z, A) ≃ (X, A) rel A such that all cells of Z - A have dimension greater than n. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.16
For every connected CW complex X and n≥1 there is a CW complex X_n containing X such that π_i(X_n)=0 for i>n and X→X_n induces isomorphisms on π_i for i≤n. Maps X_{n+1}→X_n extending X form a Postnikov tower.
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 connected CW complex X and n≥1 there is a CW complex X_n containing X such that π_i(X_n)=0 for i>n and X→X_n induces isomorphisms on π_i for i≤n. Maps X_{n+1}→X_n extending X form a Postnikov tower. CW, homotopy, and homology infrastructure exists, but no checked cellular-approximation, Whitehead, homotopy-excision/Blakers–Massey, CW-approximation, or corresponding weak-equivalence theorem realizes the complete row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — Postnikov tower
For connected CW X, one may form spaces X_n with π_i(X_n)≅π_i(X) for i≤n and π_i(X_n)=0 for i>n, together with maps X_{n+1}→X_n; this tower is the Postnikov tower.
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 connected CW X, one may form spaces X_n with π_i(X_n)≅π_i(X) for i≤n and π_i(X_n)=0 for i>n, together with maps X_{n+1}→X_n; this tower is the Postnikov tower. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.17
For every pair (X, A) with A a nonempty CW complex there exist n connected CW models f: (Z, A) → (X, A) for all n ≥ 0, and these models can be chosen to have the additional property that Z is obtained from A by attaching cells of dimension greater than 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 every pair (X, A) with A a nonempty CW complex there exist n connected CW models f: (Z, A) → (X, A) for all n ≥ 0, and these models can be chosen to have the additional property that Z is obtained from A by attaching cells of dimension greater than n. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.18
Given an n-connected CW model f:(Z,A)→(X,A), an n′-connected CW model f′:(Z′,A′)→(X′,A′), and g:(X,A)→(X′,A′), if n≥n′ there is h:Z→Z′ with h|_A=g|_A and gf≃f′h rel A; h is unique up to homotopy rel 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: Given an n-connected CW model f:(Z,A)→(X,A), an n′-connected CW model f′:(Z′,A′)→(X′,A′), and g:(X,A)→(X′,A′), if n≥n′ there is h:Z→Z′ with h|_A=g|_A and gf≃f′h rel A; h is unique up to homotopy rel A. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.19
An n connected CW model for (X, A) is unique up to homotopy equivalence rel 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: An n connected CW model for (X, A) is unique up to homotopy equivalence rel A. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.20
Whitehead Towers. If we take X to be an arbitrary CW complex with the subspace A a point, then the resulting tower of n-connected CW models amounts to a sequence of maps … → Z_{2} → Z_{1} → Z_{0} → X with Z_{n} n connected and the map Z_{n} → X inducing an isomorphism on all homotopy groups π_{i} with i > n. The space Z_{0} is path-connected and homotopy equivalent to the component of X containing A, so one may as well assume Z_{0} equals this component.
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: Whitehead Towers. If we take X to be an arbitrary CW complex with the subspace A a point, then the resulting tower of n-connected CW models amounts to a sequence of maps … → Z_{2} → Z_{1} → Z_{0} → X with Z_{n} n connected and the map Z_{n} → X inducing an isomorphism on all homotopy groups π_{i} with i > n. The space Z_{0} is path-connected and homotopy equivalent to the component of X containing A, so one may as well assume Z_{0} equals this component. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.21
A weak homotopy equivalence f: X {→ } Y induces isomorphisms f_{}: H_{n} (X; G) {→ } H_{n} (Y; G) and f^{}: H^{n} (Y; G) {→ } H^{n} (X; G) for all n and all coefficient groups 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: A weak homotopy equivalence f: X {→ } Y induces isomorphisms f_{}: H_{n} (X; G) {→ } H_{n} (Y; G) and f^{}: H^{n} (Y; G) {→ } H^{n} (X; G) for all n and all coefficient groups G. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.22
A weak homotopy equivalence f: Y → Z induces bijections [ X, Y ] [ X, Z ] and ⟨ X, Y ⟩ → ⟨ X, Z ⟩ for all CW complexes 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 weak homotopy equivalence f: Y → Z induces bijections [ X, Y ] [ X, Z ] and ⟨ X, Y ⟩ → ⟨ X, Z ⟩ for all CW complexes X. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.23
Let X be a CW complex decomposed as the union of subcomplexes A and B with nonempty connected intersection C = A ∩ B. If (A, C) is m connected and (B, C) is n connected, m, n ≥ 0, then the map π_{i} (A, C) → π_{i} (X, B) induced by inclusion is an isomorphism for i < m + n and a surjection for i = 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: Let X be a CW complex decomposed as the union of subcomplexes A and B with nonempty connected intersection C = A ∩ B. If (A, C) is m connected and (B, C) is n connected, m, n ≥ 0, then the map π_{i} (A, C) → π_{i} (X, B) induced by inclusion is an isomorphism for i < m + n and a surjection for i = m + n. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.24
The suspension map π_{i} (S^{n}) {→ } π_{i + 1} (S^{n + 1}) is an isomorphism for i < 2 n - 1 and a surjection for i = 2 n - 1. More generally this holds for the suspension π_{i} (X) → π_{i + 1} (S X) whenever X is an (n - 1) connected CW 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: The suspension map π_{i} (S^{n}) {→ } π_{i + 1} (S^{n + 1}) is an isomorphism for i < 2 n - 1 and a surjection for i = 2 n - 1. More generally this holds for the suspension π_{i} (X) → π_{i + 1} (S X) whenever X is an (n - 1) connected CW complex. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.25
π_{n} (S^{n}) ≅ ℤ, generated by the identity map, for all n ≥ 1. In particular, the degree map π_{n} (S^{n}) → ℤ is an isomorphism.
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: π_{n} (S^{n}) ≅ ℤ, generated by the identity map, for all n ≥ 1. In particular, the degree map π_{n} (S^{n}) → ℤ is an isomorphism. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.26
The calculation of π_{n} (S^{n}) can be extended to show that π_{n} (backslash_{α} S_{α}^{n}) for n ≥ 2 is free abelian with basis the homotopy classes of the inclusions S_{α}^{n} ↪ ∨{α} S{α}^{n} Suppose first that there are only finitely many summands S_{α}^{n}. Hence from the long exact sequence of homotopy groups for this pair we see that the inclusion { ∨{α} S{α}^{n} ↪ Pi_{α} S_{α}^{n} } induces an isomorphism on π_{n} if 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: The calculation of π_{n} (S^{n}) can be extended to show that π_{n} (backslash_{α} S_{α}^{n}) for n ≥ 2 is free abelian with basis the homotopy classes of the inclusions S_{α}^{n} ↪ ∨{α} S{α}^{n} Suppose first that there are only finitely many summands S_{α}^{n}. Hence from the long exact sequence of homotopy groups for this pair we see that the inclusion { ∨{α} S{α}^{n} ↪ Pi_{α} S_{α}^{n} } induces an isomorphism on π_{n} if n ≥ 2. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.27
Let us show that π_{n} (S^{1} ∨ S^{n}) for n ≥ 2 is free abelian on a countably infinite number of generators. Writing a generator of π_{1} (S^{1} ∨ S^{n}) as t, the group ring ℤ [ π_{1} (S^{1} ∨ S^{n}) ] becomes ℤ [ t, t^{- 1} ], the Laurent polynomials in t and t^{- 1} with ℤ coefficients, and we have π_{n} (S^{1} ∨ S^{n}) ≅ ℤ [ t, t^{- 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: Let us show that π_{n} (S^{1} ∨ S^{n}) for n ≥ 2 is free abelian on a countably infinite number of generators. Writing a generator of π_{1} (S^{1} ∨ S^{n}) as t, the group ring ℤ [ π_{1} (S^{1} ∨ S^{n}) ] becomes ℤ [ t, t^{- 1} ], the Laurent polynomials in t and t^{- 1} with ℤ coefficients, and we have π_{n} (S^{1} ∨ S^{n}) ≅ ℤ [ t, t^{- 1} ]. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.28
If a CW pair (X, A) is r connected and A is s connected, with r, s ≥ 0, then the map π_{i} (X, A) {→ } π_{i} (X / A) induced by the quotient map X {→ } X / A is an isomorphism for i ≤ r + s and a surjection for i = r + s + 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 a CW pair (X, A) is r connected and A is s connected, with r, s ≥ 0, then the map π_{i} (X, A) {→ } π_{i} (X / A) induced by the quotient map X {→ } X / A is an isomorphism for i ≤ r + s and a surjection for i = r + s + 1. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.29
Suppose X is obtained from a wedge of spheres ∨{α} S{α}^{n} by attaching cells e_{β}^{n + 1} via basepoint-preserving maps φ_{β}: S^{n} → ∨{α} S{α}^{n}, with n ≥ 2. Any subgroup can be realized in this way, by choosing maps φ_{β} to represent a set of generators for the subgroup, so it follows that every abelian group can be realized as π_{n} (X) for such a space X = (∨{α} S{α}^{n}) ⋃{β} e{β}^{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: Suppose X is obtained from a wedge of spheres ∨{α} S{α}^{n} by attaching cells e_{β}^{n + 1} via basepoint-preserving maps φ_{β}: S^{n} → ∨{α} S{α}^{n}, with n ≥ 2. Any subgroup can be realized in this way, by choosing maps φ_{β} to represent a set of generators for the subgroup, so it follows that every abelian group can be realized as π_{n} (X) for such a space X = (∨{α} S{α}^{n}) ⋃{β} e{β}^{n + 1}. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Eilenberg–Mac Lane space K(G,n)
A K(G,n) is a path-connected space with π_n≅G and all other homotopy groups trivial; for n≥2, G must be abelian.
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,n) is a path-connected space with π_n≅G and all other homotopy groups trivial; for n≥2, G must be abelian. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.30
The homotopy type of a CW complex K (G, n) is uniquely determined by G and 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 homotopy type of a CW complex K (G, n) is uniquely determined by G and n. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.31
Let X be a CW complex of the form (∨{α} S{α}^{n}) ∪{β} e{β}^{n + 1} for some n ≥ 1. Then for every homomorphism psi: π_{n} (X) → π_{n} (Y) with Y path-connected there exists a map f: X {→ } Y with f_{*} = psi.
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 CW complex of the form (∨{α} S{α}^{n}) ∪{β} e{β}^{n + 1} for some n ≥ 1. Then for every homomorphism psi: π_{n} (X) → π_{n} (Y) with Y path-connected there exists a map f: X {→ } Y with f_{*} = psi. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.32
If a space X is (n - 1) connected, n ≥ 2, then H̃{i} (X) = 0 for i < n and π{n} (X) ≅ H_{n} (X). If a pair (X, A) is (n - 1) connected, n ≥ 2, with A simply-connected and nonempty, then H_{i} (X, A) = 0 for i < n and π_{n} (X, A) ≅ H_{n} (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: If a space X is (n - 1) connected, n ≥ 2, then H̃{i} (X) = 0 for i < n and π{n} (X) ≅ H_{n} (X). If a pair (X, A) is (n - 1) connected, n ≥ 2, with A simply-connected and nonempty, then H_{i} (X, A) = 0 for i < n and π_{n} (X, A) ≅ H_{n} (X, A). No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.33
A map f: X {→ } Y between simply-connected CW complexes is a homotopy equivalence if f_{*}: H_{n} (X) → H_{n} (Y) is an isomorphism for each 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: A map f: X {→ } Y between simply-connected CW complexes is a homotopy equivalence if f_{*}: H_{n} (X) → H_{n} (Y) is an isomorphism for each n. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.34
For n>1 the homotopy type of a CW Moore space M(G,n) is uniquely determined by G and n. Given the standard M(G,n) and any other CW M(G,n), one constructs a map inducing an isomorphism on π_n and then on H_n; the homology-isomorphism criterion for simply-connected CW complexes makes it a homotopy equivalence.
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 n>1 the homotopy type of a CW Moore space M(G,n) is uniquely determined by G and n. Given the standard M(G,n) and any other CW M(G,n), one constructs a map inducing an isomorphism on π_n and then on H_n; the homology-isomorphism criterion for simply-connected CW complexes makes it a homotopy equivalence. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.35
We construct a space X = (S^{1} ∨ S^{n}) ∪ e^{n + 1}, for arbitrary n > 1, such that the inclusion S^{1} ↪ X induces an isomorphism on all homology groups and on π_{i} for i < n, but not on π_{n}. By looking in the universal cover we see that π_{n} (X) ≅ ℤ [ t, t^{- 1} ] / (2 t - 1), where (2 t - 1) denotes the ideal in ℤ [ t, t^{- 1} ] generated by 2 t - 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: We construct a space X = (S^{1} ∨ S^{n}) ∪ e^{n + 1}, for arbitrary n > 1, such that the inclusion S^{1} ↪ X induces an isomorphism on all homology groups and on π_{i} for i < n, but not on π_{n}. By looking in the universal cover we see that π_{n} (X) ≅ ℤ [ t, t^{- 1} ] / (2 t - 1), where (2 t - 1) denotes the ideal in ℤ [ t, t^{- 1} ] generated by 2 t - 1. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.36
The Hurewicz map h: π_{n} (X, A, x_{0}) {→ } H_{n} (X, A) is a homomorphism, assuming n > 1 so that π_{n} (X, A, x_{0}) is a 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: The Hurewicz map h: π_{n} (X, A, x_{0}) {→ } H_{n} (X, A) is a homomorphism, assuming n > 1 so that π_{n} (X, A, x_{0}) is a group. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.37
If (X, A) is an (n - 1) connected pair of path-connected spaces with n ≥ 2 and A ≠ ∅, then h^{′}: π_{n}^{′} (X, A, x_{0}) {→ } H_{n} (X, A) is an isomorphism and H_{i} (X, A) = 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: If (X, A) is an (n - 1) connected pair of path-connected spaces with n ≥ 2 and A ≠ ∅, then h^{′}: π_{n}^{′} (X, A, x_{0}) {→ } H_{n} (X, A) is an isomorphism and H_{i} (X, A) = 0 for i < n. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.38
If X is a connected CW complex to which cells e_{α}^{n} are attached for a fixed n ≥ 2, forming a CW complex W = X ⋃{α} e{α}^{n}, then π_{n} (W, X) is a free π_{1} (X) module with basis the homotopy classes of the characteristic maps Φ_{α} of the cells e_{α}^{n}, provided that the map π_{1} (X) {→ } π_{1} (W) induced by inclusion is an isomorphism. In particular, this is always the case if n ≥ 3. In the general n = 2 case, π_{2} (W, X) is generated by the classes of the characteristic maps of the cells e_{α}^{2} together with their images under the action of π_{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: If X is a connected CW complex to which cells e_{α}^{n} are attached for a fixed n ≥ 2, forming a CW complex W = X ⋃{α} e{α}^{n}, then π_{n} (W, X) is a free π_{1} (X) module with basis the homotopy classes of the characteristic maps Φ_{α} of the cells e_{α}^{n}, provided that the map π_{1} (X) {→ } π_{1} (W) induced by inclusion is an isomorphism. In particular, this is always the case if n ≥ 3. In the general n = 2 case, π_{2} (W, X) is generated by the classes of the characteristic maps of the cells e_{α}^{2} together with their images under the action of π_{1} (X). No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.39
For any (X, A, x_{0}), the formula a + b - a = (∂ a) b holds for all a, b ∈ π_{2} (X, A, x_{0}), where ∂: π_{2} (X, A, x_{0}) → π_{1} (A, x_{0}) is the usual boundary map and (∂ a) b denotes the action of ∂ a on ^ b. Hence π_{2}^{′} (X, A, x_{0}) is abelian.
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 any (X, A, x_{0}), the formula a + b - a = (∂ a) b holds for all a, b ∈ π_{2} (X, A, x_{0}), where ∂: π_{2} (X, A, x_{0}) → π_{1} (A, x_{0}) is the usual boundary map and (∂ a) b denotes the action of ∂ a on ^ b. Hence π_{2}^{′} (X, A, x_{0}) is abelian. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.40
Let X be a connected CW complex with H_{1} (X) = 0. Then there is a simply-connected CW complex X^{+} and a map X → X^{+} inducing isomorphisms on all homology 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: Let X be a connected CW complex with H_{1} (X) = 0. Then there is a simply-connected CW complex X^{+} and a map X → X^{+} inducing isomorphisms on all homology groups. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.41
If p:E→B has the homotopy lifting property with respect to every disk, F=p^{-1}(b_0), and x_0∈F, then p_*:π_n(E,F,x_0)→π_n(B,b_0) is an isomorphism for n≥1. If B is path-connected this identifies the relative homotopy sequence with the long exact fiber sequence …→π_n(F)→π_n(E)→π_n(B)→π_{n-1}(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: If p:E→B has the homotopy lifting property with respect to every disk, F=p^{-1}(b_0), and x_0∈F, then p_*:π_n(E,F,x_0)→π_n(B,b_0) is an isomorphism for n≥1. If B is path-connected this identifies the relative homotopy sequence with the long exact fiber sequence …→π_n(F)→π_n(E)→π_n(B)→π_{n-1}(F)→…. No checked Postnikov-tower, Eilenberg–Mac Lane-space, Hurewicz theorem, or the stated homotopy-group calculation was found; singular homology and absolute homotopy groups remain unbridged. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fiber bundle
A fiber bundle structure p:E→B with fiber F is locally trivial: each b∈B has a neighborhood U and a homeomorphism h:p^{-1}(U)→U×F commuting with projection; h is a local trivialization, B the base, E the total space, and p^{-1}(b) a fiber.
Formalized. Mathlib/Topology/FiberBundle/Basic.lean::FiberBundle, Bundle.Trivialization, FiberBundle.trivializationAt, FiberBundle.mem_baseSet_trivializationAt, Bundle.Trivialization.proj_toFun — FiberBundle F E supplies a local trivialization at every base point; trivializationAt and mem_baseSet_trivializationAt give the neighborhood containing that point, while Bundle.Trivialization is the local homeomorphism to base × fiber and proj_toFun is the commuting-with-projection law. This is Hatcher’s fiber/base/total-space local-product definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 4.42
A fiber bundle with fiber a discrete space is a covering space. Conversely, a covering space whose fibers all have the same cardinality, for example a covering space over a connected base space, is a fiber bundle with discrete fiber.
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 fiber bundle with fiber a discrete space is a covering space. Conversely, a covering space whose fibers all have the same cardinality, for example a covering space over a connected base space, is a fiber bundle with discrete fiber. IsFiberBundle.isCoveringMap and FiberBundle.isCoveringMap prove the discrete-fiber-bundle ⇒ covering direction, but no checked converse supplies Hatcher’s “exactly covering spaces” equivalence. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.43
One of the simplest nontrivial fiber bundles is the Möbius band, which is a bundle over S^{1} with fiber an interval. Specifically, take E to be the quotient of I × [ - 1, 1 ] under the identifications (0, ν) ∼ (1, - ν), with p: E {→ } S^{1} induced by the projection I × [ - 1, 1 ] → I, so the fiber is [−1, 1]. Glueing two copies of E together by the identity map between their boundary circles produces a Klein bottle, a bundle over S^{1} with fiber S^{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: One of the simplest nontrivial fiber bundles is the Möbius band, which is a bundle over S^{1} with fiber an interval. Specifically, take E to be the quotient of I × [ - 1, 1 ] under the identifications (0, ν) ∼ (1, - ν), with p: E {→ } S^{1} induced by the projection I × [ - 1, 1 ] → I, so the fiber is [−1, 1]. Glueing two copies of E together by the identity map between their boundary circles produces a Klein bottle, a bundle over S^{1} with fiber S^{1}. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.44
For the Hopf bundle S1→S{2n+1}→ℂP^n, the fiber-sequence calculation gives π_i(ℂPn)≅π_i(S{2n+1}) for i>2 and π_2(ℂP^n)≅ℤ; in particular ℂP^∞ is a 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: For the Hopf bundle S1→S{2n+1}→ℂP^n, the fiber-sequence calculation gives π_i(ℂPn)≅π_i(S{2n+1}) for i>2 and π_2(ℂP^n)≅ℤ; in particular ℂP^∞ is a K(ℤ,2). FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.45
The n=1 complex projective bundle is the Hopf bundle S1→S3→S2=ℂP1, with projection p(z₀,z₁)=z₀/z₁∈ℂ∪{∞}. Its fibers are slope-one circles on the nested tori in S^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: The n=1 complex projective bundle is the Hopf bundle S1→S3→S2=ℂP1, with projection p(z₀,z₁)=z₀/z₁∈ℂ∪{∞}. Its fibers are slope-one circles on the nested tori in S^3. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.46
Replacing the field ℂ by the quaternions {H }, the same constructions yield fiber bundles S^{3} → S^{4 n + 3} → ℍP^{n} over quaternionic projective spaces ℍP^{n}. Here the fiber S^{3} is the unit quaternions, and S^{4 n + 3} is the unit sphere in {H }^{n + 1}. Taking n = 1 gives a second Hopf bundle S^{3} → S^{7} → S^{4} = ℍP^{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: Replacing the field ℂ by the quaternions {H }, the same constructions yield fiber bundles S^{3} → S^{4 n + 3} → ℍP^{n} over quaternionic projective spaces ℍP^{n}. Here the fiber S^{3} is the unit quaternions, and S^{4 n + 3} is the unit sphere in {H }^{n + 1}. Taking n = 1 gives a second Hopf bundle S^{3} → S^{7} → S^{4} = ℍP^{1}. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.47
Using the octonions, the map p:S15→S8=𝕆∪{∞}, p(z_0,z_1)=z_0z_1^{-1}, is locally trivial over the complements of ∞ and 0 via the displayed octonionic charts, giving the Hopf bundle S7→S15→S^8.
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: Using the octonions, the map p:S15→S8=𝕆∪{∞}, p(z_0,z_1)=z_0z_1^{-1}, is locally trivial over the complements of ∞ and 0 via the displayed octonionic charts, giving the Hopf bundle S7→S15→S^8. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.48
A fiber bundle p: E → B has the homotopy lifting property with respect to all CW 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: A fiber bundle p: E → B has the homotopy lifting property with respect to all CW pairs (X, A). FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.49
Applying this theorem to a covering space p: E → B with E and B path-connected, and discrete fiber F, the resulting long exact sequence of homotopy groups yields Proposition 4.1 that p_{}: π_{n} (E) → π_{n} (B) is an isomorphism for n ≥ 2. We also obtain a short exact sequence 0 {→ } π_{1} (E) {→ } π_{1} (B) {→ } π_{0} (F) {→ } 0, consistent with the covering space theory facts that p_{}: π_{1} (E) → π_{1} (B) is injective and that the fiber F can be identified, via path-lifting, with the set of cosets of p_{*} π_{1} (E) in π_{1} (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: Applying this theorem to a covering space p: E → B with E and B path-connected, and discrete fiber F, the resulting long exact sequence of homotopy groups yields Proposition 4.1 that p_{}: π_{n} (E) → π_{n} (B) is an isomorphism for n ≥ 2. We also obtain a short exact sequence 0 {→ } π_{1} (E) {→ } π_{1} (B) {→ } π_{0} (F) {→ } 0, consistent with the covering space theory facts that p_{}: π_{1} (E) → π_{1} (B) is injective and that the fiber F can be identified, via path-lifting, with the set of cosets of p_{*} π_{1} (E) in π_{1} (B). FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.50
From the bundle S^{1} {→ } S^{∞} {→ } ℂP^{∞} we obtain π_{i} (ℂP^{∞}) ≅ π_{i - 1} (S^{1}) for all i since S^{∞} is contractible. Thus { (P^{∞} } is a K (ℤ, 2). In similar fashion the bundle S^{3} → S^{∞} → { H P^{∞} } gives π_{i} (ℍP^{∞}) ≅ π_{i - 1} (S^{3}) for all i, but these homotopy groups are far more complicated than for ℂP^{∞} and S^{1}. In particular, { {H } } {P }^{∞} is not a K (ℤ, 4).
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 the bundle S^{1} {→ } S^{∞} {→ } ℂP^{∞} we obtain π_{i} (ℂP^{∞}) ≅ π_{i - 1} (S^{1}) for all i since S^{∞} is contractible. Thus { (P^{∞} } is a K (ℤ, 2). In similar fashion the bundle S^{3} → S^{∞} → { H P^{∞} } gives π_{i} (ℍP^{∞}) ≅ π_{i - 1} (S^{3}) for all i, but these homotopy groups are far more complicated than for ℂP^{∞} and S^{1}. In particular, { {H } } {P }^{∞} is not a K (ℤ, 4). FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.51
The long exact sequence for the Hopf bundle S^{1} → S^{3} → S^{2} gives isomorphisms π_{2} (S^{2}) ≅ π_{1} (S^{1}) and π_{n} (S^{3}) ≅ π_{n} (S^{2}) for all n ≥ 3. Taking n = 3, we see that π_{3} (S^{2}) is infinite cyclic, generated by the Hopf map S^{3} → S^{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 long exact sequence for the Hopf bundle S^{1} → S^{3} → S^{2} gives isomorphisms π_{2} (S^{2}) ≅ π_{1} (S^{1}) and π_{n} (S^{3}) ≅ π_{n} (S^{2}) for all n ≥ 3. Taking n = 3, we see that π_{3} (S^{2}) is infinite cyclic, generated by the Hopf map S^{3} → S^{2}. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.52
For a wedge ∨_α S^2_α, π₃(∨_α S^2_α) is free abelian with basis consisting of the Hopf maps S3→S2_α and, for each unordered pair α≠β, the Whitehead-product attaching maps S3→S2_α∨S^2_β arising from the 4-cells of S2_α×S2_β.
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 ∨_α S^2_α, π₃(∨_α S^2_α) is free abelian with basis consisting of the Hopf maps S3→S2_α and, for each unordered pair α≠β, the Whitehead-product attaching maps S3→S2_α∨S^2_β arising from the 4-cells of S2_α×S2_β. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.53
The Stiefel-to-Grassmann projections are fiber bundles O(n)→V_n(ℝk)→G_n(ℝk), U(n)→V_n(ℂk)→G_n(ℂk), and Sp(n)→V_n(ℍk)→G_n(ℍk), also for k=∞. The infinite Stiefel manifolds are contractible; the finite real, complex, and quaternionic Stiefel manifolds have connectivities k−n−1, 2k−2n, and 4k−4n+2 respectively.
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 Stiefel-to-Grassmann projections are fiber bundles O(n)→V_n(ℝk)→G_n(ℝk), U(n)→V_n(ℂk)→G_n(ℂk), and Sp(n)→V_n(ℍk)→G_n(ℍk), also for k=∞. The infinite Stiefel manifolds are contractible; the finite real, complex, and quaternionic Stiefel manifolds have connectivities k−n−1, 2k−2n, and 4k−4n+2 respectively. FiberBundle supplies generic local triviality, but no checked declaration owns the specific Hopf/Stiefel/bundle construction or homotopy-group computation in this row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — real Grassmann manifold
The Grassmann manifold G_n(ℝ^k) is the space of n-dimensional vector subspaces of ℝ^k, topologized as the quotient of the Stiefel manifold V_n(ℝ^k) by the projection sending a frame to its span.
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 Grassmann manifold G_n(ℝ^k) is the space of n-dimensional vector subspaces of ℝ^k, topologized as the quotient of the Stiefel manifold V_n(ℝ^k) by the projection sending a frame to its span. Module.Grassmannian is an algebraic module/scheme-oriented Grassmannian; no checked real topological Grassmann manifold as the Stiefel quotient with the stated topology was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — unitary and symplectic groups
U(n) consists of n×n complex matrices whose columns are orthonormal for the Hermitian inner product; Sp(n) is the quaternionic analog.
Formalized. Mathlib/LinearAlgebra/UnitaryGroup.lean::Matrix.unitaryGroup, Matrix.mem_unitaryGroup_iff, Matrix.mem_unitaryGroup_iff'; Mathlib/Algebra/Star/Unitary.lean::unitary, Unitary.mem_iff; Mathlib/Algebra/Quaternion.lean::Quaternion.instRing, Quaternion.instStarRing — Matrix.unitaryGroup over ℂ is the square-matrix unitary group, and mem_unitaryGroup_iff' gives the conjugate-transpose-times-matrix identity expressing orthonormal columns. The generic unitary construction applies unchanged to quaternionic matrices because Quaternion is a ring with the standard involutive star; Unitary.mem_iff gives the same star-unitary equations. These are exactly U(n) and its quaternionic analogue Sp(n).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Example 4.54
For m<n≤k there is a fiber bundle V_{n-m}(ℝ{k-m})→V_n(ℝk)→V_m(ℝ^k) sending an n-frame to its first m vectors, with analogous complex and quaternionic bundles. For m=1 the resulting fiber sequences prove the Stiefel connectivity statements; for k=n they identify Stiefel and Grassmann manifolds as the corresponding homogeneous 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: For m<n≤k there is a fiber bundle V_{n-m}(ℝ{k-m})→V_n(ℝk)→V_m(ℝ^k) sending an n-frame to its first m vectors, with analogous complex and quaternionic bundles. For m=1 the resulting fiber sequences prove the Stiefel connectivity statements; for k=n they identify Stiefel and Grassmann manifolds as the corresponding homogeneous spaces. Suspension and homotopy groups exist, but no checked Freudenthal stabilization theorem or stable-homotopy-group interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4.55
The bundles O(n−1)→O(n)→S^{n−1}, U(n−1)→U(n)→S^{2n−1}, and Sp(n−1)→Sp(n)→S^{4n−1} imply stabilization of π_i for n≫i. Bott periodicity says the stable homotopy groups repeat with period 8 for O and Sp and period 2 for U.
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 bundles O(n−1)→O(n)→S^{n−1}, U(n−1)→U(n)→S^{2n−1}, and Sp(n−1)→Sp(n)→S^{4n−1} imply stabilization of π_i for n≫i. Bott periodicity says the stable homotopy groups repeat with period 8 for O and Sp and period 2 for U. Suspension and homotopy groups exist, but no checked Freudenthal stabilization theorem or stable-homotopy-group interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — stable homotopy groups of spheres
For fixed k, the suspension maps π_{n+k}(Sn)→π_{n+k+1}(S{n+1}) eventually become isomorphisms; the eventual group is the k-th stable homotopy group of spheres π_k^s.
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 fixed k, the suspension maps π_{n+k}(Sn)→π_{n+k+1}(S{n+1}) eventually become isomorphisms; the eventual group is the k-th stable homotopy group of spheres π_k^s. Suspension and homotopy groups exist, but no checked Freudenthal stabilization theorem or stable-homotopy-group interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.56
The composition products π_{i}^{s} × π_{j}^{s} → π_{i + j}^{s} induce a graded ring structure on π_{*}^{s} = ⊕{i} π{i}^{s} satisfying the commutativity relation α β = (- 1)^{i j} β α for α ∈ π_{i}^{s} and β ∈ π_{j}^{s}.
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 composition products π_{i}^{s} × π_{j}^{s} → π_{i + j}^{s} induce a graded ring structure on π_{}^{s} = ⊕{i} π*{i}^{s} satisfying the commutativity relation α β = (- 1)^{i j} β α for α ∈ π_{i}^{s} and β ∈ π_{j}^{s}. Suspension and homotopy groups exist, but no checked Freudenthal stabilization theorem or stable-homotopy-group interface realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.57
There are natural bijections T: ⟨ X, K (G, n) ⟩ → H^{n} (X; G) for all CW complexes X and all n > 0, with G any abelian group. Such a T has the form T ([ f ]) = f^{*} (α) for a certain distinguished class α ∈ H^{n} (K (G, n); 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: There are natural bijections T: ⟨ X, K (G, n) ⟩ → H^{n} (X; G) for all CW complexes X and all n > 0, with G any abelian group. Such a T has the form T ([ f ]) = f^{*} (α) for a certain distinguished class α ∈ H^{n} (K (G, n); G). No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fundamental class of K(G,n)
A class α∈H^n(K(G,n);G) corresponding under the universal-coefficient/Hurewicz identification to the inverse Hurewicz isomorphism is called a fundamental class of K(G,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: A class α∈H^n(K(G,n);G) corresponding under the universal-coefficient/Hurewicz identification to the inverse Hurewicz isomorphism is called a fundamental class of K(G,n). No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — sum of maps from a suspension
For based maps f,g:ΣX→K, their sum is the composite ΣX→ΣX∨ΣX→K, where the first map collapses an equatorial X and the second restricts to f and g on the two wedge summands.
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 based maps f,g:ΣX→K, their sum is the composite ΣX→ΣX∨ΣX→K, where the first map collapses an equatorial X and the second restricts to f and g on the two wedge summands. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Ω-spectrum
An Ω-spectrum is a sequence of CW complexes K_n with weak homotopy equivalences K_n→ΩK_{n+1} 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: An Ω-spectrum is a sequence of CW complexes K_n with weak homotopy equivalences K_n→ΩK_{n+1} for all n. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.58
If { K_{n} } is an Ω · spectrum, then the functors X ↦ h^{n} (X) = ⟨ X, K_{n} ⟩, n ∈ ℤ, define a reduced cohomology theory on the category of basepointed CW complexes and basepoint-preserving 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: If { K_{n} } is an Ω · spectrum, then the functors X ↦ h^{n} (X) = ⟨ X, K_{n} ⟩, n ∈ ℤ, define a reduced cohomology theory on the category of basepointed CW complexes and basepoint-preserving maps. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — infinite loopspace
A space K_n in an Ω-spectrum is called an infinite loopspace since K_n is weakly homotopy equivalent to Ω^kK_{n+k} for every 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: A space K_n in an Ω-spectrum is called an infinite loopspace since K_n is weakly homotopy equivalent to Ω^kK_{n+k} for every k. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — cofibration/Puppe sequence of a CW pair
A CW pair (X,A) gives the cofibration sequence A→X→X/A→ΣA→ΣX→…, natural in maps of pairs.
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 CW pair (X,A) gives the cofibration sequence A→X→X/A→ΣA→ΣX→…, natural in maps of pairs. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.59
If h^{*} is an unreduced cohomology theory on the category of CW pairs and h^{n} (p o i n t) = 0 for n ≠ 0, then there are natural isomorphisms h^{n} (X, A) ≅ H^{n} {(} X, A; h^{0} (p o i n t) {) } for all CW pairs (X, A) and all n. The corresponding statement for homology theories is also true.
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 h^{*} is an unreduced cohomology theory on the category of CW pairs and h^{n} (p o i n t) = 0 for n ≠ 0, then there are natural isomorphisms h^{n} (X, A) ≅ H^{n} {(} X, A; h^{0} (p o i n t) {) } for all CW pairs (X, A) and all n. The corresponding statement for homology theories is also true. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.60
If a functor h from basepointed CW complexes to abelian groups satisfies the homotopy and wedge axioms, then for any two basepoint-preserving maps f, g: Σ X {→ } K, we have (f + g){} = f_{} + g{} if h is covariant and (f + g)^{} = f^{} + g^{} if h is contravariant.
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 functor h from basepointed CW complexes to abelian groups satisfies the homotopy and wedge axioms, then for any two basepoint-preserving maps f, g: Σ X {→ } K, we have (f + g){} = f{} + g_{} if h is covariant and (f + g)^{} = f^{} + g^{} if h is contravariant. No checked K(G,n)-representability, Ω-spectrum, infinite-loopspace, or topological Puppe/cofibration-sequence interface was found; ordinary homotopy/cohomological algebra is only adjacent. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fibration
A fibration is a map p:E→B with the homotopy lifting property for every space 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 fibration is a map p:E→B with the homotopy lifting property for every space X. IsCoveringMap.liftHomotopy formalizes homotopy lifting for covering maps, but Mathlib has no general topological Hurewicz-fibration predicate satisfying HLP for every space. Model-category Fibration is a different interface. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.61
For a fibration p: E → B, the fibers F_{b} = p^{- 1} (b) over each path component of B are all homotopy equivalent.
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 fibration p: E → B, the fibers F_{b} = p^{- 1} (b) over each path component of B are all homotopy equivalent. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fiber-preserving map and fiber homotopy equivalence
For fibrations p_i:E_i→B, f:E₁→E₂ is fiber-preserving if p₁=p₂f. It is a fiber homotopy equivalence if it has a fiber-preserving inverse up to homotopies through fiber-preserving 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: For fibrations p_i:E_i→B, f:E₁→E₂ is fiber-preserving if p₁=p₂f. It is a fiber homotopy equivalence if it has a fiber-preserving inverse up to homotopies through fiber-preserving maps. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.62
Given a fibration p: E → B and a homotopy f_{t} {: } A {→ } B, the pullback fibrations f_{0}^{} (E) A and f_{1}^{} (E) → A are fiber homotopy equivalent.
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 a fibration p: E → B and a homotopy f_{t} {: } A {→ } B, the pullback fibrations f_{0}^{} (E) A and f_{1}^{} (E) → A are fiber homotopy equivalent. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.63
A fibration E → B over a contractible base B is fiber homotopy equivalent to a product fibration B {× } F → 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: A fibration E → B over a contractible base B is fiber homotopy equivalent to a product fibration B {× } F → B. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — pathspace and path fibration
For based X, the pathspace PX consists of paths beginning at the basepoint; endpoint evaluation PX→X has fiber ΩX and is the basic pathspace fibration.
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 based X, the pathspace PX consists of paths beginning at the basepoint; endpoint evaluation PX→X has fiber ΩX and is the basic pathspace fibration. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.64
The map p: E_{f} → B, p (a, γ) = γ (1), is a fibration.
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 map p: E_{f} → B, p (a, γ) = γ (1), is a fibration. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — homotopy fiber
For f:A→B, the pathspace replacement E_f→B has fiber F_f consisting of pairs (a,γ) with γ a path from f(a) to the chosen basepoint; F_f is the homotopy fiber of 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:A→B, the pathspace replacement E_f→B has fiber F_f consisting of pairs (a,γ) with γ a path from f(a) to the chosen basepoint; F_f is the homotopy fiber of f. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.65
If p: E → B is a fibration, then the inclusion E ↪ E_{p} is a fiber homotopy equivalence. In particular, the homotopy fibers of p are homotopy equivalent to the actual fibers.
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 p: E → B is a fibration, then the inclusion E ↪ E_{p} is a fiber homotopy equivalence. In particular, the homotopy fibers of p are homotopy equivalent to the actual fibers. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.66
If F {→ } E {→ } B is a fibration or fiber bundle with E contractible, then there is a weak homotopy equivalence F → Ω 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 F {→ } E {→ } B is a fibration or fiber bundle with E contractible, then there is a weak homotopy equivalence F → Ω B. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.67
For an arbitrary sequence of fibrations … → X_{2} → X_{1} the natural map λ: π_{i} (lim← X_{n}) → lim← π_{i} (X_{n}) is surjective, and λ is injective if the maps π_{i + 1} (X_{n}) {→ } π_{i + 1} (X_{n - 1}) are surjective for n sufficiently large.
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 arbitrary sequence of fibrations … → X_{2} → X_{1} the natural map λ: π_{i} (lim← X_{n}) → lim← π_{i} (X_{n}) is surjective, and λ is injective if the maps π_{i + 1} (X_{n}) {→ } π_{i + 1} (X_{n - 1}) are surjective for n sufficiently large. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.68
For the Postnikov tower {X_n} of a connected CW complex X, the natural map X→lim← X_n is a weak homotopy equivalence; equivalently, X is a CW approximation to the inverse limit.
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 Postnikov tower {X_n} of a connected CW complex X, the natural map X→lim← X_n is a weak homotopy equivalence; equivalently, X is a CW approximation to the inverse limit. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — principal fibration
A fibration is principal when it fits the commutative pullback-type diagram of §4.3 relating it to a pathspace fibration over a classifying map.
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 fibration is principal when it fits the commutative pullback-type diagram of §4.3 relating it to a pathspace fibration over a classifying map. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.69
A connected CW complex X has a Postnikov tower of principal fibrations iff π_{1} (X) acts trivially on π_{n} (X) for all 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 connected CW complex X has a Postnikov tower of principal fibrations iff π_{1} (X) acts trivially on π_{n} (X) for all n > 1. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4.70
Let (X,A) be a connected CW pair such that the homotopy fiber of A↪X is K(π,n), n≥1. Then there exists a fibration F→E→B and a map (X,A)→(E,F) inducing weak homotopy equivalences X→E and A→F iff the action of π₁(A) on π_{n+1}(X,A) is trivial.
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,A) be a connected CW pair such that the homotopy fiber of A↪X is K(π,n), n≥1. Then there exists a fibration F→E→B and a map (X,A)→(E,F) inducing weak homotopy equivalences X→E and A→F iff the action of π₁(A) on π_{n+1}(X,A) is trivial. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4.71
Every map f: X {→ } Y between connected CW complexes has a Moore– Postnikov tower, which is unique up to homotopy equivalence. A Moore–Postnikov tower of principal fibrations exists iff π_{1} (X) acts trivially on π_{n} (M_{f}, X) for all n > 1, where M_{f} is the mapping cylinder of 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: Every map f: X {→ } Y between connected CW complexes has a Moore– Postnikov tower, which is unique up to homotopy equivalence. A Moore–Postnikov tower of principal fibrations exists iff π_{1} (X) acts trivially on π_{n} (M_{f}, X) for all n > 1, where M_{f} is the mapping cylinder of f. No checked topological fibration-sequence/pathspace/homotopy-fiber/principal-fibration package realizes the row; covering-space lifting and generic pullbacks are insufficient. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — obstruction cocycle
When extending a map over successive skeleta, its restrictions to attaching spheres determine a cellular cochain with coefficients in π_n of the target; this is the obstruction cocycle, whose cohomology class is the obstruction to extension.
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 extending a map over successive skeleta, its restrictions to attaching spheres determine a cellular cochain with coefficients in π_n of the target; this is the obstruction cocycle, whose cohomology class is the obstruction to extension. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.72
A lift W → X_{n} extending the given A → X_{n} exists iff ω_{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: A lift W → X_{n} extending the given A → X_{n} exists iff ω_{n} = 0 No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4.73
If X is a connected abelian CW complex and (W, A) is a CW pair such that H^{n + 1} (W, A; π_{n} X) = 0 for all n, then every map A → X can be extended to a map W → 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 a connected abelian CW complex and (W, A) is a CW pair such that H^{n + 1} (W, A; π_{n} X) = 0 for all n, then every map A → X can be extended to a map W → X. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4.74
If X and Y are connected abelian CW complexes, then a map f: X {→ } Y inducing isomorphisms on all homology groups is a homotopy equivalence.
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 and Y are connected abelian CW complexes, then a map f: X {→ } Y inducing isomorphisms on all homology groups is a homotopy equivalence. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4A.1
There is a right action of π_{1} (X, x_{0}) on ⟨ Z, X ⟩ defined by setting [ f_{0} ] [ γ ] = [ f_{1} ] whenever there exists a homotopy f_{s}: Z → X from f_{0} to f_{1} such that f_{s} (z_{0}) is the loop γ, or any loop homotopic to γ.
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: There is a right action of π_{1} (X, x_{0}) on ⟨ Z, X ⟩ defined by setting [ f_{0} ] [ γ ] = [ f_{1} ] whenever there exists a homotopy f_{s}: Z → X from f_{0} to f_{1} such that f_{s} (z_{0}) is the loop γ, or any loop homotopic to γ. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4A.2
If (Z, z_{0}) is a CW pair and X is a path-connected space, then the natural map ⟨ Z, X ⟩ → [ Z, X ] induces a bijection of the orbit set ⟨ Z, X ⟩ / π_{1} (X, x_{0}) onto [ Z, 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 (Z, z_{0}) is a CW pair and X is a path-connected space, then the natural map ⟨ Z, X ⟩ → [ Z, X ] induces a bijection of the orbit set ⟨ Z, X ⟩ / π_{1} (X, x_{0}) onto [ Z, X ]. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4A.3
If X is an H–space with identity element x_{0}, then the action of π_{1} (X, x_{0}) on ⟨ Z, X ⟩ is trivial since for a map f: (Z, z_{0}) → (X, x_{0}) and a loop γ in X based at x_{0}, the multiplication in X defines a homotopy f_{s} (z) = f (z) γ (s). This starts and ends with a map homotopic to f, and the loop f_{s} (z_{0}) is homotopic to γ, both these homotopies being basepoint-preserving by the definition of an H-space.
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 an H–space with identity element x_{0}, then the action of π_{1} (X, x_{0}) on ⟨ Z, X ⟩ is trivial since for a map f: (Z, z_{0}) → (X, x_{0}) and a loop γ in X based at x_{0}, the multiplication in X defines a homotopy f_{s} (z) = f (z) γ (s). This starts and ends with a map homotopic to f, and the loop f_{s} (z_{0}) is homotopic to γ, both these homotopies being basepoint-preserving by the definition of an H-space. No checked obstruction-cocycle/obstruction-class theory for extending maps over CW skeleta was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Hopf invariant
For f:S{2n−1}→Sn, choose generators α∈H^n(C_f;ℤ) and β∈H^{2n}(C_f;ℤ); the integer H(f) defined by α²=H(f)β is the Hopf invariant.
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:S{2n−1}→Sn, choose generators α∈H^n(C_f;ℤ) and β∈H^{2n}(C_f;ℤ); the integer H(f) defined by α²=H(f)β is the Hopf invariant. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4B.1
The Hopf invariant H: π_{2 n - 1} (S^{n}) → ℤ is a 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 Hopf invariant H: π_{2 n - 1} (S^{n}) → ℤ is a homomorphism. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4B.2
π_{2 n - 1} (S^{n}) contains a Z direct summand when 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 n - 1} (S^{n}) contains a Z direct summand when n is even. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4C.1
Given a simply-connected CW complex X and chosen cyclic decompositions and generators of H_n(X), there is a CW complex Z and a cellular homotopy equivalence Z→X whose cells are generator n-cells representing the chosen homology generators and, for finite-order generators, relator (n+1)-cells whose cellular boundaries are the corresponding multiples of those generator cells.
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 a simply-connected CW complex X and chosen cyclic decompositions and generators of H_n(X), there is a CW complex Z and a cellular homotopy equivalence Z→X whose cells are generator n-cells representing the chosen homology generators and, for finite-order generators, relator (n+1)-cells whose cellular boundaries are the corresponding multiples of those generator cells. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4C.2
Suppose X is a simply-connected CW complex such that for some n ≥ 2, the only nonzero reduced homology groups of X are H_{n} (X), which is finitely generated, and H_{n + 1} (X), which is finitely generated and free. Hence Z is the wedge sum of spheres S^{n} and S^{n + 1} together with Moore spaces M (ℤ_{m}, n) of the form S^{n} ∪ e^{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: Suppose X is a simply-connected CW complex such that for some n ≥ 2, the only nonzero reduced homology groups of X are H_{n} (X), which is finitely generated, and H_{n + 1} (X), which is finitely generated and free. Hence Z is the wedge sum of spheres S^{n} and S^{n + 1} together with Moore spaces M (ℤ_{m}, n) of the form S^{n} ∪ e^{n + 1}. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4C.3
Let X be a simply-connected space homotopy equivalent to a CW complex, such that the only nontrivial reduced homology groups of X are H_{2} (X) ≅ ℤ^{m} and H_{4} (X) ≅ ℤ. Then the homotopy type of X is uniquely determined by the cup product ring H^{*} (X; ℤ). In particular, this applies to any simply-connected closed 4 manifold.
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 simply-connected space homotopy equivalent to a CW complex, such that the only nontrivial reduced homology groups of X are H_{2} (X) ≅ ℤ^{m} and H_{4} (X) ≅ ℤ. Then the homotopy type of X is uniquely determined by the cup product ring H^{*} (X; ℤ). In particular, this applies to any simply-connected closed 4 manifold. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4D.1
Let F→E→^pB be a fiber bundle and R a commutative ring. If each H^n(F;R) is finitely generated free and classes c_j∈H^{k_j}(E;R) restrict to an R-basis of H^(F;R) on every fiber, then Φ:H^(B;R)⊗_R H^(F;R)→H(E;R), b⊗i^c_j↦pb∪c_j, is an R-module isomorphism. Thus H^(E;R) is free over H^(B;R) on {c_j}.
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 F→E→^pB be a fiber bundle and R a commutative ring. If each H^n(F;R) is finitely generated free and classes c_j∈H^{k_j}(E;R) restrict to an R-basis of H^(F;R) on every fiber, then Φ:H^(B;R)⊗_R H^(F;R)→H(E;R), b⊗i^c_j↦pb∪c_j, is an R-module isomorphism. Thus H^(E;R) is free over H^(B;R) on {c_j}. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4D.2
Given a fiber bundle p: E → B and a subspace A ⊂ B such that (B, A) is k connected, then (E, p^{- 1} (A)) is also k 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: Given a fiber bundle p: E → B and a subspace A ⊂ B such that (B, A) is k connected, then (E, p^{- 1} (A)) is also k connected. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4D.3
There are ring isomorphisms H^(U(n);ℤ)≅Λ_ℤ[x₁,x₃,…,x_{2n−1}], H^(SU(n);ℤ)≅Λ_ℤ[x₃,x₅,…,x_{2n−1}], and H^*(Sp(n);ℤ)≅Λ_ℤ[x₃,x₇,…,x_{4n−1}], with the indicated odd-degree 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: There are ring isomorphisms H^(U(n);ℤ)≅Λ_ℤ[x₁,x₃,…,x_{2n−1}], H^(SU(n);ℤ)≅Λ_ℤ[x₃,x₅,…,x_{2n−1}], and H^*(Sp(n);ℤ)≅Λ_ℤ[x₃,x₇,…,x_{4n−1}], with the indicated odd-degree generators. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4D.4
If G_{n} (ℂ^{∞}) is the Grassmann manifold of n dimensional vector subspaces of ℂ^{∞}, then H^{} (G_{n} (ℂ^{∞}); ℤ) is a polynomial ring ℤ [ c_{1}, …, c_{n} ] on generators c_{i} of dimension 2 i. Similarly, H^{} (G_{n} (ℝ^{∞}); ℤ_{2}) is a polynomial ring ℤ_{2} [ w_{1}, …, w_{n} ] on generators w_{i} of dimension i, and H^{*} (G_{n} ({H }^{∞}); ℤ) ≅ ℤ [ q_{1}, …, q_{n} ] with q_{i} of dimension 4 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 G_{n} (ℂ^{∞}) is the Grassmann manifold of n dimensional vector subspaces of ℂ^{∞}, then H^{} (G_{n} (ℂ^{∞}); ℤ) is a polynomial ring ℤ [ c_{1}, …, c_{n} ] on generators c_{i} of dimension 2 i. Similarly, H^{} (G_{n} (ℝ^{∞}); ℤ_{2}) is a polynomial ring ℤ_{2} [ w_{1}, …, w_{n} ] on generators w_{i} of dimension i, and H^{*} (G_{n} ({H }^{∞}); ℤ) ≅ ℤ [ q_{1}, …, q_{n} ] with q_{i} of dimension 4 i. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4D.5
For a sphere bundle S^{n−1}→E→B with E contractible, the Gysin sequence gives H^(B;ℤ)≅ℤ[e] for n>1, with |e|=n; for n=1, H^(B;ℤ_2)≅ℤ_2[e]. Consequently such contractible-total-space sphere bundles can occur only for n=1,2,4.
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 sphere bundle S^{n−1}→E→B with E contractible, the Gysin sequence gives H^(B;ℤ)≅ℤ[e] for n>1, with |e|=n; for n=1, H^(B;ℤ_2)≅ℤ_2[e]. Consequently such contractible-total-space sphere bundles can occur only for n=1,2,4. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4D.6
For G_n=G_n(ℝ^∞), the universal double cover G̃_n is the space of oriented n-planes. The Gysin sequence has Euler class e=w₁ and gives H^*(G̃_n;ℤ_2)≅ℤ_2[w₁,…,w_n]/(w₁)≅ℤ_2[w₂,…,w_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_n=G_n(ℝ^∞), the universal double cover G̃_n is the space of oriented n-planes. The Gysin sequence has Euler class e=w₁ and gives H^*(G̃_n;ℤ_2)≅ℤ_2[w₁,…,w_n]/(w₁)≅ℤ_2[w₂,…,w_n]. No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4D.7
The complex analog G̃_n(ℂ∞)=V_n(ℂ∞)/SU(n) fits in S^1→G̃_n→G_n(ℂ^∞) and is 2-connected. Its Gysin sequence has e=±c₁ and yields H^*(G̃_n;ℤ)≅ℤ[c₁,…,c_n]/(c₁)≅ℤ[c₂,…,c_n]; this space is BSU(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 complex analog G̃_n(ℂ∞)=V_n(ℂ∞)/SU(n) fits in S^1→G̃_n→G_n(ℂ^∞) and is 2-connected. Its Gysin sequence has e=±c₁ and yields H^*(G̃_n;ℤ)≅ℤ[c₁,…,c_n]/(c₁)≅ℤ[c₂,…,c_n]; this space is BSU(n). No checked Hopf-invariant/minimal-cell-complex theorem or required cohomology-of-mapping-cones interface was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — fiber bundle pair
A fiber bundle pair consists of p:E→B with fiber F and a subspace E′⊂E such that p:E′→B is a bundle with fiber F′⊂F and the local trivializations of E′ are restrictions of those of E.
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 fiber bundle pair consists of p:E→B with fiber F and a subspace E′⊂E such that p:E′→B is a bundle with fiber F′⊂F and the local trivializations of E′ are restrictions of those of E. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4D.8
Suppose that (F, F^{‘}) → (E, E^{’}) → B is a fiber bundle pair such that H^{} (F, F^{′}; R) is a free R module, finitely generated in each dimension. If there exist classes c_{j} ∈ H^{} (E, E^{′}; R) whose restrictions form a basis for H^{} (F, F^{′}; R) in each fiber (F, F^{′}), then H^{} (E, E^{′}; R), as a module over H^{*} (B; R), is free with basis { c_{j} }.
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 that (F, F^{‘}) → (E, E^{’}) → B is a fiber bundle pair such that H^{} (F, F^{′}; R) is a free R module, finitely generated in each dimension. If there exist classes c_{j} ∈ H^{} (E, E^{′}; R) whose restrictions form a basis for H^{} (F, F^{′}; R) in each fiber (F, F^{′}), then H^{} (E, E^{′}; R), as a module over H^{*} (B; R), is free with basis { c_{j} }. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Thom class
For a disk bundle pair (Dn,S{n−1})→(E,E′)→B, a class c∈H^n(E,E′;R) whose restriction to each fiber generates Hn(Dn,S^{n−1};R)≅R is a Thom class.
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 disk bundle pair (Dn,S{n−1})→(E,E′)→B, a class c∈H^n(E,E′;R) whose restriction to each fiber generates Hn(Dn,S^{n−1};R)≅R is a Thom class. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4D.9
If the disk bundle (D^{n}, S^{n - 1}) → (E, E^{′}) → B has a Thom class c ∈ H^{n} (E, E^{′}; R), then the map Φ: H^{i} (B; R) {→ } H^{i + n} (E, E^{′}; R), Φ (b) = p^{*} (b) ∪ c, is an isomorphism for all i ≥ 0, and H^{i} (E, E^{′}; R) = 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: If the disk bundle (D^{n}, S^{n - 1}) → (E, E^{′}) → B has a Thom class c ∈ H^{n} (E, E^{′}; R), then the map Φ: H^{i} (B; R) {→ } H^{i + n} (E, E^{′}; R), Φ (b) = p^{*} (b) ∪ c, is an isomorphism for all i ≥ 0, and H^{i} (E, E^{′}; R) = 0 for i < n. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — Thom isomorphism and Thom space
The isomorphism Φ(b)=p^*(b)∪c is the Thom isomorphism. The Thom space T(E) is E/E′, collapsing the boundary sphere bundle to the basepoint.
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 isomorphism Φ(b)=p^*(b)∪c is the Thom isomorphism. The Thom space T(E) is E/E′, collapsing the boundary sphere bundle to the basepoint. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — orientable sphere bundle
A sphere bundle S^{n−1}→E′→B is orientable if for every loop γ in B the fiber transport L_γ induces the identity on H{n−1}(S{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 sphere bundle S^{n−1}→E′→B is orientable if for every loop γ in B the fiber transport L_γ induces the identity on H{n−1}(S{n−1};ℤ). FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — orientable disk bundle
A disk bundle is orientable when its boundary sphere subbundle is orientable.
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 disk bundle is orientable when its boundary sphere subbundle is orientable. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4D.10
Every disk bundle has a Thom class with ℤ_{2} coefficients, and orientable disk bundles have Thom classes with Z 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: Every disk bundle has a Thom class with ℤ_{2} coefficients, and orientable disk bundles have Thom classes with Z coefficients. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Euler class of an oriented sphere bundle
For a sphere bundle with Thom class c on the mapping-cylinder disk bundle M_p, the Euler class e∈H^n(B;R) is e=(p^){-1}j(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: For a sphere bundle with Thom class c on the mapping-cylinder disk bundle M_p, the Euler class e∈H^n(B;R) is e=(p^){-1}j(c). FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction/convention — Gysin sequence
Substituting the Thom isomorphism into the long exact cohomology sequence of the disk-bundle pair yields the long exact Gysin sequence of the sphere bundle.
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: Substituting the Thom isomorphism into the long exact cohomology sequence of the disk-bundle pair yields the long exact Gysin sequence of the sphere bundle. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4D.11
Suppose that S^{2 k - 1} → E → B is an orientable sphere bundle such that H^{} (E; R) is a polynomial ring R [ x_{1}, …, x_{ℓ} ] on even-dimensional generators x_{i}. Then H^{} (B; R) = R [ y_{1}, …, y_{ℓ}, e ] where e is the Euler class of the bundle and p^{*} (y_{i}) = x_{i} for each 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: Suppose that S^{2 k - 1} → E → B is an orientable sphere bundle such that H^{} (E; R) is a polynomial ring R [ x_{1}, …, x_{ℓ} ] on even-dimensional generators x_{i}. Then H^{} (B; R) = R [ y_{1}, …, y_{ℓ}, e ] where e is the Euler class of the bundle and p^{*} (y_{i}) = x_{i} for each i. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4D.12
For the infinite complex Grassmannian, H^*(G_n(ℂ^∞);ℤ)≅ℤ[c_1,…,c_n] with |c_i|=2i. Inductively, the sphere bundle S{2n-1}→E→G_n(ℂ∞) and the contractible-fiber bundle S∞→E→G_{n-1}(ℂ∞), together with the Gysin argument, adjoin the Euler/Chern class 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 the infinite complex Grassmannian, H^*(G_n(ℂ^∞);ℤ)≅ℤ[c_1,…,c_n] with |c_i|=2i. Inductively, the sphere bundle S{2n-1}→E→G_n(ℂ∞) and the contractible-fiber bundle S∞→E→G_{n-1}(ℂ∞), together with the Gysin argument, adjoin the Euler/Chern class c_n. FiberBundle and bundle pullbacks exist, but no checked bundle-pair Thom class/isomorphism, Euler class, Gysin sequence, or cohomology-of-bundles bridge realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4D.13
We have computed the cohomology of tilde(G){n} (ℝ^{∞}) with ℤ{2} coefficients, finding it to be a polynomial ring on generators in dimensions 2 through n, and now we compute the cohomology with ℤ_{p} coefficients for p an odd prime. There are two fiber bundles V_{2} (ℝ^{2 k + 1}) → E → tilde(G){2 k + 1} (ℝ^{∞}) V{2} (ℝ^{∞}) → E → tilde(G){2 k - 1} (ℝ^{∞}) where E is the space of triples (P, ν{1}, ν_{2}) with P an oriented (2 k + 1) plane in ℝ^{∞} and ν_{1} and ν_{2} two orthogonal unit vectors in P.
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 have computed the cohomology of tilde(G){n} (ℝ^{∞}) with ℤ{2} coefficients, finding it to be a polynomial ring on generators in dimensions 2 through n, and now we compute the cohomology with ℤ_{p} coefficients for p an odd prime. There are two fiber bundles V_{2} (ℝ^{2 k + 1}) → E → tilde(G){2 k + 1} (ℝ^{∞}) V{2} (ℝ^{∞}) → E → tilde(G){2 k - 1} (ℝ^{∞}) where E is the space of triples (P, ν{1}, ν_{2}) with P an oriented (2 k + 1) plane in ℝ^{∞} and ν_{1} and ν_{2} two orthogonal unit vectors in P. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4E.1
Every reduced cohomology theory on the category of basepointed CW complexes and basepoint-preserving maps has the form h^{n} (X) = ⟨ X, K_{n} ⟩ for some spectrum { 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: Every reduced cohomology theory on the category of basepointed CW complexes and basepoint-preserving maps has the form h^{n} (X) = ⟨ X, K_{n} ⟩ for some spectrum { K_{n} }. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4E.2
If h is a contravariant functor from the category of connected basepointed CW complexes to the category of pointed sets, satisfying the homotopy axiom (i){i}, the Mayer–Vietoris axiom, and the wedge axiom (iii), then there exists a connected CW complex K and an element u ∈ h (K) such that the transformation T{u}: . X, K. → h (X), T_{u} (f) = f^{*} (u), is a bijection for all 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 h is a contravariant functor from the category of connected basepointed CW complexes to the category of pointed sets, satisfying the homotopy axiom (i){i}, the Mayer–Vietoris axiom, and the wedge axiom (iii), then there exists a connected CW complex K and an element u ∈ h (K) such that the transformation T{u}: . X, K. → h (X), T_{u} (f) = f^{*} (u), is a bijection for all X. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4E.3
Given any pair (Z, z) with Z a connected CW complex and z ∈ h (Z), there exists a π_{*} universal pair (K, u) with Z a subcomplex of K and u | Z = z.
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 any pair (Z, z) with Z a connected CW complex and z ∈ h (Z), there exists a π_{*} universal pair (K, u) with Z a subcomplex of K and u | Z = z. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4E.4
Let (K, u) be a π_{} universal pair and let (X, A) be a basepointed CW pair. Then for each x ∈ h (X) and each map f: A → K with f^{} (u) = x | A there exists a map g: X {→ } K extending f with g^{*} (u) = 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 (K, u) be a π_{} universal pair and let (X, A) be a basepointed CW pair. Then for each x ∈ h (X) and each map f: A → K with f^{} (u) = x | A there exists a map g: X {→ } K extending f with g^{*} (u) = x. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4F.1
Stable homotopy groups π_{n}^{s} (X) define a reduced homology theory on the category of basepointed CW complexes and basepoint-preserving 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: Stable homotopy groups π_{n}^{s} (X) define a reduced homology theory on the category of basepointed CW complexes and basepoint-preserving maps. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — spectrum
A spectrum is a sequence of based CW complexes X_n with structure maps ΣX_n→X_{n+1}; it defines a generalized homology theory by stabilized homotopy groups of X∧X_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: A spectrum is a sequence of based CW complexes X_n with structure maps ΣX_n→X_{n+1}; it defines a generalized homology theory by stabilized homotopy groups of X∧X_n. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — homotopy groups of a spectrum
For a spectrum K, π_i(K)=lim→n π{i+n}(K_n), using the maps induced by suspension and the spectrum structure 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: For a spectrum K, π_i(K)=lim→n π{i+n}(K_n), using the maps induced by suspension and the spectrum structure maps. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4F.2
For a spectrum K, the groups h_{i} (X) = π_{i} (X ∧ K) form a reduced homology theory. When K is the Eilenberg–MacLane spectrum with K_{n} = K (G, n), this homology theory is ordinary homology, so π_{i} (X ∧ K) ≅ H̃_{i} (X; 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 a spectrum K, the groups h_{i} (X) = π_{i} (X ∧ K) form a reduced homology theory. When K is the Eilenberg–MacLane spectrum with K_{n} = K (G, n), this homology theory is ordinary homology, so π_{i} (X ∧ K) ≅ H̃_{i} (X; G). No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Construction — generalized homology theory from a spectrum
The homology theory represented by a spectrum agrees with that represented by its associated Ω-spectrum; theories satisfying the direct-limit axiom arise this way.
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 homology theory represented by a spectrum agrees with that represented by its associated Ω-spectrum; theories satisfying the direct-limit axiom arise this way. No checked Brown representability theorem or algebraic-topological spectrum/Ω-spectrum/stable homotopy theory was found. Mathlib “Spectrum” files concern unrelated analytic/ring spectra or spectral sequences. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/construction — diagram of spaces and amalgamation
A diagram of spaces assigns a space to each vertex of an oriented graph and a map to each edge. Its amalgamation ⨿X is the quotient of the coproduct by x∼f_e(x) along all edge maps.
Formalized. Mathlib/Combinatorics/Quiver/Prefunctor.lean::Prefunctor; Mathlib/CategoryTheory/PathCategory/Basic.lean::CategoryTheory.Paths, CategoryTheory.Paths.lift, CategoryTheory.Paths.lift_spec; Mathlib/CategoryTheory/Limits/Types/ColimitType.lean::CategoryTheory.Functor.ColimitTypeRel, CategoryTheory.Functor.ColimitType, CategoryTheory.Functor.ιColimitType_map; Mathlib/Topology/Category/TopCat/Limits/Basic.lean::TopCat.isColimitCoconeOfForget, TopCat.colimit_topology — Prefunctor is precisely vertex data plus a map for each oriented edge. Paths.lift freely extends it to the path category while lift_spec preserves each edge map. ColimitType is the quotient of the coproduct/sigma of the object spaces by the relation generated by diagram maps, and ιColimitType_map supplies the identifications; TopCat equips this underlying colimit with the final topology. Hence this is an equivalent formalization of Hatcher’s diagram-of-spaces amalgamation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition/construction — complex of spaces and iterated mapping cylinder
A complex of spaces over a Δ-complex assigns spaces to vertices and compatible maps to edges so every simplex gives a commutative string of maps; the associated iterated mapping cylinders are defined inductively from these strings.
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 of spaces over a Δ-complex assigns spaces to vertices and compatible maps to edges so every simplex gives a commutative string of maps; the associated iterated mapping cylinders are defined inductively from these strings. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Comparison — Borel construction as a realization
For a group G acting on X, the associated complex of spaces over BG has realization ΔX_G identifiable with (X×EG)/G=X×_G EG, the Borel construction.
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 group G acting on X, the associated complex of spaces over BG has realization ΔX_G identifiable with (X×EG)/G=X×_G EG, the Borel construction. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4G.1
If all the maps f_{ν} making up a map of complexes of spaces f: X {→ } Y are homotopy equivalences, then so is the map Δ f: Δ X → Δ Y.
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 maps f_{ν} making up a map of complexes of spaces f: X {→ } Y are homotopy equivalences, then so is the map Δ f: Δ X → Δ Y. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4G.2
When X_{U} is the complex of spaces associated to an open cover U = { X_{i} } of a paracompact space X, the map p: Δ X_{U} → ⊔ X_{U} = X is a homotopy equivalence.
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 X_{U} is the complex of spaces associated to an open cover U = { X_{i} } of a paracompact space X, the map p: Δ X_{U} → ⊔ X_{U} = X is a homotopy equivalence. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4G.3
If U is an open cover of a paracompact space X such that every nonempty intersection of finitely many sets in U is contractible, then X is homotopy equivalent to the nerve N {backslash } →.
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 cover of a paracompact space X such that every nonempty intersection of finitely many sets in U is contractible, then X is homotopy equivalent to the nerve N {backslash } →. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Convention — colimit and homotopy-colimit terminology
For diagrams of spaces, the amalgamation is commonly called a direct limit or colimit, while its realization ΔX is a homotopy direct limit, commonly “hocolim”; Hatcher uses the term realization.
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 diagrams of spaces, the amalgamation is commonly called a direct limit or colimit, while its realization ΔX is a homotopy direct limit, commonly “hocolim”; Hatcher uses the term realization. Ordinary graph-diagram colimits are formalized (U141), but no checked complex-of-spaces iterated mapping-cylinder realization, nerve theorem in this form, or homotopy-colimit realization owns the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — cofibration
A cofibration i:A→B is the arrow-dual of a fibration: it satisfies the homotopy extension property for maps out of B relative to 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: A cofibration i:A→B is the arrow-dual of a fibration: it satisfies the homotopy extension property for maps out of B relative to A. Mathlib has model-category cofibrations, but no topological cofibration defined by the Homotopy Extension Property; the model-category interface is not Hatcher’s arrow-dual topological notion. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4H.1
If i: A → B is a cofibration, then i is injective, and in fact a homeomorphism onto its image.
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 i: A → B is a cofibration, then i is injective, and in fact a homeomorphism onto its image. Mathlib has model-category cofibrations, but no topological cofibration defined by the Homotopy Extension Property; the model-category interface is not Hatcher’s arrow-dual topological notion. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — pushout
For maps f:Z→X and g:Z→Y, the pushout is the quotient of X⊔Y by the identifications f(z)∼g(z).
Formalized. Mathlib/CategoryTheory/Limits/Types/Pushouts.lean::CategoryTheory.Limits.Types.Pushout.Rel, CategoryTheory.Limits.Types.Pushout, CategoryTheory.Limits.Types.Pushout.cocone, CategoryTheory.Limits.Types.Pushout.isColimitCocone; Mathlib/Topology/Category/TopCat/Limits/Basic.lean::TopCat.isColimitCoconeOfForget, TopCat.colimit_topology — Types.Pushout.Rel generates exactly the identifications inl(f z) ~ inr(g z) on X ⊕ Y, and Types.Pushout is literally the corresponding quotient; its cocone is proved colimiting. TopCat.isColimitCoconeOfForget and colimit_topology put the final topology on that underlying quotient, giving exactly Hatcher’s topological pushout.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; Apache-2.0; Lean 4.33.0
Definition — homotopy groups with coefficients
For an abelian group G and Moore space M(G,n), π_n(X;G) is the set/group of based homotopy classes [M(G,n),X], in the dimensions where the group structure is defined.
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 and Moore space M(G,n), π_n(X;G) is the set/group of based homotopy classes [M(G,n),X], in the dimensions where the group structure is defined. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4H.2
For n>1 there is a natural short exact sequence 0→Ext(G,π_{n+1}(X))→π_n(X;G)→Hom(G,π_n(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: For n>1 there is a natural short exact sequence 0→Ext(G,π_{n+1}(X))→π_n(X;G)→Hom(G,π_n(X))→0. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4H.3
Every simply-connected CW complex has a homology decomposition.
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 simply-connected CW complex has a homology decomposition. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4I.1
If X and Y are CW complexes, then Σ (X × Y) ≃ Σ X {× } Σ Y {× } Σ (X ∧ Y)
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 and Y are CW complexes, then Σ (X × Y) ≃ Σ X {× } Σ Y {× } Σ (X ∧ Y) No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4I.2
Σ J (S^{n}) ≃ S^{n + 1} ∨ S^{2 n + 1} ∨ S^{3 n + 1} ∨ …. More generally, if X is a connected CW complex then Σ J (X) ≃ ∨_{n} Σ X^{∧ n} where X^{∧ n} denotes the smash product of n copies 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: Σ J (S^{n}) ≃ S^{n + 1} ∨ S^{2 n + 1} ∨ S^{3 n + 1} ∨ …. More generally, if X is a connected CW complex then Σ J (X) ≃ ∨_{n} Σ X^{∧ n} where X^{∧ n} denotes the smash product of n copies of X. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4I.3
For any prime power p^{n} the suspension Σ K (ℤ _ { p^{n} }, 1) is homotopy equivalent to a wedge sum X_{1} ∨ … ∨ X_{p - 1} where X_{i} is a CW complex having H̃_{*} (X_{i}; {ℤ }) nonzero only in dimensions congruent to 2 i mod 2 p - 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 any prime power p^{n} the suspension Σ K (ℤ _ { p^{n} }, 1) is homotopy equivalent to a wedge sum X_{1} ∨ … ∨ X_{p - 1} where X_{i} is a CW complex having H̃_{*} (X_{i}; {ℤ }) nonzero only in dimensions congruent to 2 i mod 2 p - 2. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4J.1
The map λ: J (X) → Ω Σ X is a weak homotopy equivalence for every connected CW complex 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: The map λ: J (X) → Ω Σ X is a weak homotopy equivalence for every connected CW complex X. No checked Moore-space homotopy-with-coefficients, homology-decomposition, stable splitting, or James-construction theorem realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4J.2
Let A be a graded algebra over a field F with A_{0} = F and let V be a graded vector space over F with V_{0} = 0. Suppose we have a linear map i: V → A preserving grading, such that the multiplication map μ: A ⊗ V → tilde(A), μ (a ⊗ ν) = a i (ν), is an isomorphism. Then the canonical algebra homomorphism i: T V → A extending the previous i is an isomorphism.
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 A be a graded algebra over a field F with A_{0} = F and let V be a graded vector space over F with V_{0} = 0. Suppose we have a linear map i: V → A preserving grading, such that the multiplication map μ: A ⊗ V → tilde(A), μ (a ⊗ ν) = a i (ν), is an isomorphism. Then the canonical algebra homomorphism i: T V → A extending the previous i is an isomorphism. TensorAlgebra.lift supplies the free-algebra universal property and Mathlib formalizes tensor-algebra gradings, but no checked theorem proves this specific multiplication-isomorphism criterion T(V) ≅ A. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4J.3
The suspension map π_{i} (X) → π_{i + 1} (Σ X) for an n connected CW complex X is an isomorphism if i ≤ 2 n and a surjection if i = 2 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: The suspension map π_{i} (X) → π_{i + 1} (Σ X) for an n connected CW complex X is an isomorphism if i ≤ 2 n and a surjection if i = 2 n + 1. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4J.4
π_{n + 1} (S^{n}) is ℤ_{2} for n ≥ 3, generated by the suspension or iterated suspension of the Hopf map.
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: π_{n + 1} (S^{n}) is ℤ_{2} for n ≥ 3, generated by the suspension or iterated suspension of the Hopf map. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4K.1
Let f: (X; A, B) → (Y; C, D) be a map of excisive triads. If the induced maps π_{i} (A, A ∩ B) {→ } π_{i} (C, C ∩ D) and π_{i} (B, A ∩ B) {→ } π_{i} (D, C ∩ D) are bijections for i < n and surjections for i = n, for all choices of basepoints, then the same is true of the induced maps π_{i} (X, A) → π_{i} (Y, C). By symmetry the conclusion holds also for the maps π_{i} (X, B) → π_{i} (Y, D).
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 f: (X; A, B) → (Y; C, D) be a map of excisive triads. If the induced maps π_{i} (A, A ∩ B) {→ } π_{i} (C, C ∩ D) and π_{i} (B, A ∩ B) {→ } π_{i} (D, C ∩ D) are bijections for i < n and surjections for i = n, for all choices of basepoints, then the same is true of the induced maps π_{i} (X, A) → π_{i} (Y, C). By symmetry the conclusion holds also for the maps π_{i} (X, B) → π_{i} (Y, D). No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4K.2
Given a map f: X {→ } Y and open covers { U_{i} } of X and { V_{i} } of Y with f (U_{i}) ⊂ V_{i} for all i, then if each restriction f: U_{i} → V_{i} and more generally each f: U _ { i_{1} } ∩ … ∩ U _ { i_{n} } → V _ { i_{1} } ∩ … ∩ V _ { i_{n} } is a weak homotopy equivalence, so is f: X {→ } Y.
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 a map f: X {→ } Y and open covers { U_{i} } of X and { V_{i} } of Y with f (U_{i}) ⊂ V_{i} for all i, then if each restriction f: U_{i} → V_{i} and more generally each f: U _ { i_{1} } ∩ … ∩ U _ { i_{n} } → V _ { i_{1} } ∩ … ∩ V _ { i_{n} } is a weak homotopy equivalence, so is f: X {→ } Y. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — quasifibration
For path-connected B, p:E→B is a quasifibration if π_i(E,p^{-1}(b),x_0)→π_i(B,b) is an isomorphism for all b, x_0 in the fiber, and i≥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 path-connected B, p:E→B is a quasifibration if π_i(E,p^{-1}(b),x_0)→π_i(B,b) is an isomorphism for all b, x_0 in the fiber, and i≥0. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Lemma 4K.3
A map p:E→B is a quasifibration if any one of these holds: (a) B=V_1∪V_2 with V_i open and the restrictions over V_1,V_2,V_1∩V_2 quasifibrations; (b) B=⋃B_n increasingly, every compact subset lies in some B_n, and each restriction over B_n is a quasifibration; (c) E deforms into E′ over a deformation of B into B′, E′→B′ is a quasifibration, and the time-one map on each fiber is a weak homotopy equivalence.
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 p:E→B is a quasifibration if any one of these holds: (a) B=V_1∪V_2 with V_i open and the restrictions over V_1,V_2,V_1∩V_2 quasifibrations; (b) B=⋃B_n increasingly, every compact subset lies in some B_n, and each restriction over B_n is a quasifibration; (c) E deforms into E′ over a deformation of B into B′, E′→B′ is a quasifibration, and the time-one map on each fiber is a weak homotopy equivalence. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4K.4
Polynomial factorization gives homeomorphisms SP_n(S2)≅ℂPn, compatible with the standard inclusions; hence SP(S2)≅ℂP∞. Similarly SP_n(S1)≃S1 for all n, including 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: Polynomial factorization gives homeomorphisms SP_n(S2)≅ℂPn, compatible with the standard inclusions; hence SP(S2)≅ℂP∞. Similarly SP_n(S1)≃S1 for all n, including n=∞. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4K.5
SP₂(S^n) is homeomorphic to the mapping cone of a map Sn(ℝP{n−1})→S^n, where Sn(ℝP{n−1}) denotes the n-fold unreduced suspension. Consequently H_(SP₂(S^n))≅H_(S^n)⊕H̃_*(S{n+1}(ℝP{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: SP₂(S^n) is homeomorphic to the mapping cone of a map Sn(ℝP{n−1})→S^n, where Sn(ℝP{n−1}) denotes the n-fold unreduced suspension. Consequently H_(SP₂(S^n))≅H_(S^n)⊕H̃_*(S{n+1}(ℝP{n−1})). No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4K.6
The functor X ↦ π_{i} S P (X) for i ≥ 1 coincides with the functor X ↦ H_{i} (X; ℤ) on the category of basepointed connected CW 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: The functor X ↦ π_{i} S P (X) for i ≥ 1 coincides with the functor X ↦ H_{i} (X; ℤ) on the category of basepointed connected CW complexes. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4K.7
A path-connected, commutative, associative H-space with a strict identity element has the weak homotopy type of a product of Eilenberg–MacLane 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 path-connected, commutative, associative H-space with a strict identity element has the weak homotopy type of a product of Eilenberg–MacLane spaces. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Comparison — Hurewicz map via the infinite symmetric product
Under π_i(SP(X))=H_i(X;ℤ), the map π_i(X)→π_i(SP(X)) induced by X=SP_1(X)↪SP(X) is the Hurewicz 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: Under π_i(SP(X))=H_i(X;ℤ), the map π_i(X)→π_i(SP(X)) induced by X=SP_1(X)↪SP(X) is the Hurewicz homomorphism. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4L.1
For fixed m, n, G, and H there is a bijection between the set of all cohomology operations Theta: H^{m} (X; G) → H^{n} (X; H) and H^{n} (K (G, m); H), defined by Theta ↦ Theta (ι) where ι ∈ H^{m} (K (G, m); G) is a fundamental class.
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 fixed m, n, G, and H there is a bijection between the set of all cohomology operations Theta: H^{m} (X; G) → H^{n} (X; H) and H^{n} (K (G, m); H), defined by Theta ↦ Theta (ι) where ι ∈ H^{m} (K (G, m); G) is a fundamental class. No checked Freudenthal/James/Dold–Thom/quasifibration/symmetric-product theorem or the stated loopspace/symmetric-product computation was found. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/data — Steenrod squares
The Steenrod squares are natural operations Sqi:Hn(X;ℤ_2)→H^{n+i}(X;ℤ_2), satisfying Sq^0=id, Sq^n(α)=α², instability, suspension stability, and the Cartan formula.
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 Steenrod squares are natural operations Sqi:Hn(X;ℤ_2)→H^{n+i}(X;ℤ_2), satisfying Sq^0=id, Sq^n(α)=α², instability, suspension stability, and the Cartan formula. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4L.2
If f: S^{2 n - 1} {→ } S^{n} has Hopf invariant 1, then [ f ] ∈ π_{n - 1}^{s} is nonzero, so the iterated suspensions Σ^{k} f: S^{2 n + k - 1} {→ } S^{n + k} are all homotopically nontrivial.
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^{2 n - 1} {→ } S^{n} has Hopf invariant 1, then [ f ] ∈ π_{n - 1}^{s} is nonzero, so the iterated suspensions Σ^{k} f: S^{2 n + k - 1} {→ } S^{n + k} are all homotopically nontrivial. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition/data — Steenrod powers
For odd prime p, the Steenrod powers Pi:Hn(X;ℤ_p)→H^{n+2i(p−1)}(X;ℤ_p) satisfy the analogous naturality, stability, instability, p-th-power, and Cartan properties.
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 odd prime p, the Steenrod powers Pi:Hn(X;ℤ_p)→H^{n+2i(p−1)}(X;ℤ_p) satisfy the analogous naturality, stability, instability, p-th-power, and Cartan properties. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4L.3
Steenrod operations tie all nonzero cohomology classes of ℝP^∞ together, so no suspension ΣkℝP∞ splits nontrivially as X∨Y with both factors having nonzero cohomology. The same argument gives no nontrivial stable splitting of ℂP^∞ or ℍP^∞.
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: Steenrod operations tie all nonzero cohomology classes of ℝP^∞ together, so no suspension ΣkℝP∞ splits nontrivially as X∨Y with both factors having nonzero cohomology. The same argument gives no nontrivial stable splitting of ℂP^∞ or ℍP^∞. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4L.4
If f:ℍP∞→ℍP∞ satisfies f^*(γ)=dγ for a generator γ∈H4(ℍP∞;ℤ), Steenrod powers imply that d must be a square. In contrast, every integer occurs as the degree of a self-map of ℂP^∞. The source further notes that the realizable degrees on ℍP^∞ are exactly 0 and the odd squares.
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:ℍP∞→ℍP∞ satisfies f^*(γ)=dγ for a generator γ∈H4(ℍP∞;ℤ), Steenrod powers imply that d must be a square. In contrast, every integer occurs as the degree of a self-map of ℂP^∞. The source further notes that the realizable degrees on ℍP^∞ are exactly 0 and the odd squares. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4L.5
Write n=2^r(2s+1). Steenrod-square obstructions show that S^{n−1} cannot have 2^r orthonormal tangent vector fields. For r≤3 this is sharp: ℂ, ℍ, and 𝕆 give exactly 2^r−1 such fields. The remaining case n≡0 mod 16 requires the sharper K-theoretic bound.
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: Write n=2^r(2s+1). Steenrod-square obstructions show that S^{n−1} cannot have 2^r orthonormal tangent vector fields. For r≤3 this is sharp: ℂ, ℍ, and 𝕆 give exactly 2^r−1 such fields. The remaining case n≡0 mod 16 requires the sharper K-theoretic bound. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4L.6
A Map of mod ±b {p } Hopf Invariant One. Let us describe a construction for a map f: S^{2 p} {→ } S^{3} such that in the mapping cone C_{f} = S^{3} ∪{f} e^{2 p + 1}, the first Steenrod power P^{1}: H^{3} (C{f}; ℤ_{p}) {→ } H^{2 p + 1} (C_{f}; ℤ_{p}) is nonzero, hence f is nonzero in π_{2 p - 3}^{s}. By construction there is a map C_{g} → C_{f} inducing an isomorphism on ℤ_{p} cohomology in dimensions 3 and 2 p + 1, so the operation P^{1} is nontrivial in H^{*} (C_{f}; ℤ_{p}) since this was true for C_{g}, the (2 p + 1) skeleton 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 Map of mod ±b {p } Hopf Invariant One. Let us describe a construction for a map f: S^{2 p} {→ } S^{3} such that in the mapping cone C_{f} = S^{3} ∪{f} e^{2 p + 1}, the first Steenrod power P^{1}: H^{3} (C{f}; ℤ_{p}) {→ } H^{2 p + 1} (C_{f}; ℤ_{p}) is nonzero, hence f is nonzero in π_{2 p - 3}^{s}. By construction there is a map C_{g} → C_{f} inducing an isomorphism on ℤ_{p} cohomology in dimensions 3 and 2 p + 1, so the operation P^{1} is nontrivial in H^{*} (C_{f}; ℤ_{p}) since this was true for C_{g}, the (2 p + 1) skeleton of X. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Example 4L.7
Moore Spaces. Let us use the operation S q^{2} to show that for n ≥ 2, the identity map of M (ℤ_{2}, n) has order 4 in the group of basepoint-preserving homotopy classes of maps M (ℤ_{2}, n) {→ } M (ℤ_{2}, n), with addition defined via the suspension structure on M (ℤ_{2}, n) = Σ M (ℤ_{2}, n - 1). Hence if the identity map of M (ℤ_{2}, n) has order 4, this short exact sequence cannot split.
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. Let us use the operation S q^{2} to show that for n ≥ 2, the identity map of M (ℤ_{2}, n) has order 4 in the group of basepoint-preserving homotopy classes of maps M (ℤ_{2}, n) {→ } M (ℤ_{2}, n), with addition defined via the suspension structure on M (ℤ_{2}, n) = Σ M (ℤ_{2}, n - 1). Hence if the identity map of M (ℤ_{2}, n) has order 4, this short exact sequence cannot split. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — Steenrod algebra
A_2 is the ℤ_2-algebra on noncommuting generators Sq^i modulo the Adem relations; A_p for odd p is defined analogously using P^i and the Bockstein.
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_2 is the ℤ_2-algebra on noncommuting generators Sq^i modulo the Adem relations; A_p for odd p is defined analogously using P^i and the Bockstein. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4L.8
There is a relation { S q^{i} = ∑{0 < j < i} a{j} S q^{i - j} S q^{j} } with coefficients a_{j} ∈ ℤ_{2} whenever i is not a power of 2. Similarly, if i is not a power of p there is a relation { P^{i} = ∑{0 < j < i} a{j} P^{i - j} P^{j} } with a_{j} ∈ ℤ_{p}.
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: There is a relation { S q^{i} = ∑{0 < j < i} a{j} S q^{i - j} S q^{j} } with coefficients a_{j} ∈ ℤ_{2} whenever i is not a power of 2. Similarly, if i is not a power of p there is a relation { P^{i} = ∑{0 < j < i} a{j} P^{i - j} P^{j} } with a_{j} ∈ ℤ_{p}. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4L.9
Suppose H^{*} (X; ℤ_{p}) is the polynomial algebra ℤ_{p} [ α ] on a generator α of dimension n, possibly truncated by the relation α^{m} = 0 for m > p. Then if p = 2, n must be a power of 2, and if p is an odd prime, n must be of the form p^{k} ℓ where ℓ is an even divisor of 2 (p - 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: Suppose H^{*} (X; ℤ_{p}) is the polynomial algebra ℤ_{p} [ α ] on a generator α of dimension n, possibly truncated by the relation α^{m} = 0 for m > p. Then if p = 2, n must be a power of 2, and if p is an odd prime, n must be of the form p^{k} ℓ where ℓ is an even divisor of 2 (p - 1). Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Corollary 4L.10
If H^{*} (X; ℤ) is a polynomial algebra ℤ [ α ], possibly truncated by α^{m} = 0 with m > 3, then | α | = 2 or 4.
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 H^{*} (X; ℤ) is a polynomial algebra ℤ [ α ], possibly truncated by α^{m} = 0 with m > 3, then | α | = 2 or 4. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Proposition 4L.11
If eta ∈ π_{1}^{s} is represented by the Hopf map S^{3} → S^{2}, then eta^{2} is nonzero in π_{2}^{s}. Similarly, the other two Hopf maps represent elements ν ∈ π_{3}^{s} and σ ∈ π_{7}^{s} whose squares are nontrivial in π_{6}^{s} and π_{1 4}^{s}.
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 eta ∈ π_{1}^{s} is represented by the Hopf map S^{3} → S^{2}, then eta^{2} is nonzero in π_{2}^{s}. Similarly, the other two Hopf maps represent elements ν ∈ π_{3}^{s} and σ ∈ π_{7}^{s} whose squares are nontrivial in π_{6}^{s} and π_{1 4}^{s}. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Definition — excess of an admissible monomial
For admissible Sq^I, the excess is Σ_j(i_j−2i_{j+1}); for odd p the analogous formula includes the p-multiples and Bockstein exponents.
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 admissible Sq^I, the excess is Σ_j(i_j−2i_{j+1}); for odd p the analogous formula includes the p-multiples and Bockstein exponents. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Convention — free commutative algebra
Here “free commutative algebra” means a polynomial algebra when p=2, and for odd p a polynomial algebra on even-dimensional generators tensored with an exterior algebra on odd-dimensional 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: Here “free commutative algebra” means a polynomial algebra when p=2, and for odd p a polynomial algebra on even-dimensional generators tensored with an exterior algebra on odd-dimensional generators. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4L.12
The operations S q^{i} satisfy the properties (1)–(7).
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 operations S q^{i} satisfy the properties (1)–(7). Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4L.13
The Adem relations hold for Steenrod squares.
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 Adem relations hold for Steenrod squares. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.
Theorem 4L.16
The operations P^{i} satisfy the properties (1)–(6) and the Adem relations.
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 operations P^{i} satisfy the properties (1)–(6) and the Adem relations. Current Mathlib code search for “Steenrod” reaches only EilenbergSteenrod.lean (homology-theory axioms), not Steenrod operations. No checked Sq/P operations, Adem relations, Steenrod algebra, admissible-basis/excess theorem, or associated K(G,n) calculation realizes the row. Strict bundle semantics reject specializations, adjacent constructions, isolated clauses/examples, and algebraic ingredients without the required topological bridge.