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.
Degree-zero Tor is the tensor product in either construction
Statement
For a right -module and a left -module over any unital ring, supplied projective resolutions in either variable give canonical degree-zero identifications with . No choice axiom is needed once the resolutions are supplied.
Proof
Given: a projective resolution and a projective resolution .
Write and . The complex is concentrated in nonnegative degrees, so its degree-zero homology is the abelian group , by Tor from a projective resolution of the left module. The balanced formula induces by Universal property of the tensor product for balanced maps into abelian groups, since .
For and , define using any lift . Any two lifts differ by , so their classes agree. Sums and scalar multiples of lifts show that is additive in both variables and . Thus the tensor universal property gives . This definition uses unique classes, not a simultaneous selection of lifts.
The composites and fix respectively and . These elements generate the two abelian groups, so the maps are inverse.
Write and . For the right-resolved construction in Tor from a projective resolution of the right module, use . The augmentation gives ; its inverse sends to for any . Differences of lifts belong to , so the class is unique, and balancing follows from using as a lift of . Both composites fix the generating tensors, proving the second canonical identification.
Depends on
Used by
Dependency tree · two levels
10 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
- Charles A. Weibel, An Introduction to Homological Algebra (standard reference, not scraped)