The action of a bifunctor on homological complexes factors through homotopies #
Given a TotalComplexShape c₁ c₂ c, a functor F : C₁ ⥤ C₂ ⥤ D,
we shall show in this file that up to homotopy the morphism
mapBifunctorMap f₁ f₂ F c only depends on the homotopy classes of
the morphism f₁ in HomologicalComplex C c₁ and of
the morphism f₂ in HomologicalComplex C c₂ (TODO).
noncomputable def
HomologicalComplex.mapBifunctorMapHomotopy.hom₁
{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.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
(j j' : J)
:
(K₁.mapBifunctor K₂ F c).X j ⟶ (L₁.mapBifunctor L₂ F c).X j'
Auxiliary definition for mapBifunctorMapHomotopy₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁
{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.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
(i₁ i₁' : I₁)
(i₂ : I₂)
(j j' : J)
(h : c₁.π c₂ c (i₁', i₂) = j)
(h' : c₁.prev i₁' = i₁)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h)
(HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))
theorem
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_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.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
(i₁ i₁' : I₁)
(i₂ : I₂)
(j j' : J)
(h : c₁.π c₂ c (i₁', i₂) = j)
(h' : c₁.prev i₁' = i₁)
{Z : D}
(h✝ : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp
(c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')))
h✝
theorem
HomologicalComplex.mapBifunctorMapHomotopy.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}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
(j j' : J)
(h : ¬c.Rel j' j)
:
HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j' = 0
theorem
HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux
{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.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
{i₁ i₁' : I₁}
(hi₁ : c₁.Rel i₁ i₁')
{i₂ i₂' : I₂}
(hi₂ : c₂.Rel i₂ i₂')
(j : J)
(hj : c₁.π c₂ c (i₁', i₂) = j)
:
c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) = -CategoryTheory.CategoryStruct.comp
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j))
(HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j)
theorem
HomologicalComplex.mapBifunctorMapHomotopy.comm₁
{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.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
(j : J)
:
(HomologicalComplex.mapBifunctorMap f₁ f₂ F c).f j = CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctor K₂ F c).d j (c.next j))
(HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j (c.prev j))
((L₁.mapBifunctor L₂ F c).d (c.prev j) j) + (HomologicalComplex.mapBifunctorMap f₁' f₂ F c).f j
noncomputable def
HomologicalComplex.mapBifunctorMapHomotopy₁
{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.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
[CategoryTheory.Preadditive C₁]
[CategoryTheory.Preadditive C₂]
[CategoryTheory.Preadditive D]
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
{K₁ L₁ : HomologicalComplex C₁ c₁}
{f₁ f₁' : K₁ ⟶ L₁}
(h₁ : Homotopy f₁ f₁')
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.Additive]
[∀ (X₁ : C₁), (F.obj X₁).Additive]
(c : ComplexShape J)
[DecidableEq J]
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
:
Homotopy (HomologicalComplex.mapBifunctorMap f₁ f₂ F c) (HomologicalComplex.mapBifunctorMap f₁' f₂ F c)
The homotopy between mapBifunctorMap f₁ f₂ F c and mapBifunctorMap f₁' f₂ F c that
is induced by an homotopy between f₁ and f₁'.
Equations
- HomologicalComplex.mapBifunctorMapHomotopy₁ h₁ f₂ F c = { hom := HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c, zero := ⋯, comm := ⋯ }