Ext along an adjunction with exact left adjoint

For L ⊣ R between abelian categories with L and R exact, there is a comparison

Ext^n (L A) B → Ext^n A (R B)

pushing a class along R and precomposing with the unit. This file constructs it, proves it is additive, and settles the two ends of the intended induction: degree zero, and positive degree on an injective.

Why this file exists

Sheaf.H n F is Ext out of the constant sheaf — the derived-category Ext of Algebra/Homology/DerivedCategory/Ext/, not the injective-resolution Ext R C n of CategoryTheory/Abelian/Ext.lean. So the cohomology comparison #572 step 3 asks for, Hⁱ(X, F) ≅ Hⁱ(Pⁿ, ι_* F) along a closed immersion, is an Ext transport along ι⁻¹ ⊣ ι_* and not a Čech computation. Sites/Sheaves/ConstantPullback.lean moved the constant sheaf across that adjunction; this file is the other half.

Nothing at the pin relates Ext to an adjunction. Grepping Algebra/Homology/ and CategoryTheory/Abelian/ returns nothing under any spelling, so the statement here is new to the tree and is not specific to sheaves — it is stated for arbitrary abelian categories.

Exactness of R is a real hypothesis

Ext.mapExactFunctor requires its functor exact, so R is assumed exact and not merely left exact. That is legitimate for the intended application — ι_* along a closed immersion is exact — but it is not the general shape of an adjunction, and a caller who has only a left-exact right adjoint gets nothing from this file.

The theorem

extAdjunctionAddEquiv — the comparison is an isomorphism of additive groups in every degree. EnoughInjectives D is what the proof needs and the only hypothesis beyond exactness.

Both halves are inductions on the degree, and both run on the same three-step shape: embed B ↪ I with I injective, take the cokernel Q, and use that R carries that short exact sequence to a short exact sequence in C whose middle term R I is again injective — which is preservesInjectiveObjects_of_adj, and is the reason the argument closes at all.

• Surjectivity. The connecting map Ext^n(-, Q) → Ext^{n+1}(-, B) is surjective on both sides, because the terms next to it vanish on an injective. Pull the target class back downstairs, lift it by the inductive hypothesis, and push it forward: the two connecting maps agree with the comparison by extAdjunctionMap_comp_extClass.
• Injectivity. Given x in the kernel, write x = x' ∘ δ by that same surjectivity. Then φ x' dies against δ', so by exactness downstairs it factors as w ∘ R g. Lift w through the comparison — this is where surjectivity in degree n is used to prove injectivity in degree n + 1, so the two theorems are not independent and the order matters — and conclude x' = v ∘ g by the inductive hypothesis. Then x = v ∘ (g ∘ δ) = 0, because consecutive maps of a long exact sequence compose to zero.

The degree-zero base cases are extAdjunctionMap_mk₀: there the comparison is the adjunction's hom-equivalence, which is bijective because Adjunction.homEquiv is an Equiv.

bijective_extAdjunctionMap_of_injective is not used by either induction. It is kept because it is the statement that makes the shape plausible before the induction is written, and because it is the cheap sanity check on the setup: if the comparison were wrong, it would already fail there.

A rw/simp trap worth recording

Ext.mk₀_comp_mk₀ is @[simp], its statement matches extAdjunctionMap's composite at degree zero syntactically, and neither rw nor simp closes the goal — the degree-addition proof term does not unify. exact Ext.mk₀_comp_mk₀ _ _ does. The same shape will recur anywhere Ext.comp is unfolded at a specific degree.

Main results

• extAdjunctionMap — the comparison, and extAdjunctionAddHom packaging its additivity.
• extAdjunctionMap_mk₀ — degree zero is the adjunction.
• extAdjunctionMap_comp, extAdjunctionMap_comp_mk₀, extAdjunctionMap_comp_extClass — the comparison is a morphism of the two long exact sequences.
• preservesInjectiveObjects_of_adj — R preserves injectives.
• bijective_extAdjunctionMap_of_injective — positive degree on an injective.
• surjective_extAdjunctionMap, injective_extAdjunctionMap, extAdjunctionAddEquiv — the additive theorem;
• extAdjunctionLinearMap, extAdjunctionLinearEquiv — its linear form when the right adjoint is linear.
• Abelian.Ext.precompAddEquiv, Abelian.Ext.precompLinearEquiv — transport along an isomorphism in the first variable, which a consumer needs whenever the comparison identifies that variable only up to isomorphism.

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

The comparison Ext^n (L A) B → Ext^n A (R B).

