feat: roadmap for algebraic topology of spaces and manifolds

[Paul-Lez]

• Develop van Kampen, relative and cellular homology, local coefficients, and spectral sequences.
• Add cohomology operations, duality, transfer, and manifold-facing calculations.

Sources: Hatcher, Spanier, Bredon, and Serre.

Motivating consumer: Levent PDF

AI assistance: Codex (GPT-5) and Codex 5.6 Sol.

[CBirkbeck]

Part of a deep adversarial review of the reusable-roadmap split — PRs #279–#284, reviewed 25 August 2026. This section covers #283 — Algebraic topology of spaces and manifolds.

Head reviewed: 79ad130a8cbb4645c5ee26367df7627889eba112

Verdict

Changes requested.

The roadmap is now genuinely reusable and has a much better internal dependency graph than the original six-sphere document. The remaining problems concern coefficient generality: several familiar short exact sequences and invariant/coinvariant statements are false over an arbitrary commutative ring unless extra hypotheses are displayed.

1. Split the Künneth theorem by coefficient regime

Eilenberg–Zilber and cross products can be developed over a general commutative ring. The familiar Künneth short exact sequence with a single Tor₁ term is not the general theorem over an arbitrary ring.

State separate results:

1. Field coefficients: the cross product is an isomorphism
   [
   H_(X;k)\otimes H_(Y;k)\cong H_*(X\times Y;k).
   ]

2. PID/hereditary coefficient ring: the standard natural short exact sequence with tensor and Tor₁, together with its noncanonical splitting.

3. General ring: a Künneth spectral sequence
   [
   E^2_{p,q}=\operatorname{Tor}^R_p(H_(X;R),H_(Y;R))
   \Longrightarrow H_*(X\times Y;R),
   ]
   or a collapse theorem under flatness/projectivity hypotheses.

“Exact Tor term and flatness hypotheses” is not sufficiently precise.

2. Make the universal coefficient theorem equally precise

For integral coefficients or a PID/hereditary ring, one obtains the familiar short exact sequence involving Hom and Ext¹. Over a general ring, higher Ext groups occur and the natural object is a spectral sequence.

State:

• the integral/PID short exact sequence;
• its naturality;
• that a splitting is generally noncanonical;
• the general-ring spectral sequence separately.

Do not advertise one short exact sequence at the full coefficient generality claimed in the introduction.

3. Separate chain-level transfer from homology invariants

For a finite regular covering with deck group (G), the universally valid formulas are

[
p_\operatorname{tr}=d,\mathrm{id},
\qquad
\operatorname{tr}p_=\sum_{g\in G}g_*.
]

The quotient of the singular chain complex by the deck action can be compared with chains downstairs. It does not follow over arbitrary coefficients that

[
H_(X/G;R)=H_(X;R)G
\quad\text{or}\quad
H(X/G;R)=H_(X;R)^G,
]

because invariants and coinvariants need not be exact.

The roadmap should supply:

• the chain-level quotient statement;
• the Cartan–Leray spectral sequence in general;
• invariants/coinvariants corollaries only when (|G|) is invertible in the coefficient ring, or under another exactness hypothesis;
• a separate statement for nonregular finite covers using the permutation local system.

4. A finite cover needs constant degree or componentwise degree

The acceptance check uses a single degree (d). A finite covering of a disconnected base can have different sheet numbers on different components.

Either assume the base connected, include a constant-fibre-cardinality hypothesis, or state the transfer formula componentwise using a locally constant degree function.

“including degree zero” should also be rewritten as “including the induced map on (H_0)” to avoid confusion with covering degree.

5. Pin the Serre spectral-sequence hypotheses

Stage 5 should state the exact fibration carrier and convergence conditions:

• Serre fibration or the precise fibre-bundle theorem which supplies it;
• a path-connected base, or a componentwise formulation;
• the monodromy local system;
• first-quadrant/bounded-below conditions;
• finite-type assumptions used for strong convergence;
• naturality under maps of fibrations.

A FiberBundle alone should not be treated as silently providing every homotopy-lifting theorem unless an exact Mathlib/Tau Ceti bridge is named.

6. State manifold hypotheses in duality

Mathlib's manifold classes do not automatically contain all separation and countability assumptions. Poincaré and Poincaré–Lefschetz duality should display the needed hypotheses, such as:

• Hausdorffness;
• second countability or paracompactness;
• finite dimension;
• boundarylessness or the chosen boundary model;
• compactness where a global fundamental class is used;
• connectedness where top homology is identified with one copy of the coefficient ring.

The orientation-local-system form should precede the orientable integral corollary.

7. Torsion-linking statements need exact dimension and finiteness assumptions

