Ext along an exact functor, from a fixed comparison morphism

Let R : D ⥤ C be an exact functor between abelian categories, P : D, A : C, and u : A ⟶ R.obj P. Pushing a class along R and precomposing with u gives

extComparisonMap u : Ext^n P B → Ext^n A (R B)

for every B : D and every n. This file proves that the comparison is bijective in every degree as soon as

• it is bijective in degree zero, and
• Ext^(n+1) A (R I) vanishes for every injective I : D (R I is acyclic against A),

provided D has enough injectives. The proof is dimension shifting along an injective presentation B ↪ I ↠ Q, exactly as for extAdjunctionAddEquiv in Ext/Adjunction.lean; that theorem is the special case u := adj.unit.app A of an adjunction L ⊣ R with L exact, where the acyclicity hypothesis holds because R I is then injective. Here nothing is assumed about a left adjoint, which is what a cohomology comparison needs when the left adjoint is only right exact: the forgetful functor from module sheaves to abelian sheaves has the extension-of-scalars functor as left adjoint, which is not exact, but its images of injective module sheaves are still acyclic, because they are flasque.

Main results

• extComparisonMap, extComparisonAddHom — the comparison and its additivity.
• extComparisonMap_comp_mk₀, extComparisonMap_comp_extClass — the comparison is a morphism of the two long exact Ext sequences.
• surjective_extComparisonMap, injective_extComparisonMap, extComparisonAddEquiv — the theorem.

noncomputable def CategoryTheory.extComparisonMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {B : D} {n : ℕ} (e : Abelian.Ext P B n) : Abelian.Ext A (R.obj B) n

The comparison Ext^n P B → Ext^n A (R B). Push the class along R, then precompose with u.

Equations

• CategoryTheory.extComparisonMap u e = (CategoryTheory.Abelian.Ext.mk₀ u).comp (CategoryTheory.Abelian.Ext.mapExactFunctor R e) ⋯

@[simp]

theorem CategoryTheory.extComparisonMap_zero {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {B : D} {n : ℕ} : extComparisonMap u 0 = 0

theorem CategoryTheory.extComparisonMap_add {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {B : D} {n : ℕ} (e f : Abelian.Ext P B n) : extComparisonMap u (e + f) = extComparisonMap u e + extComparisonMap u f

noncomputable def CategoryTheory.extComparisonAddHom {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) (B : D) (n : ℕ) : Abelian.Ext P B n →+ Abelian.Ext A (R.obj B) n

The comparison as an additive map.

Equations

• CategoryTheory.extComparisonAddHom u B n = { toFun := CategoryTheory.extComparisonMap u, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.extComparisonAddHom_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) (B : D) (n : ℕ) (e : Abelian.Ext P B n) : (extComparisonAddHom u B n) e = extComparisonMap u e

theorem CategoryTheory.extComparisonMap_comp {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {Y Z : D} {a b c : ℕ} (x : Abelian.Ext P Y a) (e : Abelian.Ext Y Z b) (h : a + b = c) : extComparisonMap u (x.comp e h) = (extComparisonMap u x).comp (Abelian.Ext.mapExactFunctor R e) h

The comparison is natural in the second variable.

theorem CategoryTheory.extComparisonMap_comp_mk₀ {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {Y Z : D} {a : ℕ} (x : Abelian.Ext P Y a) (f : Y ⟶ Z) : extComparisonMap u (x.comp (Abelian.Ext.mk₀ f) ⋯) = (extComparisonMap u x).comp (Abelian.Ext.mk₀ (R.map f)) ⋯

Naturality against a morphism: the square for the maps of the long exact sequences induced by S.f and S.g.

theorem CategoryTheory.extComparisonMap_comp_extClass {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {S : ShortComplex D} (hS : S.ShortExact) {n₀ n₁ : ℕ} (hn₁ : n₀ + 1 = n₁) (x₃ : Abelian.Ext P S.X₃ n₀) : extComparisonMap u (x₃.comp hS.extClass hn₁) = (extComparisonMap u x₃).comp ⋯.extClass hn₁

The connecting square: the comparison commutes with the connecting class of a short exact sequence, because R carries the sequence to a short exact sequence and Ext.mapExactFunctor_extClass carries the class along.

theorem CategoryTheory.extComparisonMap_mk₀ {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) {B : D} (f : P ⟶ B) : extComparisonMap u (Abelian.Ext.mk₀ f) = Abelian.Ext.mk₀ (CategoryStruct.comp u (R.map f))

In degree zero the comparison sends mk₀ f to mk₀ (u ≫ R.map f).

theorem CategoryTheory.bijective_extComparisonMap_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) (B : D) : Function.Bijective (extComparisonMap u) ↔ Function.Bijective fun (f : P ⟶ B) => CategoryStruct.comp u (R.map f)

The degree-zero comparison is bijective iff f ↦ u ≫ R.map f is, under the identifications Ext⁰ = Hom. This is how the degree-zero hypothesis of extComparisonAddEquiv is checked in practice.

theorem CategoryTheory.surjective_extComparisonMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) [EnoughInjectives D] (h₀ : ∀ (B : D), Function.Bijective (extComparisonMap u)) (hacyclic : ∀ (I : D) [Injective I] (n : ℕ), Subsingleton (Abelian.Ext A (R.obj I) (n + 1))) (n : ℕ) (B : D) : Function.Surjective (extComparisonMap u)

The comparison is surjective in every degree. Embed B in an injective I with quotient Q; both connecting maps Ext^n(-, Q) → Ext^(n+1)(-, B) are surjective, upstairs because Ext^(n+1) P I vanishes and downstairs by acyclicity of R I, so a class pulls back, lifts by induction, and pushes forward.

theorem CategoryTheory.injective_extComparisonMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) [EnoughInjectives D] (h₀ : ∀ (B : D), Function.Bijective (extComparisonMap u)) (hacyclic : ∀ (I : D) [Injective I] (n : ℕ), Subsingleton (Abelian.Ext A (R.obj I) (n + 1))) (n : ℕ) (B : D) : Function.Injective (extComparisonMap u)

The comparison is injective in every degree. The successor case uses surjectivity in degree n to lift the class that exactness produces, so the two theorems are not independent.

noncomputable def CategoryTheory.extComparisonAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) [EnoughInjectives D] (h₀ : ∀ (B : D), Function.Bijective (extComparisonMap u)) (hacyclic : ∀ (I : D) [Injective I] (n : ℕ), Subsingleton (Abelian.Ext A (R.obj I) (n + 1))) (B : D) (n : ℕ) : Abelian.Ext P B n ≃+ Abelian.Ext A (R.obj B) n

Ext comparison from acyclicity of images of injectives. Ext^n P B ≃+ Ext^n A (R B) for every n, given bijectivity in degree zero and vanishing of Ext^(n+1) A (R I) for injective I.

Equations

• CategoryTheory.extComparisonAddEquiv u h₀ hacyclic B n = AddEquiv.ofBijective (CategoryTheory.extComparisonAddHom u B n) ⋯

@[simp]

theorem CategoryTheory.extComparisonAddEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {R : Functor D C} [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {P : D} (u : A ⟶ R.obj P) [EnoughInjectives D] (h₀ : ∀ (B : D), Function.Bijective (extComparisonMap u)) (hacyclic : ∀ (I : D) [Injective I] (n : ℕ), Subsingleton (Abelian.Ext A (R.obj I) (n + 1))) (B : D) (n : ℕ) (e : Abelian.Ext P B n) : (extComparisonAddEquiv u h₀ hacyclic B n) e = extComparisonMap u e