Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-12
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.

The homology Kunneth sequence splits nonnaturally

Statement

Assume AC. For any commutative PID R and spaces X,Y, the homology Künneth short exact sequence admits an R-linear section of its Tor quotient in every degree n0. Consequently its middle term is abstractly the direct sum of its tensor and Tor terms. The section is constructed after choices; no natural choice of splitting is asserted.

Facts & Assumptions

[F1]

Topological Kunneth short exact sequence for homology gives the exact sequence 0KαWγQ0.

[F2]

The PID Kunneth sequence admits a section after choices supplies, for the tensor complex, maps r:VK and j:QV satisfying rα=1, βj=1, jβ=1αr, and rj=0.

[F3]

Singular product chain equivalence by simplex models supplies the shuffle homology isomorphism s:VW with inverse t, where V=Hn(C(X;R)RC(Y;R)). The topological maps of [F1] are α=sα, γ=βt. Assume The Axiom of Choice.

Proof

Given: R,X,Y,n and the maps in [F1]–[F3], under AC.

1.1

The singular complexes are nonnegative free PID complexes, so the section theorem [F2] applies. Define j=sj:QW and r=rt:WK. Then γj=βtsj=βj=1, rα=rtsα=1, and rj=rtsj=0. All maps are R-linear.

F1F2F3given
2.1

The remaining composite satisfies jγ=sjβt=s(1αr)t=1αr. Therefore (k,q)αk+jq and w(rw,γw) are inverse: one composite is (k,q)(k,q) using rj=0, γα=0 and the identity composites; the other is w(αr+jγ)w=w. This proves the direct-sum assertion with the actual cross product and quotient.

F1F2F3step 1.1
3.1

The maps r,j of [F2] use chosen retractions CpZpC and DqZqD, obtained by splitting the surjections onto Bp1C and Bq1D. No splitting of the inclusions BpCZpC is used. Since no compatibility of those retractions with all space maps is supplied, steps 1.1 and 2.1 assert existence of a section, without asserting its naturality. The canonical exact sequence itself retains its naturality from [F1]. This observation alone is not a proof that every possible natural section is impossible.

F1F2step 1.1step 2.1
4.1

At n=0, Q=0 and j is the unique map from zero; αr=1 gives the degree-zero cross-product isomorphism. If a factor is empty, K=V=W=Q=0 and every formula remains valid. If K=0, the section is the inverse of γ; if Q=0, no Tor summand is added. In degree zero on a pair of points, α sends the tensor of the two unit vertex classes to the unit product vertex class. AC is inherited from [F2] for arbitrary-rank cycle retractions and simultaneous degreewise choices; composing the maps adds no choices.

F1F2F3step 1.1step 2.1step 3.1

Depends on

Used by

Dependency tree · two levels

14 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