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.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_9, 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.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_9, 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.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, 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
Instances For
theorem
HomologicalComplex.mapBifunctorFlipIso_flip
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, 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