Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-06
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 cohomology universal-coefficient sequence splits nonnaturally

Statement

Assume the Axiom of Choice. Let R be a PID, C a chain complex of free R-modules, G an R-module, and n∈Z. The cohomological UCT sequence 0→Ext⁡R1(Hn−1C,G)→HnHom⁡R(C,G)→ev⁡nHom⁡R(HnC,G)→0 splits after choosing a complement of ZnC in Cn. No splitting natural in the complex C is asserted.

Proof

Given: R,C,G,n as stated and the UCT sequence of The universal coefficient theorem for cohomology over a PID.

1.1givenconstruct

The exact sequence 0→ZnC→Cn→dnBn−1C→0 comes from The cycle-boundary short exact sequences for a free complex over a PID. Under AC, Boundaries and cycles in a free complex over a PID are free makes Bn−1C free and Free modules are projective, with the exact choice boundary makes it projective. Lift its identity through dn to choose a section s. Then 1−sdn factors through the inclusion ZnC→Cn as a projection π:Cn→ZnC restricting to the identity on cycles.

2.1step 1.1algebra

Write q:ZnC→HnC for the quotient. For f:HnC→G, define σ(f)=[fqπ]. The map fqπ:Cn→G is a cocycle: dn+1 lands in BnC⊆ZnC, where π is the identity and q is zero. This assignment is R-linear in f, so it defines a homomorphism into cohomology.

3.1step 2.1algebra∎

For a cycle z, (fqπ)(z)=f(qz), so ev⁡nσ(f)=f. Thus σ is a section of the surjection in the exact UCT sequence. Its construction uses the chosen projection; it supplies existence without asserting naturality in C.

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