Let and be resolutions of -modules and .
Let be a morphism of -modules.
If is projective then lifts to a morphism , that is, a morphism of complexes which induces on homology.
Moreover, any two lifts of are homotopic.
Proof`
Consider the diagram
Since the horizontal rows are exact, that means that is surjective, so because is projective, there exists a lift .
Now, for any element then we have
as .
This means that .
Note that is surjective onto its image which is a submodule of so by projectivity of then there exists a lift .
This can be repeated indefinitely, so the lift exists.
Next, suppose that are two lifts of .
We can construct a homotopy by induction.
Considering the diagram above, looking at the far right square, we have
This implies that , that is factors through .
In other words, there is a map such that
Assume that have been constructed in a similar way.
We need to construct such that
Applying the same strategy as above, we compute
Thus, factors through so the homotopy exists as above.
Homotopy equivalence
Let be an -module.
Any two projective resolutions of are homotopy equivalent.
Proof
Let be projective resolutions of .
Applying the theorem above to the identity map gives two lifts
Then and also lift as do and .
Therefore, and are homotopic and similarly and are homotopic.
The big idea!
Let be an -module.
Consider the complexes from tensoring with , and .
Let be a morphism that lifts .
Then the tensor map
is a morphism of complexes, and thus there is a morphism of homologies
Additionally, any lift of is a homotopy inverse of .
This means that is an inverse of and
This implies the definition of the Tor groups are independent of a choice of projective resolutions up to isomorphism.