The associator for actions of bifunctors on homological complexes

In this file, we shall adapt (TODO) the results of the file CategoryTheory.GradedObject.Associator to the case of homological complexes. Given functors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃ equipped with an isomorphism associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃ (which informally means that we have natural isomorphisms G(F₁₂(X₁, X₂), X₃) ≅ F(X₁, G₂₃(X₂, X₃))), we shall define an isomorphism mapBifunctorAssociator from mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ to mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄ when we have three homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, assumptions TotalComplexShape c₁ c₂ c₁₂, TotalComplexShape c₁₂ c₃ c₄, TotalComplexShape c₂ c₃ c₂₃, TotalComplexShape c₁ c₂₃ c₄, and ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄ about the complex shapes, and technical assumptions [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] and [HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] about the commutation of certain functors to certain coproducts.

The main application of these results shall be the construction of the associator for the monoidal category structure on homological complexes (TODO).

@[reducible, inline]

abbrev HomologicalComplex.HasGoodTrifunctor₁₂Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] : Type (max (max (max (max (max (max u_9 u_10) u_6) u_3) u_16) u_17) u_7 u_8)

Given bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂, G : C₁₂ ⥤ C₃ ⥤ C₄, homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, and complexes shapes c₁₂, c₄, this asserts that for all i₁₂ : ι₁₂ and i₃ : ι₃, the functor G(-, K₃.X i₃) commutes with the coproducts of the F₁₂(X₁ i₁, X₂ i₂) such that π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂.

Equations

• HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X

@[reducible, inline]

abbrev HomologicalComplex.HasGoodTrifunctor₂₃Obj {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)) (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] : Type (max (max (max (max (max (max u_7 u_11) u_6) u_4) u_16) u_17) u_8 u_9)

Given bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃, homological complexes K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and K₃ : HomologicalComplex C₃ c₃, and complexes shapes c₁₂, c₂₃, c₄ with ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄, this asserts that for all i₁ : ι₁ and i₂₃ : ι₂₃, the functor F(K₁.X i₁, _) commutes with the coproducts of the G₂₃(K₂.X i₂, K₃.X i₃) such that π c₂ c₃ c₂₃ ⟨i₂, i₃⟩ = i₂₃.

Equations

• HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ (c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c₄) K₁.X K₂.X K₃.X

instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXπ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_13, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₁₂ : Type u_10} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (c₁₂ : ComplexShape ι₁₂) [TotalComplexShape c₁ c₂ c₁₂] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ ι₁ ι₂).obj K₁.X).obj K₂.X).HasMap (c₁.π c₂ c₁₂)

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_16, u_1} C₁] [CategoryTheory.Category.{u_17, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] : (((CategoryTheory.GradedObject.mapBifunctor G ι₁₂ ι₃).obj (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ (c₁.π c₂ c₁₂) K₁.X K₂.X)).obj K₃.X).HasMap (c₁₂.π c₃ c₄)

Equations

• ⋯ = ⋯

instance HomologicalComplex.instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_15, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_17, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_14, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₂₃] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] : (((CategoryTheory.GradedObject.mapBifunctor F ι₁ ι₂₃).obj K₁.X).obj (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ (c₂.π c₃ c₂₃) K₂.X K₃.X)).HasMap (c₁.π c₂₃ c₄)

Equations

• ⋯ = ⋯

noncomputable def HomologicalComplex.mapBifunctorAssociatorX {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Category.{u_18, u_4} C₂₃] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₂₃] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)} {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [G₂₃.PreservesZeroMorphisms] [∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).Additive] (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₂₃] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [TotalComplexShape c₂ c₃ c₂₃] [TotalComplexShape c₁ c₂₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [K₂.HasMapBifunctor K₃ G₂₃ c₂₃] [K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] [c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [H₁₂ : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] [H₂₃ : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j : ι₄) : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ≅ (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j

The associator isomorphism for the action of bifunctors on homological complexes, in each degree.

Equations

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

noncomputable def HomologicalComplex.mapBifunctor₁₂.ι {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) : (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.

Equations

• HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X i₁ i₂ i₃ j h

theorem HomologicalComplex.mapBifunctor₁₂.ι_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (i₁₂ : ι₁₂) (j : ι₄) (h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) (h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j) : HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j ⋯ = CategoryTheory.CategoryStruct.comp ((G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ i₁₂ h₁₂)).app (K₃.X i₃)) ((K₁.mapBifunctor K₂ F₁₂ c₁₂).ιMapBifunctor K₃ G c₄ i₁₂ i₃ j h)

noncomputable def HomologicalComplex.mapBifunctor₁₂.ιOrZero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) : (G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j

The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄, or zero.

Equations

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

theorem HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) : HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h

theorem HomologicalComplex.mapBifunctor₁₂.ιOrZero_eq_zero {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)) (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) ≠ j) : HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0

theorem HomologicalComplex.mapBifunctor₁₂.hom_ext_iff {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} {f : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A} {g : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A} : f = g ↔ ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) g

theorem HomologicalComplex.mapBifunctor₁₂.hom_ext {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} {f : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A} {g : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A} (hfg : ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j), CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) g) : f = g

noncomputable def HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_13, u_1} C₁] [CategoryTheory.Category.{u_14, u_2} C₂] [CategoryTheory.Category.{u_15, u_5} C₃] [CategoryTheory.Category.{u_16, u_6} C₄] [CategoryTheory.Category.{u_17, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)) : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ A

Constructor for morphisms from (mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j.

Equations

• HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f = CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorDesc f

@[simp]

theorem HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) {Z : C₄} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h✝) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f) h) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ i₃ h✝) h

@[simp]

theorem HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctor₁₂Desc {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6} [CategoryTheory.Category.{u_17, u_1} C₁] [CategoryTheory.Category.{u_16, u_2} C₂] [CategoryTheory.Category.{u_14, u_5} C₃] [CategoryTheory.Category.{u_13, u_6} C₄] [CategoryTheory.Category.{u_15, u_3} C₁₂] [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Limits.HasZeroMorphisms C₃] [CategoryTheory.Preadditive C₁₂] [CategoryTheory.Preadditive C₄] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)} {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} [F₁₂.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [G.Additive] [∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₄ : Type u_12} [DecidableEq ι₁₂] [DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃} {c₁₂ : ComplexShape ι₁₂} {c₄ : ComplexShape ι₄} [TotalComplexShape c₁ c₂ c₁₂] [TotalComplexShape c₁₂ c₃ c₄] [K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] [HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄} (f : (i₁ : ι₁) → (i₂ : ι₂) → (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶ A)) (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc f) = f i₁ i₂ i₃ h