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.
Topological Kunneth short exact sequence for homology
Statement
Assume AC. Let be a commutative PID and any spaces. For there is a natural short exact sequence All indices are nonnegative, and an empty sum is zero. The left map is the singular cross product. Naturality is covariant in maps of both spaces; no choice of a splitting is part of this sequence.
Facts & Assumptions
The natural PID Kunneth sequence is exact gives the natural exact sequence for nonnegative arbitrary-rank free PID complexes, with left map and canonical Tor quotient .
Singular product chain equivalence by simplex models supplies a natural shuffle equivalence , with explicit inverse and homotopies. Its map on generators is The singular chain cross product on generators.
Singular coefficient chains are free on singular simplex sets, as specified in Singular cochain complex with coefficients. AC is assumed as in The Axiom of Choice.
Proof
Given: as stated. Put , , , and .
Both complexes are nonnegative and free in every degree by [F3], with no finite-rank assumption. Their tensor differential is exactly that in [F1] and [F2]. Thus [F1] applies and gives with the two direct sums in the statement. All tensor-degree diagonals are finite since .
A chain homotopy changes the image of a cycle by a boundary: if and , then . Hence the inverse and homotopies in [F2] give mutually inverse homology maps and . Put . Although a chain inverse was constructed, its homology map is uniquely ; thus is independent of any inverse choices.
Define the left arrow as . It sends to , the singular cross product of [F2]. It is injective because and are injective. For , exactly when , exactly when . Finally any equals for some , and , proving surjectivity. This verifies the exactness of the actual displayed arrows.
For maps and , naturality of the shuffle gives . Multiplying by the inverse maps yields . Naturality of in [F1] now gives both squares of the topological sequence. The left square also follows directly from the cycle cross-product formula. No chosen cycle projections appear in these arrows.
At , the Tor sum is empty and the cross product is an isomorphism . At , the sole Tor index pair is , as stated. Empty or gives zero complexes and a zero sequence. On the degree-zero class of a pair of point simplices, the cross product is that point in the product, including coefficient . AC is inherited from the free PID theorem [F1] for its cycle/boundary and resolution constructions; the shuffle equivalence introduces none. There is no upper-degree or dimension restriction.
Depends on
Used by
- Field Kunneth isomorphism for homology of products Corollary
- Fundamental classes and duality for spheres and tori Example
- Homology of a product of spheres by Kunneth Example
- Integral cohomology ring of a torus Example
- Tor term in the homology of a product of real projective spaces Example
- The homology Kunneth sequence splits nonnaturally Proposition
Dependency tree · two levels
17 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
- Miller, section 25, Theorem 25.15, printed page 66 (standard reference, not scraped)