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 functor F.mapDerivedCategory : DerivedCategory C₁ ⥤ DerivedCategory C₂.

TODO

• show that F.mapDerivedCategory is a triangulated functor

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

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

Equations

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