A nonsingular torsion linking pairing is not one undifferentiated consequence for every manifold. State:

• closed oriented manifold dimension;
• the complementary torsion degrees;
• finite generation/finite torsion hypotheses;
• the target ℚ/ℤ;
• symmetry sign and naturality.

8. The relative-chain carrier needs its comparison theorem in Suggested.lean

relativeSingularChainComplex is currently an arbitrary sorry functor. Seed the theorem which identifies it naturally with

[
C_(X)/C_(A)
]

and the short exact sequence of chain complexes. That is the architectural contract from which the long exact sequence must be derived.

9. Suggested.lean is still too small

The file has targets only for relative chains, Euler characteristic, and homological Whitehead. Add representative signatures for:

• groupoid van Kampen;
• excision and Mayer–Vietoris;
• the cellular chain complex and comparison map;
• transfer and the Cartan–Leray spectral sequence;
• local coefficients;
• cap product and Poincaré duality;
• relative Hurewicz.

These signatures are needed to verify that the chosen categories and variances compose.

What is already strong

• the roadmap is entirely reusable;
• maps and natural transformations remain visible;
• the groupoid form of van Kampen handles disconnected intersections;
• the chain relative homology → excision → cellular comparison is correctly ordered;
• local coefficients are included before duality and the Serre spectral sequence;
• actual CW structures are required;
• homological Whitehead is stated with the original map as the forward map of the equivalence;
• stable homotopy and surgery are kept out of scope.

Recommended disposition

Keep the roadmap. Correct the coefficient regimes and transfer statements, display the manifold/fibration hypotheses, and expand the representative Lean interfaces. After that I would expect it to be approvable.

---

