Bifunctors on homotopy categories #
Let F : C₁ ⥤ C₂ ⥤ D be a bifunctor which is additive in each variable. Mathlib's
CategoryTheory.Functor.map₂HomologicalComplex sends complexes K₁ and K₂ to the total
complex mapBifunctor K₁ K₂ F c, and HomologicalComplex.mapBifunctorMapHomotopy₁ and
HomologicalComplex.mapBifunctorMapHomotopy₂ show that mapBifunctorMap f₁ f₂ F c only depends
on the homotopy classes of f₁ and f₂. Hence the totalized bifunctor descends to a bifunctor
F.map₂HomotopyCategory c₁ c₂ c : K(C₁) ⥤ K(C₂) ⥤ K(D)
on homotopy categories, which agrees with the totalized bifunctor on the images of complexes. In particular a homotopy equivalence in either variable becomes an isomorphism.
If F.obj X ≅ 𝟭 D for an object X of C₁, then the left unitor
CategoryTheory.Functor.mapBifunctorLeftUnitor : mapBifunctor X[0] K F c ≅ K on complexes
descends to an isomorphism between the functor of the homotopy category given by X[0] and the
identity functor.
Similarly, an associator between two composite trifunctors induces, through Mathlib's
HomologicalComplex.mapBifunctorAssociator, an isomorphism between acting by a total complex
mapBifunctor K₁ K₂ F₁₂ c₁₂ and acting by K₂ and then by K₁.
These constructions turn a complex of bimodules into an endofunctor of the homotopy category of modules: this is how complexes of bimodules, such as the braid complexes of a zigzag algebra, act on homotopy categories.
Main definitions #
CategoryTheory.Functor.map₂HomotopyCategory: the bifunctor on homotopy categories induced by a bifunctorF.CategoryTheory.Functor.map₂HomotopyCategoryLeftUnitor: the descent of the left unitorCategoryTheory.Functor.mapBifunctorLeftUnitor, an isomorphism between(F.map₂HomotopyCategory c c c).obj X[0]and the identity functor ofK(D).CategoryTheory.Functor.map₂HomotopyCategoryAssociator: the descent of the totalized associator to homotopy categories.
noncomputable def
CategoryTheory.Functor.map₂HomotopyCategory
{C₁ : Type u₁}
{C₂ : Type u₂}
{D : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
{I₁ : Type u_1}
{I₂ : Type u_2}
{J : Type u_3}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
:
Functor (HomotopyCategory C₁ c₁) (Functor (HomotopyCategory C₂ c₂) (HomotopyCategory D c))
The bifunctor on homotopy categories induced by a bifunctor F which is additive in each
variable. On the images of complexes K₁ and K₂ it is the total complex
mapBifunctor K₁ K₂ F c.
Instances For
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategory_obj_obj
{C₁ : Type u₁}
{C₂ : Type u₂}
{D : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
{I₁ : Type u_1}
{I₂ : Type u_2}
{J : Type u_3}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
:
((F.map₂HomotopyCategory c₁ c₂ c).obj ((HomotopyCategory.quotient C₁ c₁).obj K₁)).obj
((HomotopyCategory.quotient C₂ c₂).obj K₂) = (HomotopyCategory.quotient D c).obj (K₁.mapBifunctor K₂ F c)
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategory_obj_map
{C₁ : Type u₁}
{C₂ : Type u₂}
{D : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
{I₁ : Type u_1}
{I₂ : Type u_2}
{J : Type u_3}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
(K₁ : HomologicalComplex C₁ c₁)
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
:
((F.map₂HomotopyCategory c₁ c₂ c).obj ((HomotopyCategory.quotient C₁ c₁).obj K₁)).map
((HomotopyCategory.quotient C₂ c₂).map f₂) = (HomotopyCategory.quotient D c).map (HomologicalComplex.mapBifunctorMap (CategoryStruct.id K₁) f₂ F c)
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategory_map_app
{C₁ : Type u₁}
{C₂ : Type u₂}
{D : Type u₃}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} D]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
{I₁ : Type u_1}
{I₂ : Type u_2}
{J : Type u_3}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F c]
{K₁ L₁ : HomologicalComplex C₁ c₁}
(f₁ : K₁ ⟶ L₁)
(K₂ : HomologicalComplex C₂ c₂)
:
((F.map₂HomotopyCategory c₁ c₂ c).map ((HomotopyCategory.quotient C₁ c₁).map f₁)).app
((HomotopyCategory.quotient C₂ c₂).obj K₂) = (HomotopyCategory.quotient D c).map (HomologicalComplex.mapBifunctorMap f₁ (CategoryStruct.id K₂) F c)
noncomputable def
CategoryTheory.Functor.map₂HomotopyCategoryLeftUnitor
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
[Preadditive C]
[Limits.HasZeroObject C]
[Preadditive D]
(F : Functor C (Functor D D))
[F.Additive]
[∀ (X : C), (F.obj X).Additive]
(X : C)
(e : F.obj X ≅ Functor.id D)
{I : Type u_4}
[AddMonoid I]
[DecidableEq I]
(c : ComplexShape I)
[c.TensorSigns]
[∀ (K₁ : HomologicalComplex C c) (K₂ : HomologicalComplex D c), K₁.HasMapBifunctor K₂ F c]
:
(F.map₂HomotopyCategory c c c).obj ((HomotopyCategory.quotient C c).obj ((HomologicalComplex.single C c 0).obj X)) ≅ Functor.id (HomotopyCategory D c)
On homotopy categories, the complex X[0] acts as the identity functor when
e : F.obj X ≅ 𝟭 D.
Instances For
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategoryLeftUnitor_hom_app
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
[Preadditive C]
[Limits.HasZeroObject C]
[Preadditive D]
(F : Functor C (Functor D D))
[F.Additive]
[∀ (X : C), (F.obj X).Additive]
(X : C)
(e : F.obj X ≅ Functor.id D)
{I : Type u_4}
[AddMonoid I]
[DecidableEq I]
(c : ComplexShape I)
[c.TensorSigns]
[∀ (K₁ : HomologicalComplex C c) (K₂ : HomologicalComplex D c), K₁.HasMapBifunctor K₂ F c]
(K : HomologicalComplex D c)
:
(F.map₂HomotopyCategoryLeftUnitor X e c).hom.app ((HomotopyCategory.quotient D c).obj K) = (HomotopyCategory.quotient D c).map (F.mapBifunctorLeftUnitor X e K).hom
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategoryLeftUnitor_inv_app
{C : Type u₁}
{D : Type u₂}
[Category.{v₁, u₁} C]
[Category.{v₂, u₂} D]
[Preadditive C]
[Limits.HasZeroObject C]
[Preadditive D]
(F : Functor C (Functor D D))
[F.Additive]
[∀ (X : C), (F.obj X).Additive]
(X : C)
(e : F.obj X ≅ Functor.id D)
{I : Type u_4}
[AddMonoid I]
[DecidableEq I]
(c : ComplexShape I)
[c.TensorSigns]
[∀ (K₁ : HomologicalComplex C c) (K₂ : HomologicalComplex D c), K₁.HasMapBifunctor K₂ F c]
(K : HomologicalComplex D c)
:
(F.map₂HomotopyCategoryLeftUnitor X e c).inv.app ((HomotopyCategory.quotient D c).obj K) = (HomotopyCategory.quotient D c).map (F.mapBifunctorLeftUnitor X e K).inv
noncomputable def
CategoryTheory.Functor.map₂HomotopyCategoryAssociator
{C₁ : Type u_4}
{C₂ : Type u_5}
{C₃ : Type u_6}
{C₁₂ : Type u_7}
{C₂₃ : Type u_8}
{C₄ : Type u_9}
[Category.{v_1, u_4} C₁]
[Category.{v_2, u_5} C₂]
[Category.{v_3, u_6} C₃]
[Category.{v_4, u_7} C₁₂]
[Category.{v_5, u_8} C₂₃]
[Category.{v_6, u_9} C₄]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive C₃]
[Preadditive C₁₂]
[Preadditive C₂₃]
[Preadditive C₄]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
[F₁₂.Additive]
[∀ (X : C₁), (F₁₂.obj X).Additive]
[G.Additive]
[∀ (X : C₁₂), (G.obj X).Additive]
[F.Additive]
[∀ (X : C₁), (F.obj X).Additive]
[G₂₃.Additive]
[∀ (X : C₂), (G₂₃.obj X).Additive]
(associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃)
{ι₁ : Type u_10}
{ι₂ : Type u_11}
{ι₃ : Type u_12}
{ι₁₂ : Type u_13}
{ι₂₃ : Type u_14}
{ι₄ : Type u_15}
[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₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[∀ (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃), K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[∀ (K₁₂ : HomologicalComplex C₁₂ c₁₂) (K₃ : HomologicalComplex C₃ c₃), K₁₂.HasMapBifunctor K₃ G c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂₃ : HomologicalComplex C₂₃ c₂₃), K₁.HasMapBifunctor K₂₃ F c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
:
(G.map₂HomotopyCategory c₁₂ c₃ c₄).obj ((HomotopyCategory.quotient C₁₂ c₁₂).obj (K₁.mapBifunctor K₂ F₁₂ c₁₂)) ≅ ((G₂₃.map₂HomotopyCategory c₂ c₃ c₂₃).obj ((HomotopyCategory.quotient C₂ c₂).obj K₂)).comp
((F.map₂HomotopyCategory c₁ c₂₃ c₄).obj ((HomotopyCategory.quotient C₁ c₁).obj K₁))
On homotopy categories, acting by the total complex mapBifunctor K₁ K₂ F₁₂ c₁₂ through G
is isomorphic to acting first by K₂ through G₂₃ and then by K₁ through F, given an
associator between the two composite trifunctors. The components are the images of Mathlib's
HomologicalComplex.mapBifunctorAssociator.
Instances For
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategoryAssociator_hom_app
{C₁ : Type u_4}
{C₂ : Type u_5}
{C₃ : Type u_6}
{C₁₂ : Type u_7}
{C₂₃ : Type u_8}
{C₄ : Type u_9}
[Category.{v_1, u_4} C₁]
[Category.{v_2, u_5} C₂]
[Category.{v_3, u_6} C₃]
[Category.{v_4, u_7} C₁₂]
[Category.{v_5, u_8} C₂₃]
[Category.{v_6, u_9} C₄]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive C₃]
[Preadditive C₁₂]
[Preadditive C₂₃]
[Preadditive C₄]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
[F₁₂.Additive]
[∀ (X : C₁), (F₁₂.obj X).Additive]
[G.Additive]
[∀ (X : C₁₂), (G.obj X).Additive]
[F.Additive]
[∀ (X : C₁), (F.obj X).Additive]
[G₂₃.Additive]
[∀ (X : C₂), (G₂₃.obj X).Additive]
(associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃)
{ι₁ : Type u_10}
{ι₂ : Type u_11}
{ι₃ : Type u_12}
{ι₁₂ : Type u_13}
{ι₂₃ : Type u_14}
{ι₄ : Type u_15}
[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₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[∀ (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃), K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[∀ (K₁₂ : HomologicalComplex C₁₂ c₁₂) (K₃ : HomologicalComplex C₃ c₃), K₁₂.HasMapBifunctor K₃ G c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂₃ : HomologicalComplex C₂₃ c₂₃), K₁.HasMapBifunctor K₂₃ F c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(K₃ : HomologicalComplex C₃ c₃)
:
(map₂HomotopyCategoryAssociator associator c₁ c₂ c₃ c₁₂ c₂₃ c₄ K₁ K₂).hom.app
((HomotopyCategory.quotient C₃ c₃).obj K₃) = (HomotopyCategory.quotient C₄ c₄).map (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).hom
@[simp]
theorem
CategoryTheory.Functor.map₂HomotopyCategoryAssociator_inv_app
{C₁ : Type u_4}
{C₂ : Type u_5}
{C₃ : Type u_6}
{C₁₂ : Type u_7}
{C₂₃ : Type u_8}
{C₄ : Type u_9}
[Category.{v_1, u_4} C₁]
[Category.{v_2, u_5} C₂]
[Category.{v_3, u_6} C₃]
[Category.{v_4, u_7} C₁₂]
[Category.{v_5, u_8} C₂₃]
[Category.{v_6, u_9} C₄]
[Preadditive C₁]
[Preadditive C₂]
[Preadditive C₃]
[Preadditive C₁₂]
[Preadditive C₂₃]
[Preadditive C₄]
{F₁₂ : Functor C₁ (Functor C₂ C₁₂)}
{G : Functor C₁₂ (Functor C₃ C₄)}
{F : Functor C₁ (Functor C₂₃ C₄)}
{G₂₃ : Functor C₂ (Functor C₃ C₂₃)}
[F₁₂.Additive]
[∀ (X : C₁), (F₁₂.obj X).Additive]
[G.Additive]
[∀ (X : C₁₂), (G.obj X).Additive]
[F.Additive]
[∀ (X : C₁), (F.obj X).Additive]
[G₂₃.Additive]
[∀ (X : C₂), (G₂₃.obj X).Additive]
(associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃)
{ι₁ : Type u_10}
{ι₂ : Type u_11}
{ι₃ : Type u_12}
{ι₁₂ : Type u_13}
{ι₂₃ : Type u_14}
{ι₄ : Type u_15}
[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₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂), K₁.HasMapBifunctor K₂ F₁₂ c₁₂]
[∀ (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃), K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
[∀ (K₁₂ : HomologicalComplex C₁₂ c₁₂) (K₃ : HomologicalComplex C₃ c₃), K₁₂.HasMapBifunctor K₃ G c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂₃ : HomologicalComplex C₂₃ c₂₃), K₁.HasMapBifunctor K₂₃ F c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
[∀ (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃),
HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(K₃ : HomologicalComplex C₃ c₃)
:
(map₂HomotopyCategoryAssociator associator c₁ c₂ c₃ c₁₂ c₂₃ c₄ K₁ K₂).inv.app
((HomotopyCategory.quotient C₃ c₃).obj K₃) = (HomotopyCategory.quotient C₄ c₄).map (HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄).inv