Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Gysin long exact sequence of an oriented sphere bundle

Statement

Assume AC. For an R-oriented rank-n bundle ξ in the scope of the general Thom theorem, including n=0, there is a natural exact sequence ⋯→Hk−n(B;R)→⌣eTh(ξ)Hk(B;R)→p∗Hk(S(ξ);R)→∂GHk−n+1(B;R)→⌣eTh(ξ)⋯ . For n≥2, with the preceding cohomological Serre convention, the Euler class is the transgression dn of the normalized generator of Hn−1(Sn−1;R). Ranks zero and one are covered by the pair sequence, but not by that path-connected-sphere Serre comparison.

Facts & Assumptions

Given: AC, the oriented metric bundle, its disk projection π, sphere projection p, and normalized Thom class.

[F1]

Long exact sequence of a pair in singular cohomology gives the natural sequence of (D(ξ),S(ξ)).

[F2]

Gysin pushforward for an oriented zero section identifies relative groups by Thom and the relative-to-absolute map by cup with eTh after radial retraction.

[F3]

Relative cup products are natural and connector-compatible fixes the product and connector signs.

[F4]

Serre edge homomorphisms and transgression and Cohomological Serre spectral sequence define the cohomological transgression through filtered cochain extensions.

[F5]

Gysin sequence from a sphere-fiber Serre spectral sequence gives the two-row Serre Gysin sequence for a path-connected cohomology sphere.

[A1]

The Axiom of Choice is used through [F2], [F4], and [F5].

Proof

technique · rewrite the disk/sphere pair sequence and compare its filtered cochain
1.1F1F2F3

The pair sequence [F1] contains Hk(D,S)→j∗Hk(D)→Hk(S)→Hk+1(D,S). Radial retraction identifies Hk(D) with Hk(B), and the Thom isomorphism [F2] identifies Hk(D,S) with Hk−n(B). Under these identifications the middle restriction is p∗ and [F2]–[F3] identify j∗ with a↦a⌣eTh(ξ).

1.2F2F3F4

Let n≥2 and let z be the normalized class of the sphere fiber. In the filtered-cochain definition [F4], survival of z to page n means choosing extensions over successive base skeleta whose coboundaries vanish through filtration n−1; dnz is represented by the remaining base-degree-n coboundary. Perform the same extensions inside the disk bundle. The fiber pair connector sends z to the normalized disk-pair generator, so the resulting relative class is uξ. Mapping it relative-to-absolute produces j∗uξ, and radial retraction produces eTh(ξ). Thus the very cochain that represents dnz represents eTh(ξ), with the positive pair connector and ordered fiber generator fixing the sign.

2.1F1F2F3step 1.1

Substitute the identifications of step 1.1 at every degree of [F1]. Define ∂G as the pair connector followed by the inverse Thom isomorphism. Exactness and naturality are preserved by isomorphism, giving the displayed long exact sequence and its pullback-natural ladders.

3.1F4F5step 2.1step 1.2

The sphere fiber has dimension n−1≥1, so [F5] applies with its symbol n replaced by n−1. Its only differential is precisely the dn of step 1.2, and its cup map is multiplication by that transgression. Hence its Serre sequence agrees term-for-term with step 2.1 and the two Euler classes are equal.

4.1F1F2F3F4F5A1step 1.1step 2.1step 1.2step 3.1∎

For n=0, D(ξ)=B, S(ξ)=∅, and the supplied Thom class is the orientation unit o∈H0(B;R). The two bundle maps are identities, so [F2] gives e=o and the cup map is multiplication by o, an isomorphism with inverse multiplication by o−1. Thus the sequence alternates these isomorphisms with zero groups; they are identities for the standard unit orientation o=1. For n=1, the pair sequence remains valid (an oriented line is covered directly), while [F5] is inapplicable because S0 is not path-connected. Empty bases, the zero ring, zero/unit Euler classes, negative degrees, both pair-sequence endpoints, the connector sign and identity pullbacks are included in steps 1.1–3.1. AC is used exactly through [A1]; rewriting the supplied pair sequence adds no choice. No splitting or converse is asserted.

Depends on

Dependency tree · 2 levels

Sources