Behavior of the action of a bifunctor on cochain complexes with respect to shifts #
In this file, given cochain complexes K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ and
a functor F : C₁ ⥤ C₂ ⥤ D, we define an isomorphism of cochain complexes in D:
CochainComplex.mapBifunctorShift₁Iso K₁ K₂ F xof typemapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧forx : ℤ.CochainComplex.mapBifunctorShift₂Iso K₁ K₂ F yof typemapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧fory : ℤ.
In the lemma CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, we obtain
that the two ways to deduce an isomorphism
mapBifunctor (K₁⟦x⟧) (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦x + y⟧ differ by the sign
(x * y).negOnePow.
These definitions and properties can be summarised by saysing that the bifunctor
F.map₂CochainComplex : CochainComplex C₁ ℤ ⥤ CochainComplex C₂ ℤ ⥤ CochainComplex D ℤ
commutes with shifts by ℤ.
@[reducible, inline]
abbrev
CochainComplex.HasMapBifunctor
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
:
The condition that ((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂ has
a total cochain complex.
Equations
- K₁.HasMapBifunctor K₂ F = HomologicalComplex.HasMapBifunctor K₁ K₂ F (ComplexShape.up ℤ)
Instances For
@[reducible, inline]
noncomputable abbrev
CochainComplex.mapBifunctor
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
[K₁.HasMapBifunctor K₂ F]
:
Given K₁ : CochainComplex C₁ ℤ, K₂ : CochainComplex C₂ ℤ,
a bifunctor F : C₁ ⥤ C₂ ⥤ D, this mapBifunctor K₁ K₂ F : CochainComplex D ℤ
is the total complex of the bicomplex obtained by applying F to K₁ and K₂.
Equations
- K₁.mapBifunctor K₂ F = HomologicalComplex.mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)
Instances For
@[reducible, inline]
noncomputable abbrev
CochainComplex.ιMapBifunctor
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
[K₁.HasMapBifunctor K₂ F]
(n₁ n₂ n : ℤ)
(h : n₁ + n₂ = n)
:
The inclusion of a summand (F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n
of the total cochain complex when n₁ + n₂ = n.
Equations
- K₁.ιMapBifunctor K₂ F n₁ n₂ n h = HomologicalComplex.ιMapBifunctor K₁ K₂ F (ComplexShape.up ℤ) n₁ n₂ n h
Instances For
def
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
:
((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
K₂ ≅ (HomologicalComplex₂.shiftFunctor₁ D x).obj
(((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)
Auxiliary definition for mapBifunctorShift₁Iso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x i x✝ : ℤ)
:
@[simp]
theorem
CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x i x✝ : ℤ)
:
instance
CochainComplex.instHasMapBifunctorObjIntShiftFunctor
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
:
((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).HasMapBifunctor K₂ F
noncomputable def
CochainComplex.mapBifunctorShift₁Iso
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
:
((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctor K₂ F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (K₁.mapBifunctor K₂ F)
The canonical isomorphism mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧.
This isomorphism does not involve signs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CochainComplex.ι_mapBifunctorShift₁Iso_hom_f
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
(n₁ n₂ n : ℤ)
(h : n₁ + n₂ = n)
(m₁ m : ℤ)
(hm₁ : m₁ = n₁ + x)
(hm : m = n + x)
:
CategoryTheory.CategoryStruct.comp
(((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).ιMapBifunctor K₂ F n₁ n₂ n h)
((K₁.mapBifunctorShift₁Iso K₂ F x).hom.f n) = CategoryTheory.CategoryStruct.comp ((F.map (K₁.shiftFunctorObjXIso x n₁ m₁ hm₁).hom).app (K₂.X n₂))
(CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F m₁ n₂ m ⋯)
((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso x n m hm).inv)
theorem
CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
(n₁ n₂ n : ℤ)
(h : n₁ + n₂ = n)
(m₁ m : ℤ)
(hm₁ : m₁ = n₁ + x)
(hm : m = n + x)
{Z : D}
(h✝ : ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (K₁.mapBifunctor K₂ F)).X n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).ιMapBifunctor K₂ F n₁ n₂ n h)
(CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorShift₁Iso K₂ F x).hom.f n) h✝) = CategoryTheory.CategoryStruct.comp ((F.map (K₁.shiftFunctorObjXIso x n₁ m₁ hm₁).hom).app (K₂.X n₂))
(CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F m₁ n₂ m ⋯)
(CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso x n m hm).inv h✝))
@[simp]
theorem
CochainComplex.mapBifunctorShift₁Iso_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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ L₁ : CochainComplex C₁ ℤ}
(f₁ : K₁ ⟶ L₁)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
[L₁.HasMapBifunctor K₂ F]
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap
((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁)
(CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ))
(L₁.mapBifunctorShift₁Iso K₂ F x).hom = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₁Iso K₂ F x).hom
((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map
(HomologicalComplex.mapBifunctorMap f₁ (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ)))
@[simp]
theorem
CochainComplex.mapBifunctorShift₁Iso_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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ L₁ : CochainComplex C₁ ℤ}
(f₁ : K₁ ⟶ L₁)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(x : ℤ)
[K₁.HasMapBifunctor K₂ F]
[L₁.HasMapBifunctor K₂ F]
{Z : HomologicalComplex D (ComplexShape.up ℤ)}
(h : (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).obj (L₁.mapBifunctor K₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap
((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁)
(CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ))
(CategoryTheory.CategoryStruct.comp (L₁.mapBifunctorShift₁Iso K₂ F x).hom h) = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₁Iso K₂ F x).hom
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map
(HomologicalComplex.mapBifunctorMap f₁ (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ)))
h)
def
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
:
((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂) ≅ (HomologicalComplex₂.shiftFunctor₂ D y).obj
(((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)
Auxiliary definition for mapBifunctorShift₂Iso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y i i✝ : ℤ)
:
@[simp]
theorem
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y i i✝ : ℤ)
:
instance
CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
:
K₁.HasMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F
noncomputable def
CochainComplex.mapBifunctorShift₂Iso
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
:
K₁.mapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F ≅ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)
The canonical isomorphism mapBifunctor K₁ (K₂⟦y⟧) F ≅ (mapBifunctor K₁ K₂ F)⟦y⟧.
This isomorphism involves signs: on the summand (F.obj (K₁.X p)).obj (K₂.X q), it is given
by the multiplication by (p * y).negOnePow.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CochainComplex.ι_mapBifunctorShift₂Iso_hom_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
(n₁ n₂ n : ℤ)
(h : n₁ + n₂ = n)
(m₂ m : ℤ)
(hm₂ : m₂ = n₂ + y)
(hm : m = n + y)
:
CategoryTheory.CategoryStruct.comp
(K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h)
((K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n) = (n₁ * y).negOnePow • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom)
(CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯)
((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv)
theorem
CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
(n₁ n₂ n : ℤ)
(h : n₁ + n₂ = n)
(m₂ m : ℤ)
(hm₂ : m₂ = n₂ + y)
(hm : m = n + y)
{Z : D}
(h✝ : ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor K₂ F)).X n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(K₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h)
(CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorShift₂Iso K₂ F y).hom.f n) h✝) = CategoryTheory.CategoryStruct.comp
((n₁ * y).negOnePow • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X n₁)).map (K₂.shiftFunctorObjXIso y n₂ m₂ hm₂).hom)
(CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯)
((K₁.mapBifunctor K₂ F).shiftFunctorObjXIso y n m hm).inv))
h✝
@[simp]
theorem
CochainComplex.mapBifunctorShift₂Iso_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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
{K₂ L₂ : CochainComplex C₂ ℤ}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
[K₁.HasMapBifunctor L₂ F]
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁)
((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).map f₂) F (ComplexShape.up ℤ))
(K₁.mapBifunctorShift₂Iso L₂ F y).hom = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso K₂ F y).hom
((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
(HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) f₂ F (ComplexShape.up ℤ)))
@[simp]
theorem
CochainComplex.mapBifunctorShift₂Iso_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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
{K₂ L₂ : CochainComplex C₂ ℤ}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(y : ℤ)
[K₁.HasMapBifunctor K₂ F]
[K₁.HasMapBifunctor L₂ F]
{Z : HomologicalComplex D (ComplexShape.up ℤ)}
(h : (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).obj (K₁.mapBifunctor L₂ F) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁)
((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).map f₂) F (ComplexShape.up ℤ))
(CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso L₂ F y).hom h) = CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₂Iso K₂ F y).hom
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).map
(HomologicalComplex.mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) f₂ F (ComplexShape.up ℤ)))
h)
theorem
CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso
{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]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(x y : ℤ)
[K₁.HasMapBifunctor K₂ F]
:
K₁.mapBifunctorShift₁Iso ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F x ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).mapIso (K₁.mapBifunctorShift₂Iso K₂ F y) = (x * y).negOnePow • ((CategoryTheory.shiftFunctor (CochainComplex C₁ ℤ) x).obj K₁).mapBifunctorShift₂Iso K₂ F y ≪≫ (CategoryTheory.shiftFunctor (CochainComplex D ℤ) y).mapIso (K₁.mapBifunctorShift₁Iso K₂ F x) ≪≫ (CategoryTheory.shiftFunctorComm (CochainComplex D ℤ) x y).app (K₁.mapBifunctor K₂ F)
noncomputable instance
CategoryTheory.Functor.instCommShiftCochainComplexIntObjMap₂CochainComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₁ : CochainComplex C₁ ℤ)
:
(F.map₂CochainComplex.obj K₁).CommShift ℤ
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(n : ℤ)
:
theorem
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(n : ℤ)
:
instance
CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
{K₁ L₁ : CochainComplex C₁ ℤ}
(f : K₁ ⟶ L₁)
:
noncomputable instance
CategoryTheory.Functor.instCommShiftCochainComplexIntObjFlipMap₂CochainComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₂ : CochainComplex C₂ ℤ)
:
(F.map₂CochainComplex.flip.obj K₂).CommShift ℤ
Equations
- One or more equations did not get rendered due to their size.
theorem
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(n : ℤ)
:
(commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom.app K₁ = (K₁.mapBifunctorShift₁Iso K₂ F n).hom
theorem
CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
(K₁ : CochainComplex C₁ ℤ)
(K₂ : CochainComplex C₂ ℤ)
(n : ℤ)
:
(commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).inv.app K₁ = (K₁.mapBifunctorShift₁Iso K₂ F n).inv
instance
CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
{K₂ L₂ : CochainComplex C₂ ℤ}
(g : K₂ ⟶ L₂)
:
noncomputable instance
CategoryTheory.Functor.instCommShift₂IntCochainComplexIntMap₂CochainComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
[∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F]
:
Equations
- F.instCommShift₂IntCochainComplexIntMap₂CochainComplex = { commShiftObj := inferInstance, commShift_map := ⋯, commShiftFlipObj := inferInstance, commShift_flip_map := ⋯, comm := ⋯ }