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
Instances For
@[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
Instances For
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.
Instances For
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
Instances For
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.
Instances For
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
{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
Instances For
@[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
@[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
noncomputable def
HomologicalComplex.mapBifunctor₁₂.d₁
{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 first differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex.mapBifunctor₁₂.d₁_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₁.Rel i₁ (c₁.next i₁))
:
HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
theorem
HomologicalComplex.mapBifunctor₁₂.d₁_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₁' : ι₁}
(h₁ : c₁.Rel i₁ i₁')
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) • CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (K₁.d i₁ i₁')).app (K₂.X i₂))).app (K₃.X i₃))
(HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁' i₂ i₃ j)
noncomputable def
HomologicalComplex.mapBifunctor₁₂.d₂
{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 second differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex.mapBifunctor₁₂.d₂_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₂.Rel i₂ (c₂.next i₂))
:
HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
theorem
HomologicalComplex.mapBifunctor₁₂.d₂_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₂' : ι₂}
(h₂ : c₂.Rel i₂ i₂')
(i₃ : ι₃)
(j : ι₄)
:
HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = (c₁₂.ε₁ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) • CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (K₁.X i₁)).map (K₂.d i₂ i₂'))).app (K₃.X i₃))
(HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂' i₃ j)
noncomputable def
HomologicalComplex.mapBifunctor₁₂.d₃
{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 third differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex.mapBifunctor₁₂.d₃_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₃.Rel i₃ (c₃.next i₃))
:
HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0
theorem
HomologicalComplex.mapBifunctor₁₂.d₃_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₃' : ι₃}
(h₃ : c₃.Rel i₃ i₃')
(j : ι₄)
:
HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = c₁₂.ε₂ c₃ c₄ (c₁.π c₂ c₁₂ (i₁, i₂), i₃) • CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).map (K₃.d i₃ i₃'))
(HomologicalComplex.mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃' j)
noncomputable def
HomologicalComplex.mapBifunctor₁₂.D₁
{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 : ι₄)
(j' : ι₄)
:
((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'
The first differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HomologicalComplex.mapBifunctor₁₂.D₂
{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 : ι₄)
(j' : ι₄)
:
((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'
The second differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
HomologicalComplex.mapBifunctor₁₂.D₃
{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₄]
(j : ι₄)
(j' : ι₄)
:
((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j ⟶ ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j'
The third differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄.
Equations
- HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = HomologicalComplex.mapBifunctor.D₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ j j'
Instances For
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₁
{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 : ι₄)
(j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₁_assoc
{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 : ι₄)
(j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
{Z : C₄}
(h : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₂
{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 : ι₄)
(j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₂_assoc
{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 : ι₄)
(j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
{Z : C₄}
(h : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₃
{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 : ι₄)
(j' : ι₄)
(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₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₁₂.ι_D₃_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₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
{Z : C₄}
(h : ((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h✝)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j') h
theorem
HomologicalComplex.mapBifunctor₁₂.d_eq
{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₄]
(j : ι₄)
(j' : ι₄)
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).d j j' = HomologicalComplex.mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'