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 ℤ)

theorem CategoryTheory.Functor.mapDerivedCategoryFactors_hom_naturality {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] {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₁} [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] {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)

@[implicit_reducible]

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))))

@[implicit_reducible]

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 }

@[implicit_reducible]

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

@[implicit_reducible]

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

instance CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory {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] (R : Type u_1) [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₁} [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] (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₁} [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] (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₁} [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] (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₁} [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] (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