Cohomology is unchanged by an exact pushforward

sheafHPushforwardAddEquiv : Hⁿ(K, F) ≃+ Hⁿ(J, G_* F), for a continuous G whose pullback and pushforward are both exact. This is #572 step 3 — cohomology invariance along a closed immersion — with the geometry replaced by the two hypotheses that actually carry the argument.

The three pieces, and where each came from

Sheaf.H F n is Ext ((constantSheaf J _).obj (ULift ℤ)) F n, so the comparison is an Ext transport and not a Čech computation. It assembles from exactly two results and nothing else:

• constantSheafCompSheafPullbackIso (ConstantPullback.lean) moves the constant sheaf across G⁻¹ ⊣ G_*, giving G⁻¹ ℤ_J ≅ ℤ_K;
• extAdjunctionAddEquiv (ExtAdjunction.lean) transports Ext across that same adjunction;
• Ext.precompAddEquiv glues the two, because the first supplies an isomorphism rather than an equality of first arguments.

The body is one .trans. Everything hard happened in the two files it cites.

Three traps, all of them costing real time, none of them mathematics

The Abelian hypothesis is a diamond, and it was the actual blocker. Writing [Abelian (Sheaf J AddCommGrpCat.{w})] as a variable puts a second Preadditive structure on a category that already has one: the hypothesis carries Abelian.toPreadditive, while the ambient instance is Preadditive.fullSubcategory (Presheaf.IsSheaf J). Functor.Additive is stated against Preadditive, so (G.sheafPullback _ J K).Additive then fails to synthesize even when the hypothesis is named, included and haveI'd — the two spellings are not reducibly equal. The fix is to assume nothing: with HasSheafify and the imports below, sheafIsAbelian is found and there is only one Preadditive. Same family as #662.

HasSheafify, not HasWeakSheafify. sheafIsAbelian needs the former; with only the latter the Abelian instance is genuinely absent rather than duplicated.

The Sites.Abelian and Grp.Abelian imports are load-bearing. Neither ConstantPullback.lean nor ExtAdjunction.lean reaches them, and without them Abelian (Sheaf J AddCommGrpCat) is not inferrable — which reads exactly like a missing mathematical input and is not one.

A correction, recorded because the wrong diagnosis was written down first

An earlier pass concluded that stating this against Sheaf.H was itself the problem — it produced a synthInstance failure at 20k heartbeats and, raised to 1M, an isDefEq timeout after 4m24s — and that the cure was to state everything in Ext and relegate Sheaf.H to a rfl-lemma. That was wrong. The timeout was the diamond above, surfacing at the only place that forced the two Preadditive structures to meet. With the diamond gone, the Sheaf.H form elaborates in seconds and is stated directly, as #572 asks. The Ext form is kept because it is the reusable one, not because Sheaf.H needs avoiding.

Scope

Both exactness hypotheses are real and neither is decoration. G_* is exact for a closed immersion, which is the intended application, but it is only left exact in general — a caller with a general continuous map gets nothing from this file. EnoughInjectives is what extAdjunctionAddEquiv needs.

Main results

• sheafCohomologyPushforwardAddEquiv — the Ext form.
• sheafH_eq_ext — Sheaf.H is that Ext, definitionally.
• sheafHPushforwardAddEquiv — the cohomology form, which is #572 step 3's statement.

noncomputable def CategoryTheory.sheafCohomologyPushforwardAddEquiv {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} (G : Functor C D) [G.IsContinuous J K] [HasSheafify J AddCommGrpCat] [HasSheafify K AddCommGrpCat] [HasGlobalSectionsFunctor J AddCommGrpCat] [HasGlobalSectionsFunctor K AddCommGrpCat] [∀ (F : Functor Cᵒᵖ AddCommGrpCat), G.op.HasLeftKanExtension F] [Limits.HasTerminal C] [Limits.HasTerminal D] [HasExt (Sheaf J AddCommGrpCat)] [HasExt (Sheaf K AddCommGrpCat)] [hLa : (G.sheafPullback AddCommGrpCat J K).Additive] [hLl : Limits.PreservesFiniteLimits (G.sheafPullback AddCommGrpCat J K)] [hLc : Limits.PreservesFiniteColimits (G.sheafPullback AddCommGrpCat J K)] [hRa : (G.sheafPushforwardContinuous AddCommGrpCat J K).Additive] [hRl : Limits.PreservesFiniteLimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hRc : Limits.PreservesFiniteColimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hInj : EnoughInjectives (Sheaf K AddCommGrpCat)] (hG : Limits.IsTerminal (G.obj (⊤_ C))) (F : Sheaf K AddCommGrpCat) (n : ℕ) : Abelian.Ext ((constantSheaf K AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{w, 0} ℤ))) F n ≃+ Abelian.Ext ((constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{w, 0} ℤ))) ((G.sheafPushforwardContinuous AddCommGrpCat J K).obj F) n

