Exact functors between derived categories

Exact functors between arbitrary abelian categories preserve strict complex bounds and therefore preserve the canonical derived t-structure and its bounded objects. The file also records that Functor.mapDerivedCategory is functorial up to natural isomorphism: it transports natural isomorphisms and takes identities and composites to identities and composites. No scheme, sheaf, or other geometric input occurs here.

Main definitions

• NatIso.mapDerivedCategory, Functor.mapDerivedCategoryIdIso, and Functor.mapDerivedCategoryCompIso: the pseudofunctoriality of Functor.mapDerivedCategory, each obtained from the corresponding isomorphism on complexes through the universal property of the localization (Localization.liftNatIso);
• Adjunction.mapHomologicalComplex and Adjunction.mapDerivedCategory: additive adjunctions prolong degreewise to homological complexes, and exact adjunctions descend to derived categories;
• Functor.singleFunctorIsoOfFactors: the degree-n embedding commutes with any functor on derived categories that factors degreewise through F;
• DerivedCategory.isoOfFactors, with DerivedCategory.idFactors and DerivedCategory.compFactors: functors on derived categories that factor degreewise through isomorphic functors are isomorphic.

Main results

• mapDerivedCategory_bounded: an exact functor preserves bounded objects.

noncomputable def CategoryTheory.Adjunction.mapHomologicalComplex {A : Type u_1} {B : Type u_2} [Category.{u_5, u_1} A] [Category.{u_6, u_2} B] [Abelian A] [Abelian B] {F : Functor A B} {G : Functor B A} [F.Additive] [G.Additive] (adj : F ⊣ G) {I : Type u_4} (c : ComplexShape I) : F.mapHomologicalComplex c ⊣ G.mapHomologicalComplex c

An adjunction of additive functors prolongs degreewise to homological complexes.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.mapHomologicalComplex_isStrictlyLE {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] (F : Functor A B) [F.Additive] (K : CochainComplex A ℤ) (n : ℤ) (hK : K.IsStrictlyLE n) : CochainComplex.IsStrictlyLE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n

An additive functor sends a strictly bounded-above cochain complex to a strictly bounded-above cochain complex with the same bound.

theorem CategoryTheory.mapHomologicalComplex_isStrictlyGE {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] (F : Functor A B) [F.Additive] (K : CochainComplex A ℤ) (n : ℤ) (hK : K.IsStrictlyGE n) : CochainComplex.IsStrictlyGE ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K) n

An additive functor sends a strictly bounded-below cochain complex to a strictly bounded-below cochain complex with the same bound.

noncomputable def CategoryTheory.Adjunction.mapDerivedCategory {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] {F : Functor A B} {G : Functor B A} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (adj : F ⊣ G) : F.mapDerivedCategory ⊣ G.mapDerivedCategory

