Naturality of the totalized bifunctor associator #
The associator HomologicalComplex.mapBifunctorAssociator on totalized triple complexes is
natural in all three inputs. This comparison is needed to identify composition of the totalized
tensor functors in the graded bimodule action.
On the way, mapBifunctor₁₂.ι_mapBifunctorMap and mapBifunctor₂₃.ι_mapBifunctorMap compute
the maps of totalized triple complexes induced by three morphisms of complexes on each summand.
This extends Joël Riou's construction in Mathlib.Algebra.Homology.BifunctorAssociator,
using HomologicalComplex.mapBifunctorAssociator and its summand-inclusion equations.
@[simp]
theorem
TauCeti.HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctorMap
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(c₁₂ : ComplexShape ι₁₂)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
(p : ι₁)
(q : ι₂)
(r : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (p, q, r) = j)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ p q r j h)
((HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄).f j) = CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (f₁.f p)).app (K₂.X q))).app (K₃.X r))
(CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (L₁.X p)).map (f₂.f q))).app (K₃.X r))
(CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (L₁.X p)).obj (L₂.X q))).map (f₃.f r))
(HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G L₁ L₂ L₃ c₁₂ c₄ p q r j h)))
The map on totalized triple complexes induced by f₁, f₂ and f₃, restricted to the
summand of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ indexed by (p, q, r).
@[simp]
theorem
TauCeti.HomologicalComplex.mapBifunctor₁₂.ι_mapBifunctorMap_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(c₁₂ : ComplexShape ι₁₂)
(c₄ : ComplexShape ι₄)
[TotalComplexShape c₁ c₂ c₁₂]
[TotalComplexShape c₁₂ c₃ c₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
(p : ι₁)
(q : ι₂)
(r : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (p, q, r) = j)
{Z : C₄}
(h✝ : ((L₁.mapBifunctor L₂ F₁₂ c₁₂).mapBifunctor L₃ G c₄).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ p q r j h)
(CategoryTheory.CategoryStruct.comp
((HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄).f j) h✝) = CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.map (f₁.f p)).app (K₂.X q))).app (K₃.X r))
(CategoryTheory.CategoryStruct.comp ((G.map ((F₁₂.obj (L₁.X p)).map (f₂.f q))).app (K₃.X r))
(CategoryTheory.CategoryStruct.comp ((G.obj ((F₁₂.obj (L₁.X p)).obj (L₂.X q))).map (f₃.f r))
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G L₁ L₂ L₃ c₁₂ c₄ p q r j h) h✝)))
The map on totalized triple complexes induced by f₁, f₂ and f₃, restricted to the
summand of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ indexed by (p, q, r).
@[simp]
theorem
TauCeti.HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctorMap
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
(p : ι₁)
(q : ι₂)
(r : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (p, q, r) = j)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ p q r j h)
((HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄).f j) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f p)).app ((G₂₃.obj (K₂.X q)).obj (K₃.X r)))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X p)).map ((G₂₃.map (f₂.f q)).app (K₃.X r)))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X p)).map ((G₂₃.obj (L₂.X q)).map (f₃.f r)))
(HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄ p q r j h)))
The map on totalized triple complexes induced by f₁, f₂ and f₃, restricted to the
summand of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄ indexed by (p, q, r).
@[simp]
theorem
TauCeti.HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctorMap_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
(p : ι₁)
(q : ι₂)
(r : ι₃)
(j : ι₄)
(h : c₁.r c₂ c₃ c₁₂ c₄ (p, q, r) = j)
{Z : C₄}
(h✝ : (L₁.mapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄).X j ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ p q r j h)
(CategoryTheory.CategoryStruct.comp
((HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄).f j) h✝) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f p)).app ((G₂₃.obj (K₂.X q)).obj (K₃.X r)))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X p)).map ((G₂₃.map (f₂.f q)).app (K₃.X r)))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X p)).map ((G₂₃.obj (L₂.X q)).map (f₃.f r)))
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄ p q r j h)
h✝)))
The map on totalized triple complexes induced by f₁, f₂ and f₃, restricted to the
summand of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄ indexed by (p, q, r).
theorem
TauCeti.HomologicalComplex.mapBifunctorAssociator_naturality
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G L₁ L₂ L₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄)
(HomologicalComplex.mapBifunctorAssociator associator L₁ L₂ L₃ c₁₂ c₂₃ c₄).hom = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).hom
(HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄)
The totalized associator is natural in all three complexes.
theorem
TauCeti.HomologicalComplex.mapBifunctorAssociator_naturality_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G L₁ L₂ L₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
{Z : HomologicalComplex C₄ c₄}
(h : L₁.mapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator L₁ L₂ L₃ c₁₂ c₂₃ c₄).hom
h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).hom
(CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄) h)
The totalized associator is natural in all three complexes.
theorem
TauCeti.HomologicalComplex.mapBifunctorAssociator_inv_naturality
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G L₁ L₂ L₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄)
(HomologicalComplex.mapBifunctorAssociator associator L₁ L₂ L₃ c₁₂ c₂₃ c₄).inv = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).inv
(HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄)
The inverse totalized associator is natural in all three complexes.
theorem
TauCeti.HomologicalComplex.mapBifunctorAssociator_inv_naturality_assoc
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₁₂ : Type u₁₂}
{C₂₃ : Type u₂₃}
{C₄ : Type u₄}
[CategoryTheory.Category.{v₁, u₁} C₁]
[CategoryTheory.Category.{v₂, u₂} C₂]
[CategoryTheory.Category.{v₃, u₃} C₃]
[CategoryTheory.Category.{v₁₂, u₁₂} C₁₂]
[CategoryTheory.Category.{v₂₃, u₂₃} C₂₃]
[CategoryTheory.Category.{v₄, u₄} 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_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
{ι₁₂ : Type u_4}
{ι₂₃ : Type u_5}
{ι₄ : Type u_6}
[DecidableEq ι₁₂]
[DecidableEq ι₂₃]
[DecidableEq ι₄]
{c₁ : ComplexShape ι₁}
{c₂ : ComplexShape ι₂}
{c₃ : ComplexShape ι₃}
(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₄]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
{K₃ L₃ : HomologicalComplex C₃ c₃}
[K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[L₁.HasMapBifunctor L₂ F₁₂ c₁₂]
[K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[L₂.HasMapBifunctor L₃ G₂₃ c₂₃]
[(K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
[(L₁.mapBifunctor L₂ F₁₂ c₁₂).HasMapBifunctor L₃ G c₄]
[K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
[L₁.HasMapBifunctor (L₂.mapBifunctor L₃ G₂₃ c₂₃) F c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G L₁ L₂ L₃ c₁₂ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
[HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ L₁ L₂ L₃ c₁₂ c₂₃ c₄]
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(f₃ : K₃ ⟶ L₃)
{Z : HomologicalComplex C₄ c₄}
(h : (L₁.mapBifunctor L₂ F₁₂ c₁₂).mapBifunctor L₃ G c₄ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap f₁ (HomologicalComplex.mapBifunctorMap f₂ f₃ G₂₃ c₂₃) F c₄)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator L₁ L₂ L₃ c₁₂ c₂₃ c₄).inv
h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).inv
(CategoryTheory.CategoryStruct.comp
(HomologicalComplex.mapBifunctorMap (HomologicalComplex.mapBifunctorMap f₁ f₂ F₁₂ c₁₂) f₃ G c₄) h)
The inverse totalized associator is natural in all three complexes.