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.
Thom and Gysin constructions respect pullback and composition
Statement
Assume AC, let be a commutative unital ring, and let all bundles be -oriented numerable bundles over CW complexes or paracompact Hausdorff bases of CW type, as in the general Thom and Gysin theorems. Orientation-preserving pullback squares commute with Thom isomorphisms, Euler classes, zero-section Gysin maps, and the Gysin long exact sequence. For composable oriented zero sections where is an oriented bundle over , the composite has ordered normal bundle . If a compatible orientation-preserving identification of an iterated tubular neighborhood pair with the disk/sphere pair of this ordered sum is supplied, define the composite Gysin map using that identification and Thom multiplication. Then under the supplied iterated tubular/disk-pair identification. No canonical such identification is asserted.
Facts & Assumptions
Given: The ring, spaces, bundles, and orientations in the statement, together with orientation-preserving pullback data or the two composable zero sections.
Naturality and uniqueness of Thom classes gives naturality of normalized Thom classes.
External-product and Whitney-sum formulas for Thom classes gives the ordered-sum Thom formula and its Koszul convention.
Gysin pushforward for an oriented zero section defines each zero-section pushforward as Thom multiplication followed by the pair map. For the composite, the notation in the statement is defined only after the displayed compatible iterated pair identification is supplied.
Gysin long exact sequence of an oriented sphere bundle gives the natural exact ladder, while Vector-bundle pullback is canonically functorial identifies successive pullbacks.
The Axiom of Choice is used only through [F1]–[F4].
Proof
In an orientation-preserving pullback square, [F1] identifies the pulled-back Thom class. Pullback commutes with , relative cup product and the relative-to-absolute pair map, so the Thom isomorphism and [F3]'s Gysin map commute. Pulling back along the zero section gives Euler naturality, and [F4] supplies the resulting natural ladder of exact sequences.
For the composable zero sections, functoriality in [F4] identifies the restriction of the second normal bundle to as . The supplied iterated tubular identification orders the first normal directions as those of and the second as those of , hence identifies the composite normal bundle with .
Apply [F3] twice to . Under the iterated pair identification, the result is the relative-to-absolute image of cupped first with and then with the pullback of . Associativity makes this cup product . By [F1]–[F2], the parenthesized class is the Thom class of the ordered normal sum from step 1.2, so [F3] identifies the result with .
Empty bases and zero rings give unique zero maps. A rank-zero section has Thom class and Euler class and acts as an identity, so either rank may be zero; ranks one and point bases require no change. Identity pullback squares, zero inputs, both orders of the normal sum, both stages of the composite, and every Gysin-sequence endpoint are covered by steps 1.1–2.1. Reversing the order would introduce the Koszul sign from [F2], which is why the order is stated. AC is used exactly through [A1]; the two-stage calculation is finite and makes no choices.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
21 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, Chapter 23 §5 (standard reference, not scraped)