Bifunctors on homological complexes preserve homotopy equivalences

Let F : C₁ ⥤ C₂ ⥤ D be a bifunctor which is additive in each variable, and let mapBifunctor K₁ K₂ F c be the induced total complex of homological complexes K₁ and K₂ (for F the tensor product this is the tensor product of complexes). Mathlib's HomologicalComplex.mapBifunctorMapHomotopy₁ and HomologicalComplex.mapBifunctorMapHomotopy₂ show that mapBifunctorMap f₁ f₂ F c only depends on the homotopy classes of f₁ and f₂. The functoriality of mapBifunctorMap in the pair (f₁, f₂) comes from TauCeti.Algebra.Homology.Bifunctor.Basic. This file deduces that homotopy equivalences K₁ ≃ L₁ and K₂ ≃ L₂ induce a homotopy equivalence mapBifunctor K₁ K₂ F c ≃ mapBifunctor L₁ L₂ F c. In particular the homology of a tensor product of complexes only depends on the homotopy types of the factors, which is how the Künneth theorem reduces to complexes with zero differential.

Main definitions and results

• HomologicalComplex.mapBifunctorMap_id and HomologicalComplex.mapBifunctorMap_comp: functoriality of mapBifunctorMap in both variables simultaneously.
• HomotopyEquiv.mapBifunctor: the homotopy equivalence of total complexes induced by homotopy equivalences of the two factors.

noncomputable def HomotopyEquiv.mapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (e₁ : HomotopyEquiv K₁ L₁) (e₂ : HomotopyEquiv K₂ L₂) : HomotopyEquiv (K₁.mapBifunctor K₂ F c) (L₁.mapBifunctor L₂ F c)

Homotopy equivalences K₁ ≃ L₁ and K₂ ≃ L₂ induce a homotopy equivalence mapBifunctor K₁ K₂ F c ≃ mapBifunctor L₁ L₂ F c, given by mapBifunctorMap of the two homotopy equivalences and of their inverses.

@[simp]

theorem HomotopyEquiv.mapBifunctor_hom {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (e₁ : HomotopyEquiv K₁ L₁) (e₂ : HomotopyEquiv K₂ L₂) : (mapBifunctor F c e₁ e₂).hom = HomologicalComplex.mapBifunctorMap e₁.hom e₂.hom F c

The forward map of HomotopyEquiv.mapBifunctor.

@[simp]

theorem HomotopyEquiv.mapBifunctor_inv {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)} [F.Additive] [∀ (X₁ : C₁), (F.obj X₁).Additive] {c : ComplexShape J} [DecidableEq J] [TotalComplexShape c₁ c₂ c] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (e₁ : HomotopyEquiv K₁ L₁) (e₂ : HomotopyEquiv K₂ L₂) : (mapBifunctor F c e₁ e₂).inv = HomologicalComplex.mapBifunctorMap e₁.inv e₂.inv F c

The backward map of HomotopyEquiv.mapBifunctor.