The action of a bifunctor on homological complexes #
Given a bifunctor F : C₁ ⥤ C₂ ⥤ D and complexes shapes c₁ : ComplexShape I₁ and
c₂ : ComplexShape I₂, we define a bifunctor mapBifunctorHomologicalComplex F c₁ c₂
of type HomologicalComplex C₁ c₁ ⥤ HomologicalComplex C₂ c₂ ⥤ HomologicalComplex₂ D c₁ c₂.
Then, when K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂ and
c : ComplexShape J are such that we have TotalComplexShape c₁ c₂ c, we introduce
a typeclass HasMapBifunctor K₁ K₂ F c which allows to define
mapBifunctor K₁ K₂ F c : HomologicalComplex D c as the total complex of the
bicomplex (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).
def
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
:
Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂)
Auxiliary definition for mapBifunctorHomologicalComplex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ i₂' : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
{K₂ K₂' : HomologicalComplex C₂ c₂}
{φ : K₂ ⟶ K₂'}
(i₁ : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ i₁' : I₁)
(i₂ : I₂)
:
def
CategoryTheory.Functor.mapBifunctorHomologicalComplex
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
:
Functor (HomologicalComplex C₁ c₁) (Functor (HomologicalComplex C₂ c₂) (HomologicalComplex₂ D c₁ c₂))
Given a functor F : C₁ ⥤ C₂ ⥤ D, this is the bifunctor which sends
K₁ : HomologicalComplex C₁ c₁ and K₂ : HomologicalComplex C₂ c₂ to the bicomplex
which is degree (i₁, i₂) consists of (F.obj (K₁.X i₁)).obj (K₂.X i₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ i₂' : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
{K₂ K₂' : HomologicalComplex C₂ c₂}
{φ : K₂ ⟶ K₂'}
(i₁ : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ i₁' : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
(c₁ : ComplexShape I₁)
(c₂ : ComplexShape I₂)
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{K₁ K₁' : HomologicalComplex C₁ c₁}
(f : K₁ ⟶ K₁')
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ : I₂)
:
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} D]
[Limits.HasZeroMorphisms C₁]
[Limits.HasZeroMorphisms C₂]
[Limits.HasZeroMorphisms D]
(F : Functor C₁ (Functor C₂ D))
{I₁ : Type u_4}
{I₂ : Type u_5}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
:
(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).toGradedObject = ((GradedObject.mapBifunctor F I₁ I₂).obj K₁.X).obj K₂.X
@[reducible, inline]
abbrev
HomologicalComplex.HasMapBifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
:
The condition that ((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂ has
a total complex.
Equations
- K₁.HasMapBifunctor K₂ F c = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).HasTotal c
Instances For
@[reducible, inline]
noncomputable abbrev
HomologicalComplex.mapBifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
:
Given K₁ : HomologicalComplex C₁ c₁, K₂ : HomologicalComplex C₂ c₂,
a bifunctor F : C₁ ⥤ C₂ ⥤ D and a complex shape ComplexShape J such that we have
[TotalComplexShape c₁ c₂ c], this mapBifunctor K₁ K₂ F c : HomologicalComplex D c
is the total complex of the bicomplex obtained by applying F to K₁ and K₂.
Equations
- K₁.mapBifunctor K₂ F c = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).total c
Instances For
@[reducible, inline]
noncomputable abbrev
HomologicalComplex.ιMapBifunctor
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
The inclusion of a summand of (mapBifunctor K₁ K₂ F c).X j.
Equations
- K₁.ιMapBifunctor K₂ F c i₁ i₂ j h = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁ i₂ j h
Instances For
@[reducible, inline]
noncomputable abbrev
HomologicalComplex.ιMapBifunctorOrZero
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
:
The inclusion of a summand of (mapBifunctor K₁ K₂ F c).X j, or zero.
Equations
- K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotalOrZero c i₁ i₂ j
Instances For
theorem
HomologicalComplex.ιMapBifunctorOrZero_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
theorem
HomologicalComplex.ιMapBifunctorOrZero_eq_zero
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) ≠ j)
:
noncomputable def
HomologicalComplex.mapBifunctorDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{c : ComplexShape J}
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{A : D}
{j : J}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A))
:
Constructor for morphisms from (mapBifunctor K₁ K₂ F c).X j.
Equations
- HomologicalComplex.mapBifunctorDesc f = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).totalDesc f
Instances For
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorDesc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{c : ComplexShape J}
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{A : D}
{j : J}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (mapBifunctorDesc f) = f i₁ i₂ h
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorDesc_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{c : ComplexShape J}
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{A : D}
{j : J}
(f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c (i₁, i₂) = j → ((F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ A))
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
{Z : D}
(h✝ : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
(CategoryTheory.CategoryStruct.comp (mapBifunctorDesc f) h✝) = CategoryTheory.CategoryStruct.comp (f i₁ i₂ h) h✝
theorem
HomologicalComplex.mapBifunctor.hom_ext
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{c : ComplexShape J}
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{Y : D}
{j : J}
{f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f = CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g)
:
theorem
HomologicalComplex.mapBifunctor.hom_ext_iff
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
{c : ComplexShape J}
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{Y : D}
{j : J}
{f g : (K₁.mapBifunctor K₂ F c).X j ⟶ Y}
:
f = g ↔ ∀ (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c (i₁, i₂) = j),
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) f = CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) g
noncomputable def
HomologicalComplex.mapBifunctor.D₁
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
:
The first differential on mapBifunctor K₁ K₂ F c
Equations
- HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j' = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).D₁ c j j'
Instances For
noncomputable def
HomologicalComplex.mapBifunctor.D₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
:
The second differential on mapBifunctor K₁ K₂ F c
Equations
- HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j' = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).D₂ c j j'
Instances For
theorem
HomologicalComplex.mapBifunctor.d_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
:
noncomputable def
HomologicalComplex.mapBifunctor.d₁
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
:
The first differential on a summand of mapBifunctor K₁ K₂ F c
Equations
- HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₁ c i₁ i₂ j
Instances For
noncomputable def
HomologicalComplex.mapBifunctor.d₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
:
The second differential on a summand of mapBifunctor K₁ K₂ F c
Equations
- HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ j
Instances For
theorem
HomologicalComplex.mapBifunctor.d₁_eq_zero
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : ¬c₁.Rel i₁ (c₁.next i₁))
:
theorem
HomologicalComplex.mapBifunctor.d₂_eq_zero
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : ¬c₂.Rel i₂ (c₂.next i₂))
:
theorem
HomologicalComplex.mapBifunctor.d₁_eq_zero'
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
(h' : c₁.π c₂ c (i₁', i₂) ≠ j)
:
theorem
HomologicalComplex.mapBifunctor.d₂_eq_zero'
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
(h' : c₁.π c₂ c (i₁, i₂') ≠ j)
:
theorem
HomologicalComplex.mapBifunctor.d₁_eq'
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
:
theorem
HomologicalComplex.mapBifunctor.d₂_eq'
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
:
theorem
HomologicalComplex.mapBifunctor.d₁_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
{i₁ i₁' : I₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
(h' : c₁.π c₂ c (i₁', i₂) = j)
:
theorem
HomologicalComplex.mapBifunctor.d₂_eq
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(i₁ : I₁)
{i₂ i₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
(h' : c₁.π c₂ c (i₁, i₂') = j)
:
@[simp]
theorem
HomologicalComplex.mapBifunctor.ι_D₁
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (D₁ K₁ K₂ F c j j') = d₁ K₁ K₂ F c i₁ i₂ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor.ι_D₁_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
{Z : D}
(h✝ : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
(CategoryTheory.CategoryStruct.comp (D₁ K₁ K₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (d₁ K₁ K₂ F c i₁ i₂ j') h✝
@[simp]
theorem
HomologicalComplex.mapBifunctor.ι_D₂
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) (D₂ K₁ K₂ F c j j') = d₂ K₁ K₂ F c i₁ i₂ j'
@[simp]
theorem
HomologicalComplex.mapBifunctor.ι_D₂_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
(K₁ : HomologicalComplex C₁ c₁)
(K₂ : HomologicalComplex C₂ c₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[DecidableEq J]
(j j' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
{Z : D}
(h✝ : (K₁.mapBifunctor K₂ F c).X j' ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
(CategoryTheory.CategoryStruct.comp (D₂ K₁ K₂ F c j j') h✝) = CategoryTheory.CategoryStruct.comp (d₂ K₁ K₂ F c i₁ i₂ j') h✝
noncomputable def
HomologicalComplex.mapBifunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
[DecidableEq J]
:
The morphism mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c induced by
morphisms of complexes K₁ ⟶ L₁ and K₂ ⟶ L₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorMap
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h) ((mapBifunctorMap f₁ f₂ F c).f j) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h))
@[simp]
theorem
HomologicalComplex.ι_mapBifunctorMap_assoc
{C₁ : Type u_1}
{C₂ : Type u_2}
{D : Type u_3}
[CategoryTheory.Category.{u_9, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_7, u_3} D]
{I₁ : Type u_4}
{I₂ : Type u_5}
{J : Type u_6}
{c₁ : ComplexShape I₁}
{c₂ : ComplexShape I₂}
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Preadditive D]
{K₁ L₁ : HomologicalComplex C₁ c₁}
{K₂ L₂ : HomologicalComplex C₂ c₂}
(f₁ : K₁ ⟶ L₁)
(f₂ : K₂ ⟶ L₂)
(F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
[F.PreservesZeroMorphisms]
[∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms]
(c : ComplexShape J)
[TotalComplexShape c₁ c₂ c]
[K₁.HasMapBifunctor K₂ F c]
[L₁.HasMapBifunctor L₂ F c]
[DecidableEq J]
(i₁ : I₁)
(i₂ : I₂)
(j : J)
(h : c₁.π c₂ c (i₁, i₂) = j)
{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 ((mapBifunctorMap f₁ f₂ F c).f j) h✝) = CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂))
(CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂))
(CategoryTheory.CategoryStruct.comp (L₁.ιMapBifunctor L₂ F c i₁ i₂ j h) h✝))