An exact functor induces a functor on derived categories

In this file, we show that if F : C₁ ⥤ C₂ is an exact functor between abelian categories, then there is an induced triangulated functor F.mapDerivedCategory : DerivedCategory C₁ ⥤ DerivedCategory C₂. We study some of the pseudofunctorial properties of this construction, but we do not define the pseudofunctor which sends an abelian category to its derived category (TODO).

noncomputable def CategoryTheory.Functor.mapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : Functor (DerivedCategory C₁) (DerivedCategory C₂)

The functor DerivedCategory C₁ ⥤ DerivedCategory C₂ induced by an exact functor F : C₁ ⥤ C₂ between abelian categories.

Equations

• F.mapDerivedCategory = F.mapHomologicalComplexUpToQuasiIso (ComplexShape.up ℤ)

noncomputable def CategoryTheory.Functor.mapDerivedCategoryFactors {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : DerivedCategory.Q.comp F.mapDerivedCategory ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q

The functor F.mapDerivedCategory is induced by F.mapHomologicalComplex (ComplexShape.up ℤ).

Equations

• F.mapDerivedCategoryFactors = F.mapHomologicalComplexUpToQuasiIsoFactors (ComplexShape.up ℤ)

theorem CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y) : CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f)) (F.mapDerivedCategoryFactors.hom.app Y) = CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f))

theorem CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {X Y : CochainComplex C₁ ℤ} (f : X ⟶ Y) {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj Y) ⟶ Z) : CategoryStruct.comp (F.mapDerivedCategory.map (DerivedCategory.Q.map f)) (CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app Y) h) = CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryStruct.comp (DerivedCategory.Q.map ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map f)) h)

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) F.mapDerivedCategory

Equations

• F.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory = { iso := F.mapDerivedCategoryFactors }

noncomputable def CategoryTheory.Functor.mapDerivedCategoryFactorsh {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : DerivedCategory.Qh.comp F.mapDerivedCategory ≅ (F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh

The functor F.mapDerivedCategory is induced by F.mapHomotopyCategory (ComplexShape.up ℤ).

Equations

• F.mapDerivedCategoryFactorsh = F.mapHomologicalComplexUpToQuasiIsoFactorsh (ComplexShape.up ℤ)

theorem CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (K : CochainComplex C₁ ℤ) : F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient C₁ (ComplexShape.up ℤ)).obj K) = CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K)) (CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app K) (CategoryStruct.comp ((DerivedCategory.quotientCompQhIso C₂).inv.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K)) (DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K))))

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : Localization.Lifting DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh) F.mapDerivedCategory

Equations

• F.instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory = { iso := F.mapDerivedCategoryFactorsh }

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instCommShiftDerivedCategoryMapDerivedCategoryInt {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.CommShift ℤ

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : NatTrans.CommShift F.mapDerivedCategoryFactorsh.hom ℤ

instance CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : NatTrans.CommShift F.mapDerivedCategoryFactors.hom ℤ

instance CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomIsoQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : NatTrans.CommShift (Localization.Lifting.iso DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) F.mapDerivedCategory).hom ℤ

instance CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.IsTriangulated

@[instance_reducible]

instance CategoryTheory.Functor.instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.CommShift ℤ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.mapDerivedCategorySingleFunctor {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (n : ℤ) : (DerivedCategory.singleFunctor C₁ n).comp F.mapDerivedCategory ≅ F.comp (DerivedCategory.singleFunctor C₂ n)

DerivedCategory.singleFunctor commutes with F and F.mapDerivedCategory.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (n : ℤ) (X : C₁) : (F.mapDerivedCategorySingleFunctor n).hom.app X = CategoryStruct.comp (F.mapDerivedCategory.map ((DerivedCategory.singleFunctorIsoCompQ C₁ n).hom.app X)) (CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app ((CochainComplex.singleFunctor C₁ n).obj X)) (CategoryStruct.comp (DerivedCategory.Q.map ((HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n).hom.app X)) ((DerivedCategory.singleFunctorIsoCompQ C₂ n).inv.app (F.obj X))))

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (n : ℤ) (X : C₁) : (F.mapDerivedCategorySingleFunctor n).inv.app X = CategoryStruct.comp ((DerivedCategory.singleFunctorIsoCompQ C₂ n).hom.app (F.obj X)) (CategoryStruct.comp (DerivedCategory.Q.map ((HomologicalComplex.singleMapHomologicalComplex F (ComplexShape.up ℤ) n).inv.app X)) (CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((CochainComplex.singleFunctor C₁ n).obj X)) (F.mapDerivedCategory.map ((DerivedCategory.singleFunctorIsoCompQ C₁ n).inv.app X))))

instance CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (R : Type u_4) [Ring R] [CategoryTheory.Linear R C₁] [CategoryTheory.Linear R C₂] [Linear R F] : Linear R F.mapDerivedCategory

@[simp]

theorem CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X : C₁) : CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) ((F.mapDerivedCategorySingleFunctor 0).hom.app X) = DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)

@[simp]

