LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

Extending over one cell is equivalent to nullhomotoping the attaching sphere

Statement

Let $n \geq 0$ , and let $B = A \cup_{α} D^{n + 1}$ be obtained by attaching one cell along $α : S^{n} \to A$ , and let $f : A \to Y$ be continuous. Then $f$ extends to $B$ if and only if $f α : S^{n} \to Y$ is nullhomotopic.

Facts & Assumptions

[F1]

The attached space is the pushout of $S^{n} ↪ D^{n + 1}$ and $α : S^{n} \to A$ .

[F2]

$D^{n + 1}$ is the cone on $S^{n}$ , and a nullhomotopy of a sphere map descends to a map on that cone.

Proof

Given: The attachment and map in the statement.

1.1

Suppose $\overset{ˉ}{f} : B \to Y$ extends $f$ . Its restriction to the characteristic disk, composed with a radial contraction of $D^{n + 1}$ to its center, is a nullhomotopy of $\overset{ˉ}{f} ∣_{S^{n}} = f α$ .

1.2

Conversely, let $H : S^{n} \times I \to Y$ satisfy $H (-, 0) = f α$ and have constant terminal map. Collapsing $S^{n} \times {1}$ turns the cylinder into $C S^{n} ≅ D^{n + 1}$ , and [F2] makes $H$ descend to a map $F : D^{n + 1} \to Y$ with $F ∣_{S^{n}} = f α$ .

2.1

The maps $f$ on $A$ and $F$ on $D^{n + 1}$ agree on the attaching boundary. By [F1]'s pushout universal property they glue uniquely to a continuous map $\overset{ˉ}{f} : B \to Y$ extending $f$ . The two constructions are inverse existence implications and require no choice. $□$

F1step 1.1step 1.2

Used by

Incompatible choices do not define one global obstruction problem Counterexample
Primary cellular obstruction cochain Definition
Postnikov towers exist for connected CW complexes Theorem
Vanishing of the primary obstruction is equivalent to extension over the next skeleton Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

James Davis and Paul Kirk, Lecture Notes in Algebraic Topology (standard reference, not scraped)