The action of a bifunctor on homological complexes factors through homotopies

Given a TotalComplexShape c₁ c₂ c, a functor F : C₁ ⥤ C₂ ⥤ D, we show in this file that up to homotopy the morphism mapBifunctorMap f₁ f₂ F c only depends on the homotopy classes of the morphism f₁ in HomologicalComplex C c₁ and of the morphism f₂ in HomologicalComplex C c₂.

noncomputable def HomologicalComplex.mapBifunctorMapHomotopy.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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (j j' : J) : (K₁.mapBifunctor K₂ F c).X j ⟶ (L₁.mapBifunctor L₂ F c).X j'

Auxiliary definition for mapBifunctorMapHomotopy₁.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.mapBifunctorMapHomotopy.ι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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j) (h' : c₁.prev i₁' = i₁) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (hom₁ h₁ f₂ F c j j') = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))

theorem HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j) (h' : c₁.prev i₁' = i₁) {Z : D} (h✝ : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (CategoryTheory.CategoryStruct.comp (hom₁ h₁ f₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))) h✝

noncomputable def HomologicalComplex.mapBifunctorMapHomotopy.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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (j j' : J) : (K₁.mapBifunctor K₂ F c).X j ⟶ (L₁.mapBifunctor L₂ F c).X j'

Auxiliary definition for mapBifunctorMapHomotopy₂.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.mapBifunctorMapHomotopy.ι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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ : I₁) (i₂ i₂' : I₂) (j j' : J) (h : c₁.π c₂ c (i₁, i₂') = j) (h' : c₂.prev i₂' = i₂) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h) (hom₂ f₁ h₂ F c j j') = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂')) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))

theorem HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (i₁ : I₁) (i₂ i₂' : I₂) (j j' : J) (h : c₁.π c₂ c (i₁, i₂') = j) (h' : c₂.prev i₂' = i₂) {Z : D} (h✝ : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h) (CategoryTheory.CategoryStruct.comp (hom₂ f₁ h₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂')) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))) h✝

theorem HomologicalComplex.mapBifunctorMapHomotopy.zero₁ {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (j j' : J) (h : ¬c.Rel j' j) : hom₁ h₁ f₂ F c j j' = 0

theorem HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] {i₁ i₁' : I₁} (hi₁ : c₁.Rel i₁ i₁') {i₂ i₂' : I₂} (hi₂ : c₂.Rel i₂ i₂') (j : J) (hj : c₁.π c₂ c (i₁', i₂) = j) : c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) = -CategoryTheory.CategoryStruct.comp ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j)) (hom₁ h₁ f₂ F c (c.next j) j)

theorem HomologicalComplex.mapBifunctorMapHomotopy.comm₁ {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] (j : J) : (mapBifunctorMap f₁ f₂ F c).f j = CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctor K₂ F c).d j (c.next j)) (hom₁ h₁ f₂ F c (c.next j) j) + CategoryTheory.CategoryStruct.comp (hom₁ h₁ f₂ F c j (c.prev j)) ((L₁.mapBifunctor L₂ F c).d (c.prev j) j) + (mapBifunctorMap f₁' f₂ F c).f j

noncomputable def HomologicalComplex.mapBifunctorMapHomotopy₁ {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁' f₂ F c)

The homotopy between mapBifunctorMap f₁ f₂ F c and mapBifunctorMap f₁' f₂ F c that is induced by a homotopy between f₁ and f₁'.

Equations

• HomologicalComplex.mapBifunctorMapHomotopy₁ h₁ f₂ F c = { hom := HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c, zero := ⋯, comm := ⋯ }

noncomputable def HomologicalComplex.mapBifunctorMapHomotopy₂ {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] [CategoryTheory.Preadditive C₁] [CategoryTheory.Preadditive C₂] [CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (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₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c)

The homotopy between mapBifunctorMap f₁ f₂ F c and mapBifunctorMap f₁ f₂' F c that is induced by a homotopy between f₂ and f₂'.

Equations

• HomologicalComplex.mapBifunctorMapHomotopy₂ f₁ h₂ F c = { hom := HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c, zero := ⋯, comm := ⋯ }