Push the class along R, then precompose with the unit of the adjunction. Both steps need R exact: Ext.mapExactFunctor is only defined for an exact functor.

Equations

• CategoryTheory.extAdjunctionMap adj e = (CategoryTheory.Abelian.Ext.mk₀ (adj.unit.app A)).comp (CategoryTheory.Abelian.Ext.mapExactFunctor R e) ⋯

@[simp]

theorem CategoryTheory.extAdjunctionMap_zero {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {B : D} {n : ℕ} : extAdjunctionMap adj 0 = 0

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

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

The comparison as an additive map, which is how the induction consumes it: the long exact sequences of Ext are sequences of additive groups, and a bare function does not map into them.

Equations

• CategoryTheory.extAdjunctionAddHom adj A B n = { toFun := CategoryTheory.extAdjunctionMap adj, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.extAdjunctionAddHom_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] (A : C) (B : D) (n : ℕ) (e : Abelian.Ext (L.obj A) B n) : (extAdjunctionAddHom adj A B n) e = extAdjunctionMap adj e

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

The comparison is natural in the second variable.

Post-composing before or after the comparison gives the same class. This is the lemma the induction step runs on: it is what makes the comparison a morphism of the two long exact sequences rather than a family of unrelated maps.

The proof is Ext.mapExactFunctor_comp followed by associativity — no exactness of the sequences and no injectivity is used, so it holds for arbitrary classes in arbitrary degrees.

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

Naturality against a morphism, the Ext.mk₀ case of extAdjunctionMap_comp.

This is the square for the two "easy" maps of the long exact sequences — the ones induced by S.f and S.g.

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

The connecting square.

The comparison commutes with the connecting class of a short exact sequence. R is exact, so it carries S to a short exact sequence in C, and Ext.mapExactFunctor_extClass says the connecting class goes along with it.

Together with extAdjunctionMap_comp_mk₀ this makes the comparison a morphism of the two long exact sequences, which is the entire structural input to the dimension-shifting induction.

theorem CategoryTheory.extAdjunctionMap_mk₀ {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {B : D} (f : L.obj A ⟶ B) : extAdjunctionMap adj (Abelian.Ext.mk₀ f) = Abelian.Ext.mk₀ ((adj.homEquiv A B) f)

In degree zero the comparison is the adjunction's hom-equivalence.

Stated in Ext.mk₀ form rather than through Ext.homEquiv₀, because that is the form the induction's base case needs and it avoids a round trip through the equivalence.

The proof is three rewrites and then exact, not simp — see the module docstring on Ext.mk₀_comp_mk₀.

theorem CategoryTheory.preservesInjectiveObjects_of_adj {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] : R.PreservesInjectiveObjects

A right adjoint whose left adjoint preserves monomorphisms preserves injectives.

Not an instance: adj is not inferrable from R alone, so instance search cannot find it. Every use is an explicit haveI.

theorem CategoryTheory.subsingleton_ext_right_of_injective {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [HasExt C] {A : C} {B : D} [Injective B] {n : ℕ} : Subsingleton (Abelian.Ext A (R.obj B) (n + 1))

The target vanishes in positive degree, because R B is injective.

theorem CategoryTheory.bijective_extAdjunctionMap_of_injective {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {A : C} {B : D} [Injective B] {n : ℕ} : Function.Bijective (extAdjunctionMap adj)

The comparison is bijective in positive degree on an injective.

Both sides are subsingletons — the source by Ext.subsingleton_of_injective directly, the target by subsingleton_ext_right_of_injective — so there is nothing to check. This is the base case the dimension shift descends to, and it is the only reason the induction terminates.

theorem CategoryTheory.bijective_extAdjunctionMap_zero {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] (A : C) (B : D) : Function.Bijective (extAdjunctionMap adj)

In degree zero the comparison is bijective: it is the adjunction hom-equivalence transported through Ext.mk₀.

theorem CategoryTheory.surjective_extAdjunctionMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] [EnoughInjectives D] (n : ℕ) (A : C) (B : D) : Function.Surjective (extAdjunctionMap adj)

The comparison is surjective in every degree.

This is surjective_extComparisonMap for u := adj.unit.app A: degree zero is the adjunction, and R I is injective for injective I (preservesInjectiveObjects_of_adj), hence acyclic.

theorem CategoryTheory.injective_extAdjunctionMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] [EnoughInjectives D] (n : ℕ) (A : C) (B : D) : Function.Injective (extAdjunctionMap adj)

The comparison is injective in every degree. Likewise a special case of injective_extComparisonMap.

noncomputable def CategoryTheory.extAdjunctionAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] [EnoughInjectives D] (A : C) (B : D) (n : ℕ) : Abelian.Ext (L.obj A) B n ≃+ Abelian.Ext A (R.obj B) n

Ext along an adjunction with exact left adjoint.

Ext^n (L A) B ≃+ Ext^n A (R B), for every n. This is the statement the cohomology comparison of #572 step 3 instantiates at L = ι⁻¹, R = ι_* for a closed immersion.

Equations

• CategoryTheory.extAdjunctionAddEquiv adj A B n = AddEquiv.ofBijective (CategoryTheory.extAdjunctionAddHom adj A B n) ⋯

@[simp]

theorem CategoryTheory.extAdjunctionAddEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] [EnoughInjectives D] (A : C) (B : D) (n : ℕ) (e : Abelian.Ext (L.obj A) B n) : (extAdjunctionAddEquiv adj A B n) e = extAdjunctionMap adj e

