The derived functor of an exact functor on bounded objects

Let F : A ⥤ B be an exact functor between abelian categories and F.mapDerivedCategory : DerivedCategory A ⥤ DerivedCategory B its derived functor. Suppose F induces bijections on all Ext groups,

Ext^n_A(X, Y) → Ext^n_B(F X, F Y) for all X Y : A and n : ℕ.

Then this file proves:

• Functor.mapDerivedCategory_map_bijective_of_bounded: the derived functor is fully faithful on bounded objects;
• Functor.exists_bounded_iso_mapDerivedCategory_obj: every bounded object of DerivedCategory B whose cohomology objects lie in the essential image of F is isomorphic to the image of a bounded object of DerivedCategory A.

Together these say that Dᵇ(A) ⥤ Dᵇ_{F(A)}(B) is an equivalence as soon as F is an Ext-isomorphism on the hearts. Nothing here asks F to be full, faithful, or an inclusion; both of those follow from the Ext⁰ case.

Proof

Everything is a dévissage on cohomological amplitude, run through DerivedCategory.bounded_induction. The step is the five lemma applied to the long exact Hom sequences of a distinguished triangle and of its image, with F.mapDerivedCategory supplying the vertical maps. That lemma is stated twice, once in each variable (mapDerivedCategory_map_bijective_obj₃_left and mapDerivedCategory_map_bijective_obj₃_right), because Hom is contravariant in the first variable and covariant in the second; both are proved for the third object of a triangle, and the middle-object statements follow by inverse rotation. Full faithfulness on single objects, the base case, is exactly the Ext hypothesis once Ext.mapExactFunctor_hom and the vanishing of negative Ext in both categories are unwound. Essential surjectivity is the standard cone argument: a bounded object with cohomology in the essential image is an extension of two objects of smaller amplitude that are already images, the connecting morphism lifts by full faithfulness, and the image of a cone in A is a cone in B.

Why the hypothesis is Ext-bijectivity

For F the inclusion of a weak Serre subcategory this is the classical statement that Dᵇ(A) → Dᵇ_A(B) is an equivalence; it is not automatic and does need an input on Ext. Mathlib proves the Ext hypothesis in two cases (Functor.mapExt_bijective_of_preservesProjectiveObjects and Functor.mapExt_bijective_of_preservesInjectiveObjects); a geometric consumer supplies it separately.

Implementation notes

Every shift comparison isomorphism (F.mapDerivedCategory.commShiftIso n).app X is given an explicit type (F.mapDerivedCategory.obj X)⟦n⟧ ≅ … before use. Mathlib states it between (F ⋙ shiftFunctor _ n).obj X and (shiftFunctor _ n ⋙ F).obj X, which are only definitionally the shifted objects, and rw/simp do not see through Functor.comp at instance transparency; the annotated lets keep every composite well-typed on the nose.

