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]
:
The functor DerivedCategory C₁ ⥤ DerivedCategory C₂
induced
by an exact functor F : C₁ ⥤ C₂
between abelian categories.
Equations
- F.mapDerivedCategory = F.mapHomologicalComplexUpToQuasiIso (ComplexShape.up ℤ)
Instances For
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 ℤ)
Instances For
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 ℤ)
Instances For
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 }