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₂.

noncomputable def CategoryTheory.Functor.mapDerivedCategory {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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 ℤ)

noncomputable instance CategoryTheory.Functor.instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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))))

noncomputable instance CategoryTheory.Functor.instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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 }

noncomputable instance CategoryTheory.Functor.instCommShiftDerivedCategoryMapDerivedCategoryInt {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} 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.instIsTriangulatedDerivedCategoryMapDerivedCategory {C₁ : Type u₁} [Category.{v₁, u₁} C₁] [Abelian C₁] [HasDerivedCategory C₁] {C₂ : Type u₂} [Category.{v₂, u₂} C₂] [Abelian C₂] [HasDerivedCategory C₂] (F : Functor C₁ C₂) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : F.mapDerivedCategory.IsTriangulated