Transport of bijectivity along isomorphisms and shifts

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_iff_of_iso_left {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {E₁ E₂ : DerivedCategory A} (e : E₁ ≅ E₂) (W : DerivedCategory A) : Function.Bijective F.mapDerivedCategory.map ↔ Function.Bijective F.mapDerivedCategory.map

Bijectivity of F.mapDerivedCategory on a hom-set is invariant under isomorphism of the source object.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_iff_of_iso_right {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (E : DerivedCategory A) {W₁ W₂ : DerivedCategory A} (e : W₁ ≅ W₂) : Function.Bijective F.mapDerivedCategory.map ↔ Function.Bijective F.mapDerivedCategory.map

Bijectivity of F.mapDerivedCategory on a hom-set is invariant under isomorphism of the target object.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_shift_iff {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (E W : DerivedCategory A) (a : ℤ) : Function.Bijective F.mapDerivedCategory.map ↔ Function.Bijective F.mapDerivedCategory.map

Bijectivity of F.mapDerivedCategory on a hom-set is invariant under shifting both objects by the same integer, because the derived functor commutes with shifts.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_shift_left {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {E W : DerivedCategory A} (h : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (m k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Shifting the source: bijectivity for all shifts of the target gives bijectivity for all shifts of the source as well.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_of_forall_shift {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] {E W : DerivedCategory A} (h : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) : Function.Bijective F.mapDerivedCategory.map

Bijectivity for all shifts of the target gives bijectivity for the target itself.

The five lemma on the long exact Hom sequences of a distinguished triangle

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_obj₃_left {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (T : Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ Pretriangulated.distinguishedTriangles) (W : DerivedCategory A) (h₁ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (h₂ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Contravariant cone closure. If F.mapDerivedCategory is bijective on morphisms from the first two objects of a distinguished triangle to all shifts of W, it is bijective on morphisms from the third object to all shifts of W.

The five lemma is applied to the rows Hom(T₂⟦1⟧, W') → Hom(T₁⟦1⟧, W') → Hom(T₃, W') → Hom(T₂, W') → Hom(T₁, W') and their images, with W' := W⟦k⟧.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_obj₃_right {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (T : Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ Pretriangulated.distinguishedTriangles) (V : DerivedCategory A) (h₁ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (h₂ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Covariant cone closure. If F.mapDerivedCategory is bijective on morphisms from V to all shifts of the first two objects of a distinguished triangle, it is bijective on morphisms from V to all shifts of the third object.

The five lemma is applied, for the k-shifted triangle S, to the rows Hom(V, S₁) → Hom(V, S₂) → Hom(V, S₃) → Hom(V, S₁⟦1⟧) → Hom(V, S₂⟦1⟧) and their images.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_obj₂_left {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (T : Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ Pretriangulated.distinguishedTriangles) (W : DerivedCategory A) (h₁ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (h₃ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Cone closure in the first variable for the middle object of a distinguished triangle, by inverse rotation.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_obj₂_right {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (T : Pretriangulated.Triangle (DerivedCategory A)) (hT : T ∈ Pretriangulated.distinguishedTriangles) (V : DerivedCategory A) (h₁ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (h₃ : ∀ (k : ℤ), Function.Bijective F.mapDerivedCategory.map) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Cone closure in the second variable for the middle object of a distinguished triangle, by inverse rotation.

The base case: single objects and Ext

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_single_of_neg {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] (X Y : A) (k : ℤ) (hk : k < 0) : Function.Bijective F.mapDerivedCategory.map

Negative Ext vanishes in both categories, so F.mapDerivedCategory is trivially bijective on morphisms (singleFunctor A 0).obj X ⟶ ((singleFunctor A 0).obj Y)⟦k⟧ for k < 0.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_single_iff_mapExt_bijective {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt A] [HasExt B] (X Y : A) (n : ℕ) : Function.Bijective F.mapDerivedCategory.map ↔ Function.Bijective ⇑(F.mapExtAddHom X Y n)

Unwinding Ext.mapExactFunctor_hom: bijectivity of F.mapExtAddHom X Y n is bijectivity of F.mapDerivedCategory on morphisms (singleFunctor A 0).obj X ⟶ ((singleFunctor A 0).obj Y)⟦n⟧.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_single {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt A] [HasExt B] (hF : ∀ (X Y : A) (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)) (X Y : A) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Under the Ext hypothesis, F.mapDerivedCategory is bijective on all morphisms between degree-zero single objects and their shifts.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_bounded_single {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt A] [HasExt B] (hF : ∀ (X Y : A) (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)) {E : DerivedCategory A} (hE : DerivedCategory.TStructure.t.bounded E) (Y : A) (k : ℤ) : Function.Bijective F.mapDerivedCategory.map

Under the Ext hypothesis, F.mapDerivedCategory is bijective on morphisms from any bounded object to any shift of a degree-zero single object: the first-variable dévissage.

theorem CategoryTheory.Functor.mapDerivedCategory_map_bijective_of_bounded {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt A] [HasExt B] (hF : ∀ (X Y : A) (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)) {E E' : DerivedCategory A} (hE : DerivedCategory.TStructure.t.bounded E) (hE' : DerivedCategory.TStructure.t.bounded E') : Function.Bijective F.mapDerivedCategory.map

Full faithfulness on bounded objects. If F induces bijections on all Ext groups, then F.mapDerivedCategory is bijective on morphisms between bounded objects: the second-variable dévissage, on top of the first.

theorem CategoryTheory.Functor.exists_bounded_iso_mapDerivedCategory_obj {A : Type u} [Category.{v, u} A] [Abelian A] {B : Type u'} [Category.{v', u'} B] [Abelian B] [HasDerivedCategory A] [HasDerivedCategory B] (F : Functor A B) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt A] [HasExt B] (hF : ∀ (X Y : A) (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)) {E' : DerivedCategory B} (hE' : DerivedCategory.TStructure.t.bounded E') (hP : DerivedCategory.cohomologyIn F.essImage E') : ∃ (E : DerivedCategory A), DerivedCategory.TStructure.t.bounded E ∧ Nonempty (F.mapDerivedCategory.obj E ≅ E')

Essential surjectivity onto the cohomological image. If F induces bijections on all Ext groups, every bounded object of DerivedCategory B whose cohomology objects lie in the essential image of F is isomorphic to the image of a bounded object of DerivedCategory A.

The cone step: for a distinguished triangle E₁ ⟶ E ⟶ E₃ ⟶ E₁⟦1⟧ with E₁ ≅ F X and E₃ ≅ F Z for bounded X, Z, the connecting morphism lifts to g : Z ⟶ X⟦1⟧ by full faithfulness; a distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ with third morphism g has bounded Y, and its image is isomorphic to the given triangle by isIso₂_of_isIso₁₃.