theorem KunnethIsos.quasiIso_tensorHom {R : Type u_1} [CommRing R] [IsPrincipalIdealRing R] {C' C D' D : ChainComplex (ModuleCat R) ℕ} (f : C' ⟶ C) (g : D' ⟶ D) [∀ (n : ℕ), Module.Free R ↑(C'.X n)] [∀ (n : ℕ), Module.Free R ↑(C.X n)] [HomologicalComplex.HasTensor C' D'] [HomologicalComplex.HasTensor C D] [∀ (i : ℕ), (HomologicalComplex.tensorObj C' D').HasHomology i] [∀ (i : ℕ), (HomologicalComplex.tensorObj C D).HasHomology i] [∀ (i : ℕ), HomologicalComplex.HasHomology C' i] [∀ (i : ℕ), HomologicalComplex.HasHomology C i] [∀ (i : ℕ), HomologicalComplex.HasHomology D' i] [∀ (i : ℕ), HomologicalComplex.HasHomology D i] [QuasiIso f] [QuasiIso g] : QuasiIso (HomologicalComplex.tensorHom f g)

Tensor of quasi-isomorphisms is a quasi-isomorphism (Section 25 helper for the Künneth theorem). Over a principal ideal ring R, if f : C' ⟶ C and g : D' ⟶ D are quasi-isomorphisms of chain complexes of R-modules and the source complexes are degreewise free, then the induced map f ⊗ g : C' ⊗ D' ⟶ C ⊗ D on tensor-product complexes is again a quasi-isomorphism. Freeness of the source ensures that tensoring preserves homology, which is the key ingredient for the Künneth isomorphism in algebraic topology.