ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Cofiber sequence of a wedge summand inclusion

Example

For well-pointed based CGWH spaces U,V, the summand inclusion $U ↪ U \lor V$ is a cofibration with quotient V. Its Puppe connecting map $V \to Σ U$ is based nullhomotopic. For example, the inclusion of the first circle in $S^{1} \lor S^{1}$ has cofiber equivalent to the second circle and zero connecting map.

Facts & Assumptions

[F1]

The wedge identifies the two basepoints and no other points. The wedge of a family of pointed spaces

[F2]

Pushouts preserve cofibrations. Pushouts and products preserve the cofibrations used here

[F3]

The cofiber is formed by attaching the reduced cone. Reduced cone suspension and cofiber sequence

[F4]

For a based cofibration collapsing its cone yields the quotient homotopy equivalence. Cofiber of a based cofibration is equivalent to the quotient

Verification

Given: The spaces, maps, and hypotheses in the statement above.

1.1F1F2F4

The inclusion U→U∨V is the pushout of the basepoint inclusion {* }→V along {* }→U. That inclusion is an unbased cofibration by well-pointedness, so F2 proves the claim. Collapsing U identifies the remaining V only at its existing basepoint, and compatible quotient maps in both directions give $(U \lor V) / U ≅ V$ . F4 consequently identifies its cofiber with V up to based homotopy.

2.1F1F2F3F4step 1.1∎

More explicitly that cofiber is $C U \lor V$ : the original U is the base of the attached cone. On CU use $[u, s] \mapsto [u, s + t - s t]$ and keep V fixed. At t=0 this is the identity, at t=1 all of CU is the tip, and the basepoint track is fixed. The quotient-times-I construction in F2 makes this a continuous based deformation onto V. The cofiber projection to ΣU collapses all of V, so its composite with the inclusion V→CU∨V is identically the basepoint. Under this explicit inverse of the equivalence, the connecting map is therefore constant. For U=V=S1 this gives the stated two-circle instance.

Remarks

The first three arrows below are the cofiber sequence in its explicit cone model. Here $i$ is the summand inclusion, $a$ includes the wedge in its cofiber, $q$ collapses that wedge, $j$ includes the remaining summand, and $r$ collapses $C U$ .

The map $r$ is the cone-collapse equivalence $C_{i} \to (U \lor V) / U ≅ V$ of step 1.1: the quotient identification with $V$ is a based homeomorphism, whereas $C_{i} ≃ V$ is a based homotopy equivalence. Step 2.1 gives $r j = {id}_{V}$ , $j r ≃ {id}_{C_{i}}$ through based maps, and $q j = *$ exactly. Thus the connecting map represented on $V$ by $q j$ is constant. The diagram illustrates these constructions; the verification above proves them independently.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

May, A Concise Course in Algebraic Topology (standard reference, not scraped)