theorem CategoryTheory.Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂} (h : (DerivedCategory.singleFunctor C₂ 0).obj (F.obj X) ⟶ Z) : CategoryStruct.comp (F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) (CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).hom.app X) h) = CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)) h

@[simp]

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X : C₁) : CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X) (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) = DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)

@[simp]

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_mapDerivedCategoryFactors_hom_app_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X : C₁) {Z : DerivedCategory C₂} (h : DerivedCategory.Q.obj ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) ⟶ Z) : CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor 0).inv.app X) (CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X)) h) = CategoryStruct.comp (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)) h

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpMapDerivedCategoryId {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] : Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) DerivedCategory.Q (Functor.id C₁).mapDerivedCategory

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomIsoQQuasiIsoUpMapDerivedCategoryId {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] : NatTrans.CommShift (Localization.Lifting.iso DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) DerivedCategory.Q (Functor.id C₁).mapDerivedCategory).hom ℤ

noncomputable def CategoryTheory.Functor.mapDerivedCategoryIdIso (C₁ : Type u_1) [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] : (Functor.id C₁).mapDerivedCategory ≅ Functor.id (DerivedCategory C₁)

The functor DerivedCategory C₁ ⥤ DerivedCategory C₁ induced by the identity functor of C₁ identifies to the identity functor of the derived category.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftDerivedCategoryHomMapDerivedCategoryIdIsoInt {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] : NatTrans.CommShift (mapDerivedCategoryIdIso C₁).hom ℤ

theorem CategoryTheory.Functor.mapDerivedCategoryIdIso_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] (X : CochainComplex C₁ ℤ) : (mapDerivedCategoryIdIso C₁).hom.app (DerivedCategory.Q.obj X) = CategoryStruct.comp ((Functor.id C₁).mapDerivedCategoryFactors.hom.app X) (DerivedCategory.Q.map ((mapHomologicalComplexIdIso C₁ (ComplexShape.up ℤ)).hom.app X))

theorem CategoryTheory.Functor.mapDerivedCategoryIdIso_hom_app_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] (X : CochainComplex C₁ ℤ) {Z : DerivedCategory C₁} (h : DerivedCategory.Q.obj X ⟶ Z) : CategoryStruct.comp ((mapDerivedCategoryIdIso C₁).hom.app (DerivedCategory.Q.obj X)) h = CategoryStruct.comp ((Functor.id C₁).mapDerivedCategoryFactors.hom.app X) (CategoryStruct.comp (DerivedCategory.Q.map ((mapHomologicalComplexIdIso C₁ (ComplexShape.up ℤ)).hom.app X)) h)

theorem CategoryTheory.Functor.mapDerivedCategoryIdIso_hom_app_singleFunctor_obj {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] (X : C₁) : (mapDerivedCategoryIdIso C₁).hom.app ((DerivedCategory.singleFunctor C₁ 0).obj X) = ((Functor.id C₁).mapDerivedCategorySingleFunctor 0).hom.app X

theorem CategoryTheory.Functor.mapDerivedCategoryIdIso_inv_app_singleFunctor_obj {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] (X : C₁) : (mapDerivedCategoryIdIso C₁).inv.app ((DerivedCategory.singleFunctor C₁ 0).obj X) = ((Functor.id C₁).mapDerivedCategorySingleFunctor 0).inv.app X

@[instance_reducible]

noncomputable instance CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory_1 {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp ((G.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q)) (F.mapDerivedCategory.comp G.mapDerivedCategory)

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomIsoQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory_1 {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : NatTrans.CommShift (Localization.Lifting.iso DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ)) ((F.mapHomologicalComplex (ComplexShape.up ℤ)).comp ((G.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q)) (F.mapDerivedCategory.comp G.mapDerivedCategory)).hom ℤ

noncomputable def CategoryTheory.Functor.mapDerivedCategoryCompIso {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : F.mapDerivedCategory.comp G.mapDerivedCategory ≅ (F.comp G).mapDerivedCategory

If F and G are exact functors between abelian categories, the composition of the induced functors on the derived category identifies to the functor induced by F ⋙ G.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.instCommShiftDerivedCategoryHomMapDerivedCategoryCompIsoInt {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : NatTrans.CommShift (F.mapDerivedCategoryCompIso G).hom ℤ

theorem CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_Q_obj {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (X : CochainComplex C₁ ℤ) : (F.mapDerivedCategoryCompIso G).hom.app (DerivedCategory.Q.obj X) = CategoryStruct.comp (G.mapDerivedCategory.map (F.mapDerivedCategoryFactors.hom.app X)) (CategoryStruct.comp (G.mapDerivedCategoryFactors.hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj X)) (CategoryStruct.comp (DerivedCategory.Q.map ((mapHomologicalComplexCompIso (Iso.refl (F.comp G)) (ComplexShape.up ℤ)).hom.app X)) ((F.comp G).mapDerivedCategoryFactors.inv.app X)))

theorem CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_comp_mapDerivedCategorySingleFunctor_hom_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (X : C₁) (n : ℤ) : CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).hom.app ((DerivedCategory.singleFunctor C₁ n).obj X)) (((F.comp G).mapDerivedCategorySingleFunctor n).hom.app X) = CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor n).hom.app X)) ((G.mapDerivedCategorySingleFunctor n).hom.app (F.obj X))

