The associator for actions of bifunctors on homological complexes #
In this file, we shall adapt 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 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.
@[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₄]
:
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₄]
:
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₁₂]
:
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}
{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₁₂]
[DecidableEq ι₁₂]
[(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₄)
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}
{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₂₃]
[DecidableEq ι₂₃]
[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₄)
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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[H₂₃ : 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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)
:
ι 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
:
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) ≠ j)
:
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
{j : ι₄}
{A : C₄}
{f 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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[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))
:
Constructor for morphisms from
(mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j.
@[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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(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.
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₁.Rel i₁ (c₁.next i₁))
:
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
{i₁ i₁' : ι₁}
(h₁ : c₁.Rel i₁ 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(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.
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₂.Rel i₂ (c₂.next i₂))
:
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
{i₂ i₂' : ι₂}
(h₂ : c₂.Rel 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(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.
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₃.Rel i₃ (c₃.next i₃))
:
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(i₁ : ι₁)
(i₂ : ι₂)
{i₃ i₃' : ι₃}
(h₃ : c₃.Rel 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[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.
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[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.
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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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'
@[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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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)
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
CategoryTheory.CategoryStruct.comp (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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)
[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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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)
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
CategoryTheory.CategoryStruct.comp (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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)
[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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h) (D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') = 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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(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 (ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (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 ι₄]
{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₁₂]
[DecidableEq ι₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
(j j' : ι₄)
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
:
((K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄).d j j' = D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' + D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j'
noncomputable def
HomologicalComplex.mapBifunctor₂₃.ι
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
:
The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ (c₁.ρ₂₃ 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_4}
{C₃ : Type u_5}
{C₄ : Type u_6}
[CategoryTheory.Category.{u_15, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(i₂₃ : ι₂₃)
(j : ι₄)
(h₂₃ : c₂.π c₃ c₂₃ (i₂, i₃) = i₂₃)
(h : c₁.π c₂₃ c₄ (i₁, i₂₃) = j)
:
ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j ⋯ = CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.ιMapBifunctor K₃ G₂₃ c₂₃ i₂ i₃ i₂₃ h₂₃))
(K₁.ιMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ i₁ i₂₃ j h)
noncomputable def
HomologicalComplex.mapBifunctor₂₃.ιOrZero
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F 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_4}
{C₃ : Type u_5}
{C₄ : Type u_6}
[CategoryTheory.Category.{u_15, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
:
theorem
HomologicalComplex.mapBifunctor₂₃.ιOrZero_eq_zero
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) ≠ j)
:
theorem
HomologicalComplex.mapBifunctor₂₃.hom_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₂₃ : Type u_4}
{C₃ : Type u_5}
{C₄ : Type u_6}
[CategoryTheory.Category.{u_14, 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_15, 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_10}
{ι₂₃ : 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 ι₂₃}
{c₄ : ComplexShape ι₄}
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{j : ι₄}
{A : C₄}
{f g : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ A}
(hfg :
∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) f = CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) g)
:
noncomputable def
HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃}
{c₄ : ComplexShape ι₄}
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{j : ι₄}
{A : C₄}
(f :
(i₁ : ι₁) →
(i₂ : ι₂) →
(i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶ A))
:
Constructor for morphisms from
(mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j.
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃}
{c₄ : ComplexShape ι₄}
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{j : ι₄}
{A : C₄}
(f :
(i₁ : ι₁) →
(i₂ : ι₂) →
(i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((F.obj (K₁.X i₁)).obj ((G₂₃.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 (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (mapBifunctor₂₃Desc c₁₂ f) = f i₁ i₂ i₃ h
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc_assoc
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃}
{c₄ : ComplexShape ι₄}
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{j : ι₄}
{A : C₄}
(f :
(i₁ : ι₁) →
(i₂ : ι₂) →
(i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((F.obj (K₁.X i₁)).obj ((G₂₃.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 (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃Desc c₁₂ 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_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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
The first differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- One or more equations did not get rendered due to their size.
theorem
HomologicalComplex.mapBifunctor₂₃.d₁_eq_zero
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₁.Rel i₁ (c₁.next i₁))
:
theorem
HomologicalComplex.mapBifunctor₂₃.d₁_eq
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
{i₁ i₁' : ι₁}
(h₁ : c₁.Rel i₁ i₁')
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
noncomputable def
HomologicalComplex.mapBifunctor₂₃.d₂
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
The second differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- One or more equations did not get rendered due to their size.
theorem
HomologicalComplex.mapBifunctor₂₃.d₂_eq_zero
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₂.Rel i₂ (c₂.next i₂))
:
theorem
HomologicalComplex.mapBifunctor₂₃.d₂_eq
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
{i₂ i₂' : ι₂}
(h₂ : c₂.Rel i₂ i₂')
(i₃ : ι₃)
(j : ι₄)
:
noncomputable def
HomologicalComplex.mapBifunctor₂₃.d₃
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
The third differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- One or more equations did not get rendered due to their size.
theorem
HomologicalComplex.mapBifunctor₂₃.d₃_eq_zero
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : ¬c₃.Rel i₃ (c₃.next i₃))
:
theorem
HomologicalComplex.mapBifunctor₂₃.d₃_eq
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
{i₃ i₃' : ι₃}
(h₃ : c₃.Rel i₃ i₃')
(j : ι₄)
:
noncomputable def
HomologicalComplex.mapBifunctor₂₃.D₁
{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₃]
[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₂₃]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(j j' : ι₄)
:
(K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'
The first differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' = HomologicalComplex.mapBifunctor.D₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ j j'
noncomputable def
HomologicalComplex.mapBifunctor₂₃.D₂
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(j j' : ι₄)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
:
(K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'
The second differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
HomologicalComplex.mapBifunctor₂₃.D₃
{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₃]
[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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(j j' : ι₄)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
:
(K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j'
The third differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₁
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') = d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₁_assoc
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₂
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₂_assoc
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{Z : C₄}
(h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₃
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) (D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor₂₃.ι_D₃_assoc
{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_17, u_2} C₂]
[CategoryTheory.Category.{u_16, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j j' : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
{Z : C₄}
(h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h✝) = CategoryTheory.CategoryStruct.comp (d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j') h✝
theorem
HomologicalComplex.mapBifunctor₂₃.d_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{C₂₃ : Type u_4}
{C₃ : Type u_5}
{C₄ : Type u_6}
[CategoryTheory.Category.{u_14, 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_15, 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_10}
{ι₂₃ : 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 ι₂₃)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
[TotalComplexShape c₂ c₃ c₂₃]
[TotalComplexShape c₁ c₂₃ c₄]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
:
(K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).d j j' = D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' + D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' + D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j'
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorAssociatorX_hom
{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_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.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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
:
CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃))
(mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h)
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorAssociatorX_hom_assoc
{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_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.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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j)
{Z : C₄}
(h✝ : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h)
(CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom h✝) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃))
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h) h✝)
@[simp]
theorem
HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom
{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_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.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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
:
CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j)
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃))
(mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j)
@[simp]
theorem
HomologicalComplex.ιOrZero_mapBifunctorAssociatorX_hom_assoc
{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_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.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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(i₁ : ι₁)
(i₂ : ι₂)
(i₃ : ι₃)
(j : ι₄)
{Z : C₄}
(h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j)
(CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom h) = CategoryTheory.CategoryStruct.comp (((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃))
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j) h)
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₁
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₁_assoc
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
{Z : C₄}
(h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₂
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
{Z : C₄}
(h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₃
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom
theorem
HomologicalComplex.mapBifunctorAssociatorX_hom_D₃_assoc
{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_16, u_1} C₁]
[CategoryTheory.Category.{u_17, u_2} C₂]
[CategoryTheory.Category.{u_15, u_5} C₃]
[CategoryTheory.Category.{u_13, u_6} C₄]
[CategoryTheory.Category.{u_14, 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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(j j' : ι₄)
{Z : C₄}
(h : (K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom
(CategoryTheory.CategoryStruct.comp (mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j') h) = CategoryTheory.CategoryStruct.comp (mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j')
(CategoryTheory.CategoryStruct.comp (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom h)
noncomputable def
HomologicalComplex.mapBifunctorAssociator
{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 ι₄]
{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₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄]
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
:
(K₁.mapBifunctor K₂ F₁₂ c₁₂).mapBifunctor K₃ G c₄ ≅ K₁.mapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
The associator isomorphism for the action of bifunctors on homological complexes.
Equations
- HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ = HomologicalComplex.Hom.isoOfComponents (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄) ⋯