Ext along an exact functor, from a class of acyclic generators

Let F : D ⥤ C be an exact functor between abelian categories, and let Q be a class of objects of D such that

• every object of D receives an epimorphism from an object of Q,
• Ext^(n+1) P Y = 0 in D for P ∈ Q and every Y,
• Ext^(n+1) (F P) (F Y) = 0 in C for P ∈ Q and every Y, and
• F is bijective on Ext⁰, for instance because it is fully faithful.

Then F induces bijections Ext^n X Y → Ext^n (F X) (F Y) for all X, Y and n. The proof is dimension shifting in the first variable along K ↪ P ↠ X, using the contravariant long exact sequences of Ext in both categories; it is the mirror image of extComparisonAddEquiv in Ext/AcyclicComparison.lean, which shifts in the second variable along injective presentations.

The intended use is the inclusion of coherent sheaves on an affine noetherian scheme into all module sheaves, with Q the free sheaves 𝒪^k: they are projective among coherent sheaves, and Ext^(n+1) (𝒪^k, G) in all module sheaves is H^(n+1)(G)^k, which vanishes for quasi-coherent G on an affine scheme.

Main results

• Ext.subsingleton_of_iso_left, Ext.subsingleton_biproduct_left — vanishing of Ext transports along isomorphisms and finite biproducts in the first variable; Ext.subsingleton_coproduct_left is the corresponding arbitrary-coproduct statement when the derived single functor preserves that coproduct.
• Functor.bijective_mapExtAddHom_zero_iff, Functor.bijective_mapExtAddHom_zero — degree zero.
• Functor.surjective_mapExtAddHom_of_generators, Functor.injective_mapExtAddHom_of_generators, Functor.bijective_mapExtAddHom_of_generators — the theorem.

theorem CategoryTheory.Ext.subsingleton_of_iso_left {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X X' Y : C} (e : X ≅ X') (n : ℕ) (h : Subsingleton (Abelian.Ext X' Y n)) : Subsingleton (Abelian.Ext X Y n)

Vanishing of Ext transports along an isomorphism in the first variable.

theorem CategoryTheory.Ext.subsingleton_biproduct_left {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {J : Type} [Fintype J] (f : J → C) [Limits.HasBiproduct f] (Y : C) (n : ℕ) (h : ∀ (j : J), Subsingleton (Abelian.Ext (f j) Y n)) : Subsingleton (Abelian.Ext (⨁ f) Y n)

Ext out of a finite biproduct vanishes when Ext out of each summand does.

theorem CategoryTheory.Ext.subsingleton_coproduct_left {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {J : Type w'} (f : J → C) [Limits.HasCoproduct f] [HasDerivedCategory C] [Limits.PreservesColimitsOfShape (Discrete J) (DerivedCategory.singleFunctor C 0)] (Y : C) (n : ℕ) (h : ∀ (j : J), Subsingleton (Abelian.Ext (f j) Y n)) : Subsingleton (Abelian.Ext (∐ f) Y n)

Ext out of an arbitrary coproduct vanishes when it vanishes on every summand, provided the derived single functor preserves that coproduct.

The preservation hypothesis is deliberately stated on singleFunctor rather than derived here from AB4. This keeps the lemma applicable to any abelian category whose relevant coproduct survives into the derived category, while DerivedCategory.Coproducts supplies the instance for the scheme-module application.

theorem CategoryTheory.Functor.bijective_mapExtAddHom_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor D C) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt C] [HasExt D] (X Y : D) : Function.Bijective ⇑(F.mapExtAddHom X Y 0) ↔ Function.Bijective F.map

In degree zero, F.mapExtAddHom is F.map up to the identifications Ext⁰ = Hom.

theorem CategoryTheory.Functor.bijective_mapExtAddHom_zero {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor D C) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt C] [HasExt D] [F.Full] [F.Faithful] (X Y : D) : Function.Bijective ⇑(F.mapExtAddHom X Y 0)

A fully faithful exact functor is bijective on Ext⁰.

theorem CategoryTheory.Functor.surjective_mapExtAddHom_of_generators {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor D C) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt C] [HasExt D] (Q : ObjectProperty D) (hpres : ∀ (X : D), ∃ (P : D) (p : P ⟶ X), Q P ∧ Epi p) (hC : ∀ (P : D), Q P → ∀ (Y : D) (n : ℕ), Subsingleton (Abelian.Ext (F.obj P) (F.obj Y) (n + 1))) (h₀ : ∀ (X Y : D), Function.Bijective ⇑(F.mapExtAddHom X Y 0)) (n : ℕ) (X Y : D) : Function.Surjective ⇑(F.mapExtAddHom X Y n)

Surjectivity in every degree. Present X by K ↪ P ↠ X with P ∈ Q; downstairs Ext^n (F K) (F Y) → Ext^(n+1) (F X) (F Y) is surjective because Ext^(n+1) (F P) (F Y) vanishes, so a class lifts by induction and pushes forward.

theorem CategoryTheory.Functor.injective_mapExtAddHom_of_generators {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor D C) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt C] [HasExt D] (Q : ObjectProperty D) (hpres : ∀ (X : D), ∃ (P : D) (p : P ⟶ X), Q P ∧ Epi p) (hD : ∀ (P : D), Q P → ∀ (Y : D) (n : ℕ), Subsingleton (Abelian.Ext P Y (n + 1))) (hC : ∀ (P : D), Q P → ∀ (Y : D) (n : ℕ), Subsingleton (Abelian.Ext (F.obj P) (F.obj Y) (n + 1))) (h₀ : ∀ (X Y : D), Function.Bijective ⇑(F.mapExtAddHom X Y 0)) (n : ℕ) (X Y : D) : Function.Injective ⇑(F.mapExtAddHom X Y n)

Injectivity in every degree. The successor case uses surjectivity in degree n, so the two theorems are not independent.

theorem CategoryTheory.Functor.bijective_mapExtAddHom_of_generators {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (F : Functor D C) [F.Additive] [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] [HasExt C] [HasExt D] (Q : ObjectProperty D) (hpres : ∀ (X : D), ∃ (P : D) (p : P ⟶ X), Q P ∧ Epi p) (hD : ∀ (P : D), Q P → ∀ (Y : D) (n : ℕ), Subsingleton (Abelian.Ext P Y (n + 1))) (hC : ∀ (P : D), Q P → ∀ (Y : D) (n : ℕ), Subsingleton (Abelian.Ext (F.obj P) (F.obj Y) (n + 1))) (h₀ : ∀ (X Y : D), Function.Bijective ⇑(F.mapExtAddHom X Y 0)) (n : ℕ) (X Y : D) : Function.Bijective ⇑(F.mapExtAddHom X Y n)

Ext comparison from acyclic generators. An exact functor bijective on Ext⁰ is bijective on every Ext as soon as a generating class of objects is acyclic on both sides.