An adjunction of exact functors descends to the corresponding derived categories.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.mapDerivedCategory_isLE {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (E : DerivedCategory A) (n : ℤ) (hE : DerivedCategory.TStructure.t.IsLE E n) : DerivedCategory.TStructure.t.IsLE (F.mapDerivedCategory.obj E) n

The functor on derived categories induced by an exact functor preserves the canonical ≤ n truncation bound.

theorem CategoryTheory.mapDerivedCategory_isGE {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (E : DerivedCategory A) (n : ℤ) (hE : DerivedCategory.TStructure.t.IsGE E n) : DerivedCategory.TStructure.t.IsGE (F.mapDerivedCategory.obj E) n

The functor on derived categories induced by an exact functor preserves the canonical ≥ n truncation bound.

theorem CategoryTheory.mapDerivedCategory_bounded {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (E : DerivedCategory A) (hE : DerivedCategory.TStructure.t.bounded E) : DerivedCategory.TStructure.t.bounded (F.mapDerivedCategory.obj E)

Exact functors preserve bounded objects in the canonical derived t-structures.

noncomputable def CategoryTheory.NatIso.mapDerivedCategory {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] {F G : Functor A B} [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] (e : F ≅ G) : F.mapDerivedCategory ≅ G.mapDerivedCategory

A natural isomorphism of exact functors induces a natural isomorphism of the functors on derived categories, by the universal property of the localization applied to NatIso.mapHomologicalComplex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.mapDerivedCategoryIdIso (A : Type u_1) [Category.{u_4, u_1} A] [Abelian A] [HasDerivedCategory A] : (Functor.id A).mapDerivedCategory ≅ Functor.id (DerivedCategory A)

The derived functor of the identity is the identity, up to the natural isomorphism lifted from Functor.mapHomologicalComplexIdIso. The category is explicit because nothing else determines it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.mapDerivedCategoryCompIso {A : Type u_1} {B : Type u_2} {C : Type u_3} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Category.{u_6, u_3} C] [Abelian A] [Abelian B] [Abelian C] [HasDerivedCategory A] [HasDerivedCategory B] [HasDerivedCategory C] {F : Functor A B} {G : Functor B C} {H : Functor A C} (e : F.comp G ≅ H) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [G.Additive] [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] [H.Additive] [Limits.PreservesFiniteLimits H] [Limits.PreservesFiniteColimits H] : F.mapDerivedCategory.comp G.mapDerivedCategory ≅ H.mapDerivedCategory

A factorization F ⋙ G ≅ H of exact functors induces the factorization of the derived functors, in the shape of Functor.mapHomologicalComplexCompIso: the composite is given as a third functor H so that a caller need not elaborate (F ⋙ G).mapDerivedCategory, whose exactness instances comp_preservesFiniteLimits does not supply by search.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Functor.singleFunctorIsoOfFactors {A : Type u_1} {B : Type u_2} [Category.{u_4, u_1} A] [Category.{u_5, u_2} B] [Abelian A] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.PreservesZeroMorphisms] (G : Functor (DerivedCategory A) (DerivedCategory B)) (e : DerivedCategory.Q.comp G ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q) (n : ℤ) : (DerivedCategory.singleFunctor A n).comp G ≅ F.comp (DerivedCategory.singleFunctor B n)

The degree-n embedding commutes with any functor G on derived categories that is degreewise F on complexes, DerivedCategory.Q ⋙ G ≅ F.mapHomologicalComplex _ ⋙ Q. This is the argument of Mathlib's Functor.mapDerivedCategorySingleFunctor, whose G is F.mapDerivedCategory, run on an arbitrary factorization, so that a contract carrying its derived functor as data can use it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DerivedCategory.isoOfFactors {A : Type u_1} {B : Type u_2} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_5, u_2} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] {F₁ F₂ : CategoryTheory.Functor A B} [F₁.PreservesZeroMorphisms] [F₂.PreservesZeroMorphisms] {G₁ G₂ : CategoryTheory.Functor (DerivedCategory A) (DerivedCategory B)} (e₁ : Q.comp G₁ ≅ (F₁.mapHomologicalComplex (ComplexShape.up ℤ)).comp Q) (e₂ : Q.comp G₂ ≅ (F₂.mapHomologicalComplex (ComplexShape.up ℤ)).comp Q) (e : F₁ ≅ F₂) : G₁ ≅ G₂

Two functors on derived categories that factor degreewise through naturally isomorphic functors are isomorphic, by the universal property of the localization: the factorizations are the Localization.Lifting data that Localization.liftNatIso needs. This is how a contract that carries its derived functor as data, with only a factorization Q ⋙ G ≅ F.mapHomologicalComplex _ ⋙ Q, obtains identity and composition laws.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DerivedCategory.idFactors (A : Type u_1) [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Abelian A] [HasDerivedCategory A] : Q.comp (CategoryTheory.Functor.id (DerivedCategory A)) ≅ ((CategoryTheory.Functor.id A).mapHomologicalComplex (ComplexShape.up ℤ)).comp Q

The identity of the derived category factors degreewise through the identity, by Functor.mapHomologicalComplexIdIso; the input of DerivedCategory.isoOfFactors for an identity law. The category is explicit because nothing else determines it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DerivedCategory.compFactors {A : Type u_1} {B : Type u_2} {C : Type u_3} [CategoryTheory.Category.{u_4, u_1} A] [CategoryTheory.Category.{u_5, u_2} B] [CategoryTheory.Category.{u_6, u_3} C] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] [CategoryTheory.Abelian C] [HasDerivedCategory A] [HasDerivedCategory B] [HasDerivedCategory C] {F₁ : CategoryTheory.Functor A B} {F₂ : CategoryTheory.Functor B C} [F₁.PreservesZeroMorphisms] [F₂.PreservesZeroMorphisms] {G₁ : CategoryTheory.Functor (DerivedCategory A) (DerivedCategory B)} {G₂ : CategoryTheory.Functor (DerivedCategory B) (DerivedCategory C)} (e₁ : Q.comp G₁ ≅ (F₁.mapHomologicalComplex (ComplexShape.up ℤ)).comp Q) (e₂ : Q.comp G₂ ≅ (F₂.mapHomologicalComplex (ComplexShape.up ℤ)).comp Q) : Q.comp (G₁.comp G₂) ≅ ((F₁.comp F₂).mapHomologicalComplex (ComplexShape.up ℤ)).comp Q

A composite of two functors that factor degreewise factors degreewise through the composite; (F₁ ⋙ F₂).mapHomologicalComplex is definitionally the composite of the two, so only associators enter. The input of DerivedCategory.isoOfFactors for a composition law.

Equations

• One or more equations did not get rendered due to their size.