noncomputable def CategoryTheory.extAdjunctionLinearMap {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {S : Type t} [CommRing S] [Linear S C] [Linear S D] [Functor.Linear S R] (A : C) (B : D) (n : ℕ) : Abelian.Ext (L.obj A) B n →ₗ[S] Abelian.Ext A (R.obj B) n

The Ext comparison along a linear exact right adjoint is linear.

The scalar on an Ext class is postcomposition by the corresponding scalar endomorphism. The exact functor R carries scalar multiples to scalar multiples, and Ext composition is linear in the second variable.

Equations

• CategoryTheory.extAdjunctionLinearMap adj A B n = { toFun := (↑(CategoryTheory.extAdjunctionAddHom adj A B n)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CategoryTheory.extAdjunctionLinearMap_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {S : Type t} [CommRing S] [Linear S C] [Linear S D] [Functor.Linear S R] (A : C) (B : D) (n : ℕ) (a✝ : Abelian.Ext (L.obj A) B n) : (extAdjunctionLinearMap adj A B n) a✝ = (↑(extAdjunctionAddHom adj A B n)).toFun a✝

noncomputable def CategoryTheory.extAdjunctionLinearEquiv {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {S : Type t} [CommRing S] [Linear S C] [Linear S D] [Functor.Linear S R] [EnoughInjectives D] (A : C) (B : D) (n : ℕ) : Abelian.Ext (L.obj A) B n ≃ₗ[S] Abelian.Ext A (R.obj B) n

Linear Ext along an adjunction with exact left adjoint.

This is extAdjunctionAddEquiv with its canonical scalar compatibility exposed. Only the right adjoint must be linear: it is the functor applied to Ext classes in the comparison map.

Equations

• CategoryTheory.extAdjunctionLinearEquiv adj A B n = LinearEquiv.ofBijective (CategoryTheory.extAdjunctionLinearMap adj A B n) ⋯

@[simp]

theorem CategoryTheory.extAdjunctionLinearEquiv_apply {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) [L.Additive] [Limits.PreservesFiniteLimits L] [Limits.PreservesFiniteColimits L] [R.Additive] [Limits.PreservesFiniteLimits R] [Limits.PreservesFiniteColimits R] [HasExt C] [HasExt D] {S : Type t} [CommRing S] [Linear S C] [Linear S D] [Functor.Linear S R] [EnoughInjectives D] (A : C) (B : D) (n : ℕ) (e : Abelian.Ext (L.obj A) B n) : (extAdjunctionLinearEquiv adj A B n) e = extAdjunctionMap adj e

noncomputable def CategoryTheory.Abelian.Ext.precompAddEquiv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X X' : C} (e : X ≅ X') (B : C) (n : ℕ) : Ext X' B n ≃+ Ext X B n

Precomposition with an isomorphism is an isomorphism of Ext groups.

Not in Mathlib at the pin under any spelling, and needed the moment a comparison identifies the first variable up to isomorphism rather than on the nose — which is exactly what happens when the constant sheaf is carried across a pullback.

Equations

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

noncomputable def CategoryTheory.Abelian.Ext.precompLinearEquiv {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S : Type t} [CommRing S] [Linear S C] {X X' : C} (e : X ≅ X') (B : C) (n : ℕ) : Ext X' B n ≃ₗ[S] Ext X B n

Linear transport in the first variable of Ext along an isomorphism.

This is the scalar-compatible refinement of precompAddEquiv. The scalar action on Ext is linear in either argument of the Yoneda product, so precomposition with the degree-zero class of an isomorphism is linear.

Equations

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