TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-14

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Difference cochains classify homotopies of extensions in the stable stage

Statement

Assume AC. Let $(X, A)$ be a relative CW complex, let $n \geq 1$ , and let $Y$ be $(n - 1)$ -connected and $n$ -simple; when $n = 1$ , assume in particular that $π_{1} (Y)$ is abelian. Fix $a : A \to Y$ and put $Π = π_{n} (Y)$ with its resulting simple coefficient system.

Let $E_{n} (a)$ consist of maps $g : X^{n} \cup A \to Y$ extending $a$ whose obstruction cochain is zero, modulo homotopy rel $A$ on $X^{n} \cup A$ . Equivalently, these are the $n$ -stage maps which extend over $X^{n + 1} \cup A$ , with an extension chosen only when needed. If $E_{n} (a)$ is nonempty, then

$H^{n} (X, A; Π)$

acts freely and transitively on it. For $g_{0}, g_{1} \in E_{n} (a)$ , the displacement is the difference class

$[d (g_{0}, g_{1})] \in H^{n} (X, A; Π),$

and this class is zero if and only if $g_{0}$ and $g_{1}$ are homotopic rel $A$ through the $n$ -skeleton. For a finite relative CW pair, only finite choice is used.

Facts & Assumptions

[F1]

Since $Y$ is $(n - 1)$ -connected, every two extensions of $a$ are homotopic rel $A$ through $X^{n - 1} \cup A$ ; for $n = 1$ , abelianness makes the conjugation action simple.

[F2]

For a chosen prior-stage homotopy, $δ d (g_{0}, g_{1}) = θ (g_{0}) - θ (g_{1})$ (The primary obstruction class is independent of cellular choices).

[F3]

The difference-cochain construction uses one shifted prism cell for each relative cell and identifies its primary obstruction cochain with the signed difference cochain (Difference cochain between two cellular extensions).

[F4]

For every cellular $n$ -cochain $d$ , the vanishing-obstruction theorem constructs a map $f_{d}$ equal to $f$ on the prior skeleton and having prescribed difference $d (f, const, f_{d}) = d$ , by relative pinch maps and simultaneous choice; it makes no claim that $f$ and $f_{d}$ are homotopic on the $n$ -skeleton (Vanishing of the primary obstruction is equivalent to extension over the next skeleton).

[A1]

AC is used only to choose representatives and fillers for arbitrary cell families (The Axiom of Choice).

Proof

Given: $(X, A)$ , $Y$ , $a$ , and [A1] as in the statement.

1.1

Let $g_{0}, g_{1} \in E_{n} (a)$ . By [F1], choose a homotopy $H$ rel $A$ between their restrictions to $X^{n - 1} \cup A$ . Because $θ (g_{0}) = θ (g_{1}) = 0$ , [F2] gives $δ d (g_{0}, H, g_{1}) = 0$ . Thus the difference cochain defines a class in $H^{n} (X, A; Π)$ .

F1F2

1.2

Changing $H$ or changing either endpoint through a homotopy rel $A$ changes this cocycle by a coboundary: apply the obstruction-class independence theorem to the corresponding boundary map on the product pair. Hence $[d (g_{0}, g_{1})]$ depends only on the two classes in $E_{n} (a)$ . Reversing a prism changes its sign, and gluing prisms gives

$[d (g_{0}, g_{2})] = [d (g_{0}, g_{1})] + [d (g_{1}, g_{2})] .$

[F3]

2.1

Regard the homotopy problem as extension over the product pair in [F3]. Suppose $[d (g_{0}, H, g_{1})] = 0$ , and choose $c \in C^{n - 1} (X, A; Π)$ with $d (g_{0}, H, g_{1}) = δ c$ . Keep both endpoint maps fixed. On each relative prism $e^{n - 1} \times I$ , whose dimension is $n$ , insert by the relative pinch construction of [F4] a sphere representative of $- c (e^{n - 1})$ into the interior of $H$ , leaving its entire boundary, including the two endpoint faces, fixed. AC makes these simultaneous insertions over arbitrary cells; the CW pushout glues them to a new prior-stage homotopy $H_{c}$ rel $A$ with the same endpoints. On a boundary prism $e^{n} \times I$ , the only changed faces are the prisms over the $(n - 1)$ -cells of $\partial e^{n}$ . Their signed incidence sum, with the interval-last sign in [F3], is $- δ c (e^{n})$ ; the same oriented boundary calculation as [F2] therefore gives $d (g_{0}, H_{c}, g_{1}) = d (g_{0}, H, g_{1}) - δ c = 0$ as a cochain, not just as a class. The zero obstruction on each $e^{n} \times I$ now supplies a filling extending $H_{c}$ over the relative $n$ -prisms, while the fixed bottom and top faces remain $g_{0}$ and $g_{1}$ . The glued fillings are a homotopy $g_{0} ≃ g_{1}$ on $X^{n} \cup A$ rel $A$ . Conversely, such a homotopy fills every prism, making its difference cochain zero and hence its class zero.

A1F2F3F4step 1.1

2.2

Fix $g \in E_{n} (a)$ and let $z \in Z^{n} (X, A; Π)$ . Since $g$ has zero obstruction as in Step 1.1, apply [F4] to a stationary prior-stage homotopy and prescribe difference cochain $z$ . It produces $g_{z} : X^{n} \cup A \to Y$ with $d (g, c o n s t, g_{z}) = z$ . By [F2],

F2F4step 1.1

$θ (g_{z}) = θ (g) - δ z = 0,$

so $g_{z} \in E_{n} (a)$ . [F2, F4]

3.1

If $z$ and $z^{'}$ differ by a coboundary, Step 1.2 gives $[d (g_{z}, g_{z^{'}})] = [z^{'} - z] = 0$ , so Step 2.1 makes $g_{z}$ and $g_{z^{'}}$ equivalent. Thus Step 2.2 defines an action of $H^{n} (X, A; Π)$ on $E_{n} (a)$ . The addition formula in Step 1.2 proves the action law.

step 1.2step 2.1step 2.2

4.1

For any $g_{0}, g_{1}$ , the class $[d (g_{0}, g_{1})]$ sends $g_{0}$ to $g_{1}$ , proving transitivity. If a class fixes $g_{0}$ , its displacement is zero by Step 2.1, proving freeness. AC enters only in [F4] and in simultaneous extension over arbitrary cell families; finite families need only finite choice. Empty cell sets, $A = X$ , and the zero group give the asserted singleton torsors. $□$

A1step 2.1step 3.1

Depends on

Used by

Eilenberg--Mac Lane spaces represent singular cohomology Theorem

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

James Davis and Paul Kirk, Lecture Notes in Algebraic Topology (standard reference, not scraped)
Haynes Miller, MIT 18.906 Algebraic Topology II lecture notes (standard reference, not scraped)