Documentation

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

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

source
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
    Instances For
      source
      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
        Instances For
          source
          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
            source
            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
              Instances For
                source
                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))))
                source
                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
                  source
                  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
                    source
                    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 ℤ
                    source
                    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 ℤ
                    source
                    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