LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

A framed cobordism of regular preimages produces a homotopy

Statement

Assume ${A C}_{ω}$ . Let $M$ be a closed smooth $m$ -manifold, $m \geq 1$ , and let $f, g : M \to S^{m}$ be smooth. Suppose $y, y^{'} \in S^{m}$ are regular values with positive bases $b, b^{'}$ and the framed regular preimages $(f^{- 1} (y), f_{*} b)$ and $(g^{- 1} (y^{'}), g_{*} b^{'})$ are framed cobordant in $M$ . Then $f$ and $g$ are smoothly homotopic, hence homotopic.

Facts & Assumptions

Given: A closed smooth $m$ -manifold $M$ , smooth maps $f, g : M \to S^{m}$ , regular values $y, y^{'}$ with positive bases $b, b^{'}$ , and a framed cobordism between the framed preimages $(f^{- 1} (y), f_{*} b)$ and $(g^{- 1} (y^{'}), g_{*} b^{'})$ (Framed regular preimages of a map to a sphere, Framed cobordism of framed submanifolds, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For a smooth map $h : M \to S^{m}$ , a regular value $z$ with positive basis $c$ and the framed preimage $(h^{- 1} (z), h_{*} c)$ , the Pontryagin-Thom map $f_{(h^{- 1} (z), h_{*} c)} : M \to S^{m}$ of that framed submanifold is homotopic to $h$ (The Pontryagin-Thom map of a framed submanifold, The collapse of a regular preimage is homotopic to the original map).

[F2]

Framed cobordant closed framed codimension- $m$ submanifolds of the closed manifold $M$ have homotopic Pontryagin-Thom maps $M \to S^{m}$ ; a framed cobordism supplies an explicit homotopy of the based maps (Framed cobordant submanifolds have homotopic Pontryagin-Thom maps, The Pontryagin-Thom map of a framed submanifold).

[F3]

Continuous homotopies concatenate and reverse. Under ${A C}_{ω}$ , continuously homotopic smooth maps are smoothly homotopic (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Continuously homotopic smooth maps are smoothly homotopic).

Proof

technique · direct

1.1F1given

Write $f_{0} : = f_{(f^{- 1} (y), f_{*} b)}$ and $g_{0} : = f_{(g^{- 1} (y^{'}), g_{*} b^{'})}$ for the Pontryagin-Thom maps of the two framed preimages. By [F1], applied to $h = f, z = y, c = b$ and to $h = g, z = y^{'}, c = b^{'}$ , there are continuous homotopies from $f$ to $f_{0}$ and from $g$ to $g_{0}$ , so it suffices to connect $f_{0}$ and $g_{0}$ .

1.2F2given

The hypothesis that the two framed preimages are framed cobordant in $M$ , together with [F2], gives a homotopy from $f_{0}$ to $g_{0}$ , in fact an explicit one induced by the cobordism.

2.1F3step 1.1step 1.2∎

Concatenate the homotopy $f ≃ f_{0}$ , the homotopy $f_{0} ≃ g_{0}$ , and the reversal of $g ≃ g_{0}$ . This gives a continuous homotopy $f ≃ g$ by [F3]. Since the endpoint maps $f, g$ are smooth, the smoothing theorem in [F3] then supplies a smooth homotopy with these endpoints. It is not necessary that the middle collapse homotopy be smooth.

Depends on

Used by

Dependency tree · two levels

46 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

Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
John Milnor, Topology from the Differentiable Viewpoint (standard reference, not scraped)