theorem CategoryTheory.Functor.mapDerivedCategoryCompIso_hom_app_comp_mapDerivedCategorySingleFunctor_hom_app_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (X : C₁) (n : ℤ) {Z : DerivedCategory C₃} (h : (DerivedCategory.singleFunctor C₃ n).obj (G.obj (F.obj X)) ⟶ Z) : CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).hom.app ((DerivedCategory.singleFunctor C₁ n).obj X)) (CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor n).hom.app X) h) = CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor n).hom.app X)) (CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor n).hom.app (F.obj X)) h)

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_comp_mapDerivedCategoryCompIso_inv_app {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (X : C₁) : CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor 0).inv.app X) ((F.mapDerivedCategoryCompIso G).inv.app ((DerivedCategory.singleFunctor C₁ 0).obj X)) = CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor 0).inv.app (F.obj X)) (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor 0).inv.app X))

theorem CategoryTheory.Functor.mapDerivedCategorySingleFunctor_inv_app_comp_mapDerivedCategoryCompIso_inv_app_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {C₃ : Type u_3} [Category.{v_3, u_3} C₃] [Abelian C₃] [HasDerivedCategory C₃] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (G : Functor C₂ C₃) [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (X : C₁) {Z : DerivedCategory C₃} (h : G.mapDerivedCategory.obj (F.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C₁ 0).obj X)) ⟶ Z) : CategoryStruct.comp (((F.comp G).mapDerivedCategorySingleFunctor 0).inv.app X) (CategoryStruct.comp ((F.mapDerivedCategoryCompIso G).inv.app ((DerivedCategory.singleFunctor C₁ 0).obj X)) h) = CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor 0).inv.app (F.obj X)) (CategoryStruct.comp (G.mapDerivedCategory.map ((F.mapDerivedCategorySingleFunctor 0).inv.app X)) h)

noncomputable def CategoryTheory.NatTrans.mapDerivedCategory {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) : F.mapDerivedCategory ⟶ G.mapDerivedCategory

A natural transformation between exact functors between abelian categories induces a natural transformation between the corresponding induced functors on the derived categories.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.NatTrans.instCommShiftDerivedCategoryMapDerivedCategoryInt {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) : CommShift (mapDerivedCategory τ) ℤ

theorem CategoryTheory.NatTrans.mapDerivedCategory_app_Q_obj {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : CochainComplex C₁ ℤ) : (mapDerivedCategory τ).app (DerivedCategory.Q.obj X) = CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryStruct.comp (DerivedCategory.Q.map ((mapHomologicalComplex τ (ComplexShape.up ℤ)).app X)) (G.mapDerivedCategoryFactors.inv.app X))

theorem CategoryTheory.NatTrans.mapDerivedCategory_app_Q_obj_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : CochainComplex C₁ ℤ) {Z : DerivedCategory C₂} (h : G.mapDerivedCategory.obj (DerivedCategory.Q.obj X) ⟶ Z) : CategoryStruct.comp ((mapDerivedCategory τ).app (DerivedCategory.Q.obj X)) h = CategoryStruct.comp (F.mapDerivedCategoryFactors.hom.app X) (CategoryStruct.comp (DerivedCategory.Q.map ((mapHomologicalComplex τ (ComplexShape.up ℤ)).app X)) (CategoryStruct.comp (G.mapDerivedCategoryFactors.inv.app X) h))

theorem CategoryTheory.NatTrans.mapDerivedCategory_app_singleFunctor_obj {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : C₁) (n : ℤ) : (mapDerivedCategory τ).app ((DerivedCategory.singleFunctor C₁ n).obj X) = CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor n).hom.app X) (CategoryStruct.comp ((DerivedCategory.singleFunctor C₂ n).map (τ.app X)) ((G.mapDerivedCategorySingleFunctor n).inv.app X))

theorem CategoryTheory.NatTrans.mapDerivedCategory_app_singleFunctor_obj_assoc {C₁ : Type u_1} [Category.{v_1, u_1} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u_2} [Category.{v_2, u_2} C₂] [Abelian C₂] [HasDerivedCategory C₂] {F : Functor C₁ C₂} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {G : Functor C₁ C₂} [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (τ : F ⟶ G) (X : C₁) (n : ℤ) {Z : DerivedCategory C₂} (h : G.mapDerivedCategory.obj ((DerivedCategory.singleFunctor C₁ n).obj X) ⟶ Z) : CategoryStruct.comp ((mapDerivedCategory τ).app ((DerivedCategory.singleFunctor C₁ n).obj X)) h = CategoryStruct.comp ((F.mapDerivedCategorySingleFunctor n).hom.app X) (CategoryStruct.comp ((DerivedCategory.singleFunctor C₂ n).map (τ.app X)) (CategoryStruct.comp ((G.mapDerivedCategorySingleFunctor n).inv.app X) h))