Cohomology transports along an exact pushforward, in Ext form.

Ext.precompAddEquiv absorbs the isomorphism G⁻¹ ℤ_J ≅ ℤ_K; extAdjunctionAddEquiv does the transport. The Ext spelling is the reusable one — a caller who wants to compose this with other Ext machinery should not have to unfold Sheaf.H first.

Equations

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

theorem CategoryTheory.sheafH_eq_ext {D : Type u} [Category.{v, u} D] {K : GrothendieckTopology D} [HasSheafify K AddCommGrpCat] [HasExt (Sheaf K AddCommGrpCat)] (F : Sheaf K AddCommGrpCat) (n : ℕ) : F.H n = Abelian.Ext ((constantSheaf K AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{w, 0} ℤ))) F n

Sheaf cohomology is that Ext, by definition of Sheaf.H. Recorded so a reader can see that the two statements below are the same one, not a transport between them.

noncomputable def CategoryTheory.sheafHPushforwardAddEquiv {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} (G : Functor C D) [G.IsContinuous J K] [HasSheafify J AddCommGrpCat] [HasSheafify K AddCommGrpCat] [HasGlobalSectionsFunctor J AddCommGrpCat] [HasGlobalSectionsFunctor K AddCommGrpCat] [∀ (F : Functor Cᵒᵖ AddCommGrpCat), G.op.HasLeftKanExtension F] [Limits.HasTerminal C] [Limits.HasTerminal D] [HasExt (Sheaf J AddCommGrpCat)] [HasExt (Sheaf K AddCommGrpCat)] [hLa : (G.sheafPullback AddCommGrpCat J K).Additive] [hLl : Limits.PreservesFiniteLimits (G.sheafPullback AddCommGrpCat J K)] [hLc : Limits.PreservesFiniteColimits (G.sheafPullback AddCommGrpCat J K)] [hRa : (G.sheafPushforwardContinuous AddCommGrpCat J K).Additive] [hRl : Limits.PreservesFiniteLimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hRc : Limits.PreservesFiniteColimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hInj : EnoughInjectives (Sheaf K AddCommGrpCat)] (hG : Limits.IsTerminal (G.obj (⊤_ C))) (F : Sheaf K AddCommGrpCat) (n : ℕ) : F.H n ≃+ ((G.sheafPushforwardContinuous AddCommGrpCat J K).obj F).H n

Hⁿ(K, F) ≃+ Hⁿ(J, G_* F).

#572 step 3's statement. The HasExt universe stays a parameter, as that issue asks, and the Sheaf.H spelling costs nothing over the Ext one — see the module docstring, which records why an earlier pass believed otherwise.

Equations

• CategoryTheory.sheafHPushforwardAddEquiv G hG F n = CategoryTheory.sheafCohomologyPushforwardAddEquiv G hG F n

theorem CategoryTheory.sheafHPushforwardAddEquiv_naturality {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} (G : Functor C D) [G.IsContinuous J K] [HasSheafify J AddCommGrpCat] [HasSheafify K AddCommGrpCat] [HasGlobalSectionsFunctor J AddCommGrpCat] [HasGlobalSectionsFunctor K AddCommGrpCat] [∀ (F : Functor Cᵒᵖ AddCommGrpCat), G.op.HasLeftKanExtension F] [Limits.HasTerminal C] [Limits.HasTerminal D] [HasExt (Sheaf J AddCommGrpCat)] [HasExt (Sheaf K AddCommGrpCat)] [hLa : (G.sheafPullback AddCommGrpCat J K).Additive] [hLl : Limits.PreservesFiniteLimits (G.sheafPullback AddCommGrpCat J K)] [hLc : Limits.PreservesFiniteColimits (G.sheafPullback AddCommGrpCat J K)] [hRa : (G.sheafPushforwardContinuous AddCommGrpCat J K).Additive] [hRl : Limits.PreservesFiniteLimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hRc : Limits.PreservesFiniteColimits (G.sheafPushforwardContinuous AddCommGrpCat J K)] [hInj : EnoughInjectives (Sheaf K AddCommGrpCat)] (hG : Limits.IsTerminal (G.obj (⊤_ C))) {F F' : Sheaf K AddCommGrpCat} (φ : F ⟶ F') (n : ℕ) (x : F.H n) : (sheafHPushforwardAddEquiv G hG F' n) ((Sheaf.H.map φ n) x) = (Sheaf.H.map ((G.sheafPushforwardContinuous AddCommGrpCat J K).map φ) n) ((sheafHPushforwardAddEquiv G hG F n) x)

The comparison is natural in the sheaf. Both sides are Ext composites: the induced map on cohomology is postcomposition with mk₀ φ, which extAdjunctionMap_comp_mk₀ carries across the adjunction transport and associativity carries across the precomposition with the constant-sheaf isomorphism.