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]
:
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]
:
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
Instances For
@[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]
:
@[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)