Action of the flip of a bifunctor on homological complexes

Given K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂, a bifunctor F : C₁ ⥤ C₂ ⥤ D, and a complex shape c with [TotalComplexShape c₁ c₂ c] and [TotalComplexShape c₂ c₁ c], we define an isomorphism mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c under the additional assumption [TotalComplexShapeSymmetry c₁ c₂ c].

theorem HomologicalComplex.hasMapBifunctor_flip_iff {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] : K₂.HasMapBifunctor K₁ F.flip c ↔ K₁.HasMapBifunctor K₂ F c

instance HomologicalComplex.instHasMapBifunctorFlip {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] : K₂.HasMapBifunctor K₁ F.flip c

noncomputable def HomologicalComplex.mapBifunctorFlipIso {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] : K₂.mapBifunctor K₁ F.flip c ≅ K₁.mapBifunctor K₂ F c

The canonical isomorphism mapBifunctor K₂ K₁ F.flip c ≅ mapBifunctor K₁ K₂ F c.

Equations

• K₁.mapBifunctorFlipIso K₂ F c = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalFlipIso c

@[simp]

theorem HomologicalComplex.ι_mapBifunctorFlipIso_hom {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₂.π c₁ c (i₂, i₁) = j) : CategoryTheory.CategoryStruct.comp (K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j hj) ((K₁.mapBifunctorFlipIso K₂ F c).hom.f j) = c₁.σ c₂ c i₁ i₂ • K₁.ιMapBifunctor K₂ F c i₁ i₂ j ⋯

@[simp]

theorem HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₂.π c₁ c (i₂, i₁) = j) {Z : D} (h : (K₁.mapBifunctor K₂ F c).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j hj) (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorFlipIso K₂ F c).hom.f j) h) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K₁.ιMapBifunctor K₂ F c i₁ i₂ j ⋯) h

@[simp]

theorem HomologicalComplex.ι_mapBifunctorFlipIso_inv {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₁.π c₂ c (i₁, i₂) = j) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj) ((K₁.mapBifunctorFlipIso K₂ F c).inv.f j) = c₁.σ c₂ c i₁ i₂ • K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j ⋯

@[simp]

theorem HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₁.π c₂ c (i₁, i₂) = j) {Z : D} (h : (K₂.mapBifunctor K₁ F.flip c).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj) (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorFlipIso K₂ F c).inv.f j) h) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j ⋯) h

theorem HomologicalComplex.mapBifunctorFlipIso_flip {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] [TotalComplexShapeSymmetry c₂ c₁ c] [TotalComplexShapeSymmetrySymmetry c₁ c₂ c] : K₂.mapBifunctorFlipIso K₁ F.flip c = (K₁.mapBifunctorFlipIso K₂ F c).symm

@[simp]

theorem HomologicalComplex.mapBifunctorFlipIso_hom_naturality {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} (φ₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} (φ₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] : CategoryTheory.CategoryStruct.comp (mapBifunctorMap φ₂ φ₁ F.flip c) (L₁.mapBifunctorFlipIso L₂ F c).hom = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorFlipIso K₂ F c).hom (mapBifunctorMap φ₁ φ₂ F c)

@[simp]

theorem HomologicalComplex.mapBifunctorFlipIso_hom_naturality_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{v_1, u_1} C₁] [CategoryTheory.Category.{v_2, u_2} C₂] [CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} (φ₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂} (φ₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [TotalComplexShape c₂ c₁ c] [TotalComplexShapeSymmetry c₁ c₂ c] [DecidableEq J] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] {Z : HomologicalComplex D c} (h : L₁.mapBifunctor L₂ F c ⟶ Z) : CategoryTheory.CategoryStruct.comp (mapBifunctorMap φ₂ φ₁ F.flip c) (CategoryTheory.CategoryStruct.comp (L₁.mapBifunctorFlipIso L₂ F c).hom h) = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorFlipIso K₂ F c).hom (CategoryTheory.CategoryStruct.comp (mapBifunctorMap φ₁ φ₂ F c) h)