Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

Stabilizing a framed submanifold suspends its Pontryagin-Thom map

Statement

Assume ACω. For d≥0, k≥1, equatorial stabilization of a closed framed d-submanifold (N,φ) of Sd+k satisfies PT(σ(N,φ))=E(PT(N,φ))∈πd+k+1(Sk+1). The new equatorial normal is prepended, agreeing with the new first smash coordinate in the sphere-prespectrum convention. Thus the levelwise bijections intertwine stabilization and suspension.

Facts & Assumptions

Given: (N,φ) as above, its equatorial stabilization, and the suspension map E.

[F1]

The stabilized framing prepends the chosen equatorial normal, and stabilization respects framed cobordism (Stabilized framed cobordism and the framed bordism group).

[F2]

The sphere-prespectrum bonding map uses S1∧Sk≅Sk+1 with the new coordinate first (Suspension and sphere prespectra, Stable stems of the sphere). Smash products and their coherence are Smash product of based spaces and Canonical associativity, symmetry, and unit maps for smash products.

[F3]

The normalized collapse is smooth, constant off a small tube, and has its given framing as centre differential (The Pontryagin-Thom map of a framed submanifold). A continuous sphere-valued map smooth near a regular fibre is homotopic to the collapse of that framed fibre (The collapse of a regular preimage is homotopic to the original map).

[F4]

The fixed-codimension correspondence and the based/free identification are The Pontryagin-Thom correspondence in fixed codimension and Based and free homotopy classes of maps between spheres agree.

Proof

1.1F1F3F4construct

Choose a point outside N, possible because a positive-codimension submanifold has empty interior. A plane-rotation path can move that point to the chosen sphere basepoint; transporting N and its framing along this path gives a framed cobordism (flatten the time at its ends). Thus we may choose a representative avoiding the basepoint. Take its tube small enough to avoid that point too. Its collapse f is then based on Sn itself, n=d+k, and constant on a neighbourhood of its basepoint, with f−1(y0)=N and centre differential φ.

2.1F1F2F3step 1.1construct

Write the sphere complements as Rn and Rk, choosing an equatorial stereographic chart of the next sphere in which the equator is {0}×Rn and the chosen new normal points in the positive first coordinate. The smash S1∧Sn is the one-point compactification of R×Rn: the quotient of the compact product of the two one-point compactifications has exactly this open complement of its collapsed wedge, and its neighbourhoods at the collapsed point have compact complements. Under this identification idS1∧f is F(t,x)=(t,z(f(x)))(f(x)≠∞),F(t,x)=∞(f(x)=∞). It is continuous by the smash quotient, represents E[f], and near its centre fibre it is smooth. Its centre preimage is exactly {0}×N, with normal differential (a,v)↦(a,φ(v)), the prepended framing of [F1]. This is a statement about the class, not an assertion that a radial stabilized tube collapse equals a suspension pointwise.

3.1F3F4step 2.1∎

By the continuous local-smooth version of [F3], F is homotopic to the collapse of its framed centre preimage, namely σ(N,φ). Hence its free class is PT(σ(N,φ)), and [F4] identifies the corresponding based classes. Since [F]=E[f], the desired identity follows. Both constructions respect classes, so it gives a map of directed systems.

Depends on

Used by

Dependency tree · two levels

58 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