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 balanced Tor bifunctor
Definition
Assume Dependent Choice (DC), as in The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain, and work with supplied projective resolutions of the modules under consideration. For a right -module , a left -module , and , define to be either for a projective resolution of or for a projective resolution of , identified by The left and right projective constructions of Tor are naturally isomorphic. On module maps use the well-defined homology maps from Each resolution-defined Tor construction is covariant in both variables. The natural coherent identifications of The Tor balance isomorphism is natural and coherent under a change of resolutions make this a covariant bifunctor up to canonical change-of-resolution isomorphism, not literal equality between different resolution complexes.
DC licenses the comparison maps and homotopies in those suppliers. Existence of projective resolutions for arbitrary modules is a separate prerequisite, not a consequence asserted here of DC. When such existence and a system of resolutions have separately been supplied, this gives the usual Tor bifunctor on the corresponding module categories. Without DC, homology of a specified tensor-resolution complex is still defined; claiming the balanced bifunctor then requires explicit comparison and coherence data instead of silently invoking the DC-bearing theorems.
Depends on
- The left and right projective constructions of Tor are naturally isomorphic
- The Tor balance isomorphism is natural and coherent under a change of resolutions
- Each resolution-defined Tor construction is covariant in both variables
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
Used by
- Field Kunneth isomorphism for homology of products Corollary
- betti numbers of a finite local module Definition
- A polynomial PID has a nonzero Kunneth Tor class Example
- Homology of a product of spheres by Kunneth Example
- Localization is flat and has vanishing positive Tor Example
- Over a field the cross product itself is a natural isomorphism Example
- The simple module over dual numbers is not perfect Example
- Tor term in the homology of a product of real projective spaces Example
- Tor one of R modulo I and M is not always the I-torsion submodule of M False statement
- Vanishing Tor one does not require a projective factor False statement
- Dimension of the kernel modulo n-minus equals the next term (BGG 10.7) Lemma
- Local flatness criterion by regular parameters Lemma
- minimal free resolution reduces to zero differential Lemma
- projective dimension from last nonzero betti number Lemma
- regular element reduction preserves minimal resolution Lemma
- The cycle-boundary tensor sequence has the Kunneth kernel and cokernel Lemma
- The homological universal-coefficient Tor obstruction map Lemma
- The Kunneth Tor map Lemma
- Tor with the trivial module is computed by the weak BGG resolution Lemma
- Homology of the derived tensor product is tor Proposition
- Semisimple rings have vanishing positive Tor and Ext Proposition
- A left module is flat exactly when Tor one against every right module vanishes Theorem
- A right module is flat exactly when Tor one against every left module vanishes Theorem
- Flat dimension at most n is equivalent to the prescribed higher Tor vanishing Theorem
- Higher Tor over the integers vanishes Theorem
- Hochschild homology is Tor over the enveloping algebra Theorem
- Polynomial Hochschild homology from the diagonal Koszul complex Theorem
- The long exact Tor sequence in the left-module variable Theorem
- The long exact Tor sequence in the right-module variable Theorem
- Tor is symmetric over a commutative ring Theorem
- Tor one of a cyclic abelian group detects n-torsion Theorem
- Weak global dimension is Tor-detected and left-right symmetric Theorem
Dependency tree · two levels
23 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
- Weibel, An Introduction to Homological Algebra (standard reference, not scraped)