Cross-roadmap notes (apply across the #279–#284 split)

• PRs #280, #282, #283, and #284 still use the Levent six-sphere PDF as the link in the PR body. These are now general-purpose roadmaps. The construction paper should be described only as a motivating consumer; each PR body should instead foreground the standard sources listed in its README.
• Every downstream roadmap should import or #check the exact representative interfaces of its supplier once those suppliers land. Prose references alone are not enough to prevent incompatible carriers.
• The intended merge order is:
  #279 and corrected #283 first; #280 after both; #281 after #279 and an exact algebraic toric supplier; #282 after #279 and a reconciled compact-Riemann-surface degree API; and #284 after corrected #283 plus its geometric-topology and Morse/transversality suppliers.

[Paul-Lez]

🤖 Addressed in d761bfd. The roadmap now separates Kunneth and UCT by coefficient regime; gives the chain-level transfer identities and Cartan--Leray form before exactness corollaries; handles covering degree componentwise; pins Serre convergence and manifold-duality hypotheses; and states the torsion-linking dimensions and finiteness conditions. Suggested.lean now exposes the relative quotient comparison and representative van Kampen, excision, cellular, transfer, local-coefficient, duality, and Hurewicz interfaces. The PR body foregrounds the standard sources and retains the Levent paper only as a motivating consumer.

[Paul-Lez]

🤖 Follow-up in 8635f3c: Added the concrete compactManifoldFiniteCWType supplier contract used by the downstream homotopy-spheres roadmap, including its model topology, CW structure, finiteness witness, and homotopy equivalence.

[CBirkbeck]

Part of the second deep review of the reusable-roadmap split — PRs #279–#284, reviewed 26 August 2026 against the updated heads. This section covers #283 — Algebraic topology of spaces and manifolds.

Head reviewed: 8635f3c1e3c1ab8ad0a5fe045acd8d0ac7fa7bc1

All six updated branches pass their current CI. The comments below concern the mathematics and the proposed public APIs, not elaboration failures.

What has been fixed

The coefficient-generalities are now stated correctly and carefully:

• general-ring Künneth and UCT spectral sequences;
• field isomorphisms;
• PID/hereditary-ring short exact sequences with non-natural splitting;
• Cartan–Leray rather than unconditional invariant/coinvariant formulas;
• explicit invertibility/exactness hypotheses;
• constant-degree and componentwise transfer formulations;
• explicit Serre-fibration and convergence hypotheses;
• precise manifold and torsion-linking hypotheses.

Suggested.lean is also substantially better: it now seeds the relative quotient complex, van Kampen, excision, Mayer–Vietoris, cellular comparison, transfer, Cartan–Leray, local coefficients, duality and finite-CW-type supplier.

There is one substantive error in the proposed relative-homotopy carrier.

Relative homotopy is not always a ℤ-module

The file defines

relativeHomotopyGroup (n : ℕ) (X : TopPair) : ModuleCat ℤ

for every n.

But relative homotopy has different algebraic structures in low degrees:

• pointed-set behavior at the bottom;
• a group in the appropriate degree range;
• an abelian group only from the stable low-degree threshold onward.

In particular, π₂(X,A) need not be abelian. Take

$$ (X,A)=(C(Y),Y) $$

where Y = S¹ ∨ S¹. Since the cone is contractible, the long exact sequence gives

$$ \pi_2(CY,Y)\cong\pi_1(Y)\cong F_2, $$

which is nonabelian. It cannot be an object of ModuleCat ℤ.

Use either:

• separate pointed-set, group and abelian-group carriers by degree; or
• define a module-valued relative homotopy group only for n ≥ 3.

For the relative Hurewicz theorem at n=2, the required abelianization/commutativity should be derived from the theorem's connectivity and simple-connectivity hypotheses, not built into the general definition.

A smaller API improvement would be to package regular deck transformations as homeomorphisms (or a homomorphism into Homeomorph E) rather than merely continuous self-maps with laws, although the displayed laws are enough to derive inverses.

Verdict

One substantive correction requested; otherwise close. Once the low-degree relative-homotopy carrier is fixed, this roadmap is in strong shape.

---

Cross-roadmap disposition (applies across #279–#284)

• #279: fix one gluing signature; then merge.
• #280: add the complex-linear analytic input and group-valued connecting API; then merge.
• #281: repair the lattice foundation and monomial-domain theorem before further review.
• #282: make cusp data primitive and resolve degree/Riemann–Hurwitz ownership.
• #283: fix the low-degree relative-homotopy carrier; then merge.
• #284: keep the revised README, but substantially rewrite Suggested.lean around genuine manifold orientations, tangent-bundle trivializations, collared boundary data and actual quadratic forms/formations.

[Paul-Lez]

🤖 Addressed in d67818f. Relative homotopy is now group-valued in degree 2, module-valued only from degree 3, and Hurewicz uses abelianization; the degree-2 commutativity comparison is derived from the connectivity hypotheses. Deck actions are also packaged by homeomorphisms.

[Paul-Lez]

🤖 Follow-up CI fix in 56ac4c8: replaced the fragile tactic proof of 2 ≤ 2 with Nat.le_refl 2, and named/reused the 2 ≤ i hypothesis in the relative Hurewicz contract. The focused Lean check now passes with only the expected sorry warnings.

[CBirkbeck]

Part of the third adversarial review of the reusable-roadmap split (#279–#284) and companion roadmaps (#288, #81, #250), reviewed 26 August 2026 against the current heads. This section covers #283 — Algebraic topology of spaces and manifolds.

Head reviewed: 56ac4c8a5ad2f0570fa3a11aa67bb98bf605fc2c

What has been fixed

The low-degree algebraic-structure error is repaired:

• relative homotopy in degree at least two is group-valued;
• degree two is abelianized only when needed;
• the module-valued carrier begins in degree at least three;
• the degree-two commutativity theorem is derived under simple-connectivity hypotheses.

Remaining issue: relative homotopy has no basepoint

The proposed declarations still take only

X : TopPair

and no chosen point of X.snd.

Mathlib's TopPair stores an embedded map $A\to X$; it does not store a point $a_0\in A$. Relative homotopy groups are based objects:

$$ \pi_n(X,A,a_0). $$

Without a₀:

• no boundary cube can be required to land at the correct distinguished point;
• the relative long exact sequence has no canonical basepoint;
• the definition cannot even be made for an empty subspace in the usual based form;
• basepoint-change and naturality cannot be stated honestly.

The clean repair is either:

structure BasedTopPair extends TopPair where
  basepoint : snd

with basepoint-preserving maps, or to pass (a₀ : X.snd) through every relative homotopy, boundary and Hurewicz declaration.

This is separate from the abelian/nonabelian correction and remains necessary.

Verdict

Changes requested; otherwise close.

---

Cross-roadmap dependency recommendation — Topology chain

AlgebraicTopology (with based relative homotopy)
    ↓
HomotopySpheres

HomotopySpheres should import the supplier declarations and expose its geometric quotient API rather than mirror shared carriers indefinitely.

Recommended disposition (all nine PRs)

1. Merge after routine CI: #279, #280, #281.
2. Small focused repairs: #283, #81.
3. Coordinate and repair together: #282 and #288.
4. Rewrite the representative architecture before merge: #284.
5. Complete the class-field endpoint and state the global-function-field scope: #250.

[Paul-Lez]

🤖 Addressed in 30ff661. Relative homotopy now takes a BasedTopPair with an actual basepoint : pair.snd; pair maps preserve that point, and the relative groups, induced maps, boundary, basepoint change, relative Hurewicz map, and low-degree statements all thread the based carrier. Lean LSP reports no errors for TauCetiRoadmap/AlgebraicTopology/Suggested.lean.