Functoriality of bifunctor totalizations #
Fixing a left complex needs totalizations only for that complex and the right arguments.
CategoryTheory.Functor.mapBifunctorLeft and its maps in the left variable use Mathlib's
pairwise totalization and its existing maps. When all totalizations exist, this is the left
component of Mathlib's totalized bifunctor. The totalized bifunctor preserves zero morphisms.
The identity and composition calculations were previously in
TauCeti.Algebra.Homology.Bifunctor.Homotopy; that module reuses them for homotopy equivalences.
All constructions use Joël Riou's Mathlib bifunctor totalization in
Mathlib.Algebra.Homology.Bifunctor and Mathlib.Algebra.Homology.TotalComplex.
@[simp]
theorem
HomologicalComplex.mapBifunctorMap_id
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[CategoryTheory.Category.{v_1, u_1} C₁]
[CategoryTheory.Category.{v_2, u_2} C₂]
[CategoryTheory.Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
[K₁.HasMapBifunctor K₂ F c]
:
mapBifunctorMap (CategoryTheory.CategoryStruct.id K₁) (CategoryTheory.CategoryStruct.id K₂) F c = CategoryTheory.CategoryStruct.id (K₁.mapBifunctor K₂ F c)
mapBifunctorMap sends the pair of identities to the identity.
theorem
HomologicalComplex.mapBifunctorMap_comp
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[CategoryTheory.Category.{v_1, u_1} C₁]
[CategoryTheory.Category.{v_2, u_2} C₂]
[CategoryTheory.Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K₁ L₁ M₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ M₂ : HomologicalComplex C₂ c₂}
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
[M₁.HasMapBifunctor M₂ F c]
(f₁ : K₁ ⟶ L₁)
(g₁ : L₁ ⟶ M₁)
(f₂ : K₂ ⟶ L₂)
(g₂ : L₂ ⟶ M₂)
:
mapBifunctorMap (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) F c = CategoryTheory.CategoryStruct.comp (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap g₁ g₂ F c)
mapBifunctorMap is compatible with composition in both variables simultaneously.
theorem
HomologicalComplex.mapBifunctorMap_comp_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[CategoryTheory.Category.{v_1, u_1} C₁]
[CategoryTheory.Category.{v_2, u_2} C₂]
[CategoryTheory.Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K₁ L₁ M₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ M₂ : HomologicalComplex C₂ c₂}
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
[M₁.HasMapBifunctor M₂ F c]
(f₁ : K₁ ⟶ L₁)
(g₁ : L₁ ⟶ M₁)
(f₂ : K₂ ⟶ L₂)
(g₂ : L₂ ⟶ M₂)
{Z : HomologicalComplex D c}
(h : M₁.mapBifunctor M₂ F c ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(mapBifunctorMap (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) F c) h = CategoryTheory.CategoryStruct.comp (mapBifunctorMap f₁ f₂ F c)
(CategoryTheory.CategoryStruct.comp (mapBifunctorMap g₁ g₂ F c) h)
mapBifunctorMap is compatible with composition in both variables simultaneously.
@[simp]
theorem
HomologicalComplex.mapBifunctorMap_zero_left
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[CategoryTheory.Category.{v_1, u_1} C₁]
[CategoryTheory.Category.{v_2, u_2} C₂]
[CategoryTheory.Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K L : HomologicalComplex C₁ c₁)
{N N' : HomologicalComplex C₂ c₂}
(g : N ⟶ N')
[K.HasMapBifunctor N F c]
[L.HasMapBifunctor N' F c]
:
Totalization sends a zero morphism in the left argument to zero.
@[simp]
theorem
HomologicalComplex.mapBifunctorMap_zero_right
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[CategoryTheory.Category.{v_1, u_1} C₁]
[CategoryTheory.Category.{v_2, u_2} C₂]
[CategoryTheory.Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K L : HomologicalComplex C₁ c₁}
(f : K ⟶ L)
(N N' : HomologicalComplex C₂ c₂)
[K.HasMapBifunctor N F c]
[L.HasMapBifunctor N' F c]
:
Totalization sends a zero morphism in the right argument to zero.
@[reducible, inline]
noncomputable abbrev
CategoryTheory.Functor.mapBifunctorLeft
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K : HomologicalComplex C₁ c₁)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
:
Functor (HomologicalComplex C₂ c₂) (HomologicalComplex D c)
Totalization against a fixed left complex, requiring only its own totalizations.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorLeft_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K : HomologicalComplex C₁ c₁)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
(N : HomologicalComplex C₂ c₂)
:
The object of a fixed-left totalization is the corresponding pairwise total complex.
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorLeft_map
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K : HomologicalComplex C₁ c₁)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
{N N' : HomologicalComplex C₂ c₂}
(g : N ⟶ N')
:
Maps of a fixed-left totalization use the identity on the left complex.
instance
CategoryTheory.Functor.mapBifunctorLeft_preservesZeroMorphisms
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K : HomologicalComplex C₁ c₁)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
:
(F.mapBifunctorLeft c₂ c K).PreservesZeroMorphisms
The fixed-left totalization preserves zero morphisms in its right argument.
noncomputable def
CategoryTheory.Functor.mapBifunctorLeftMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K L : HomologicalComplex C₁ c₁}
(f : K ⟶ L)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), L.HasMapBifunctor N F c]
:
A map of the chosen left complexes induces a natural map of their totalizations.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorLeftMap_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K L : HomologicalComplex C₁ c₁}
(f : K ⟶ L)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), L.HasMapBifunctor N F c]
(N : HomologicalComplex C₂ c₂)
:
(F.mapBifunctorLeftMap c₂ c f).app N = HomologicalComplex.mapBifunctorMap f (CategoryStruct.id N) F c
The component of a map between fixed-left totalizations is the pairwise totalization map.
theorem
CategoryTheory.Functor.mapBifunctorLeftMap_comp
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K L M : HomologicalComplex C₁ c₁}
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), L.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), M.HasMapBifunctor N F c]
(f : K ⟶ L)
(g : L ⟶ M)
:
F.mapBifunctorLeftMap c₂ c (CategoryStruct.comp f g) = CategoryStruct.comp (F.mapBifunctorLeftMap c₂ c f) (F.mapBifunctorLeftMap c₂ c g)
Maps between fixed-left totalizations preserve composition in the left argument.
theorem
CategoryTheory.Functor.mapBifunctorLeftMap_comp_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
{K L M : HomologicalComplex C₁ c₁}
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), L.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), M.HasMapBifunctor N F c]
(f : K ⟶ L)
(g : L ⟶ M)
{Z : Functor (HomologicalComplex C₂ c₂) (HomologicalComplex D c)}
(h : F.mapBifunctorLeft c₂ c M ⟶ Z)
:
CategoryStruct.comp (F.mapBifunctorLeftMap c₂ c (CategoryStruct.comp f g)) h = CategoryStruct.comp (F.mapBifunctorLeftMap c₂ c f) (CategoryStruct.comp (F.mapBifunctorLeftMap c₂ c g) h)
Maps between fixed-left totalizations preserve composition in the left argument.
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorLeftMap_zero
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
(K L : HomologicalComplex C₁ c₁)
[∀ (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
[∀ (N : HomologicalComplex C₂ c₂), L.HasMapBifunctor N F c]
:
A zero left map induces the zero natural transformation.
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorLeft_eq_map₂HomologicalComplex_obj
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K : HomologicalComplex C₁ c₁) (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
(K : HomologicalComplex C₁ c₁)
:
The fixed-left construction agrees with the corresponding component of the full bifunctor.
instance
CategoryTheory.Functor.map₂HomologicalComplex_preservesZeroMorphisms
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
[Category.{v_1, u_1} C₁]
[Category.{v_2, u_2} C₂]
[Category.{v_3, u_3} D]
{c₁ : ComplexShape I₁}
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Preadditive D]
(F : Functor C₁ (Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X : C₁), (F.obj X).PreservesZeroMorphisms]
(c₂ : ComplexShape I₂)
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[∀ (K : HomologicalComplex C₁ c₁) (N : HomologicalComplex C₂ c₂), K.HasMapBifunctor N F c]
:
(F.map₂HomologicalComplex c₁ c₂ c).PreservesZeroMorphisms
The full totalized bifunctor preserves zero morphisms in its left argument.
In particular this supplies zero preservation for F.map₂CochainComplex.