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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_3} D]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₁)
:
CategoryTheory.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_map_f_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂}
{K₂' : HomologicalComplex C₂ c₂}
{φ : K₂ ⟶ K₂'}
(i₁ : I₁)
(i₂ : I₂)
:
(((F.mapBifunctorHomologicalComplexObj c₂ K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂)
:
(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂ : I₂)
:
(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂' : I₂)
:
(((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
def
CategoryTheory.Functor.mapBifunctorHomologicalComplex
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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]
:
CategoryTheory.Functor (HomologicalComplex C₁ c₁)
(CategoryTheory.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_d_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂ : I₂)
:
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d i₁ i₁').f i₂ = (F.map (K₁.d i₁ i₁')).app (K₂.X i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂)
:
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).X i₂ = (F.obj (K₁.X i₁)).obj (K₂.X i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂}
{K₂' : HomologicalComplex C₂ c₂}
{φ : K₂ ⟶ K₂'}
(i₁ : I₁)
(i₂ : I₂)
:
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).map φ).f i₁).f i₂ = (F.obj (K₁.X i₁)).map (φ.f i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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₂' : I₂)
:
((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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 : K₁ ⟶ K₁')
(K₂ : HomologicalComplex C₂ c₂)
(i₁ : I₁)
(i₂ : I₂)
:
((((F.mapBifunctorHomologicalComplex c₁ c₂).map f).app K₂).f i₁).f i₂ = (F.map (f.f i₁)).app (K₂.X i₂)
@[simp]
theorem
CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject
{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]
[CategoryTheory.Limits.HasZeroMorphisms C₁]
[CategoryTheory.Limits.HasZeroMorphisms C₂]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C₁ (CategoryTheory.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 = ((CategoryTheory.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)
:
(F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X 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)
:
(F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X 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)
:
K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = K₁.ιMapBifunctor K₂ F c i₁ i₂ j h
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)
:
K₁.ιMapBifunctorOrZero K₂ F c i₁ i₂ j = 0
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))
:
(K₁.mapBifunctor K₂ F c).X j ⟶ 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) (HomologicalComplex.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 (HomologicalComplex.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 : (K₁.mapBifunctor K₂ F c).X j ⟶ Y}
{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)
:
f = 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' : J)
:
(K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X 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' : J)
:
(K₁.mapBifunctor K₂ F c).X j ⟶ (K₁.mapBifunctor K₂ F c).X 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' : J)
:
(K₁.mapBifunctor K₂ F c).d j j' = HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j' + HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c 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)
:
(F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X 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)
:
(F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X 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₁))
:
HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = 0
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₂))
:
HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = 0
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₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
(h' : c₁.π c₂ c (i₁', i₂) ≠ j)
:
HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = 0
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₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
(h' : c₁.π c₂ c (i₁, i₂') ≠ j)
:
HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = 0
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₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
:
HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctorOrZero K₂ F 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₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
:
HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctorOrZero K₂ F 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₁}
(h : c₁.Rel i₁ i₁')
(i₂ : I₂)
(j : J)
(h' : c₁.π c₂ c (i₁', i₂) = j)
:
HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (K₁.d i₁ i₁')).app (K₂.X i₂)) (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h')
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₂' : I₂}
(h : c₂.Rel i₂ i₂')
(j : J)
(h' : c₁.π c₂ c (i₁, i₂') = j)
:
HomologicalComplex.mapBifunctor.d₂ K₁ K₂ F c i₁ i₂ j = c₁.ε₂ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')) (K₁.ιMapBifunctor 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' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
(HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j') = HomologicalComplex.mapBifunctor.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' : 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 (HomologicalComplex.mapBifunctor.D₁ K₁ K₂ F c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.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' : J)
(i₁ : I₁)
(i₂ : I₂)
(h : c₁.π c₂ c (i₁, i₂) = j)
:
CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂ j h)
(HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j') = HomologicalComplex.mapBifunctor.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' : 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 (HomologicalComplex.mapBifunctor.D₂ K₁ K₂ F c j j') h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctor.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₁ : HomologicalComplex C₁ c₁}
{L₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{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]
:
K₁.mapBifunctor K₂ F c ⟶ L₁.mapBifunctor L₂ F c
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₁ : HomologicalComplex C₁ c₁}
{L₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{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)
((HomologicalComplex.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₁ : HomologicalComplex C₁ c₁}
{L₁ : HomologicalComplex C₁ c₁}
{K₂ : HomologicalComplex C₂ c₂}
{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 ((HomologicalComplex.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))