Cohomology is unchanged by pushforward along a closed embedding

cohomologyPushforwardAddEquiv : Hⁿ(X, F) ≃+ Hⁿ(Y, f_* F) for f an inducing map with closed range. This is #572 step 3's statement, instantiated at an actual map of spaces.

Everything here is plumbing

CategoryTheory/Sites/Sheaves/CohomologyPushforward.lean proves the comparison abstractly, for a continuous functor of sites whose pullback and pushforward are both exact. This composition-layer file discharges those hypotheses for Opens.map f. No mathematics happens: the one non-formal input, exactness of f_*, is PushforwardStalks.lean, and the rest is instance supply.

That was not obvious in advance and it is worth recording why. Three separate estimates of this step were wrong, each in the same direction:

• the site bridge is rfl. TopCat.Sheaf.pushforward C f is defined as (Opens.map f).sheafPushforwardContinuous _ _ _, so the topological and site-level functors are the same term. Nothing is transported.
• EnoughInjectives and HasExt are imports, not theorems. Both follow from IsGrothendieckAbelian, which holds for Sheaf D X once Topology.Sheaves.Abelian and Grp.AB are in scope. A missing import here presents as a bare "failed to synthesize", which is indistinguishable from a missing result.
• HasGlobalSectionsFunctor and the left Kan extension are already instances for Opens.map.

What must be supplied by hand, and why

Four instances that exist but that search will not find or cannot afford:

• PreservesFiniteLimits of the pullback. The instance is Functor.sheafPullbackConstruction.preservesFiniteLimits; searching for it instead runs whnf past 200000 heartbeats while unifying through site functors. Name it.
• Additive of the pushforward — rfl per morphism, but not found.
• Additive of the pullback — from the pushforward's, through Adjunction.left_adjoint_additive.
• IsLeftAdjoint/IsRightAdjoint of the two, to get the remaining exactness halves.

⊤_ is not ⊤

The abstract theorem wants IsTerminal ((Opens.map f).obj (⊤_ (Opens Y))). Opens.map sends ⊤ to ⊤ by rfl, but the categorical terminal ⊤_ (Opens Y) is not syntactically the lattice ⊤; terminal_opens_eq_top is the one-line antisymmetry that identifies them, and IsTerminal.ofUnique does not discharge the goal without it.

Scope

Spaces, not schemes. A closed immersion of schemes induces a closed embedding of underlying spaces, so this applies to one — but that final step is not taken here, and #572's acceptance criterion is phrased about schemes.

Main results

• cohomologyPushforwardAddEquivAt — the comparison, at a chosen HasExt witness.
• cohomologyPushforwardAddEquivAt_naturality — it is natural in the sheaf.
• cohomologyPushforwardAddEquiv — the same at the witness instance search finds.

noncomputable def DerivedAlgGeo.Topology.isTerminalTopOpens {X : TopCat} : CategoryTheory.Limits.IsTerminal ⊤

⊤ is terminal in Opens: morphisms are proofs of ≤, so le_top is the unique one.

Equations

• DerivedAlgGeo.Topology.isTerminalTopOpens = CategoryTheory.Limits.IsTerminal.ofUniqueHom (fun (x : TopologicalSpace.Opens ↑X) => CategoryTheory.homOfLE ⋯) ⋯

theorem DerivedAlgGeo.Topology.terminal_opens_eq_top {Y : TopCat} : (⊤_ TopologicalSpace.Opens ↑Y) = ⊤

The categorical terminal of Opens is the lattice ⊤. Needed because the two are not syntactically equal and the abstract theorem asks about the former.

noncomputable def DerivedAlgGeo.Topology.isTerminalOpensMapTerminal {X Y : TopCat} (f : X ⟶ Y) : CategoryTheory.Limits.IsTerminal ((TopologicalSpace.Opens.map f).obj (⊤_ TopologicalSpace.Opens ↑Y))

Opens.map f carries the categorical terminal open of Y to a terminal open of X: it sends ⊤ to ⊤. Named, because it is data that the comparison and its naturality statement have to share.

Equations

• DerivedAlgGeo.Topology.isTerminalOpensMapTerminal f = ⋯.mpr (⋯.mpr DerivedAlgGeo.Topology.isTerminalTopOpens)

noncomputable def DerivedAlgGeo.Topology.cohomologyPushforwardAddEquivAt {X Y : TopCat} (f : X ⟶ Y) (hemb : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (hcl : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))) (hX : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)) (hY : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat)) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (n : ℕ) : F.H n ≃+ (((TopologicalSpace.Opens.map f).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).obj F).H n

Cohomology is unchanged by pushforward along a closed embedding, at a chosen HasExt witness.

#572 step 3, at a map of spaces. Every hypothesis of the abstract comparison is discharged here; the only one that is not an instance or an import is exactness of f_*, which is preservesFiniteColimits_pushforward.

The HasExt witnesses are positional, as in the Čech lane: Sheaf.H lands in the HasExt universe, and a caller whose groups are named at HasExt.standard (the coherent-cohomology convention, HasExt.{u + 1}) cannot let instance search pick the Grothendieck-category HasExt.{u}, which names different groups.

Equations

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

theorem DerivedAlgGeo.Topology.cohomologyPushforwardAddEquivAt_naturality {X Y : TopCat} (f : X ⟶ Y) (hemb : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (hcl : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))) (hX : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)) (hY : CategoryTheory.HasExt (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑Y) AddCommGrpCat)) {F F' : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (φ : F ⟶ F') (n : ℕ) (x : F.H n) : (cohomologyPushforwardAddEquivAt f hemb hcl hX hY F' n) ((CategoryTheory.Sheaf.H.map φ n) x) = (CategoryTheory.Sheaf.H.map (((TopologicalSpace.Opens.map f).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).map φ) n) ((cohomologyPushforwardAddEquivAt f hemb hcl hX hY F n) x)

The comparison is natural in the sheaf. The abstract naturality sheafHPushforwardAddEquiv_naturality, at the same instances and the same terminal witness.

noncomputable def DerivedAlgGeo.Topology.cohomologyPushforwardAddEquiv {X Y : TopCat} (f : X ⟶ Y) (hemb : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (hcl : IsClosed (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f))) (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (n : ℕ) : F.H n ≃+ (((TopologicalSpace.Opens.map f).sheafPushforwardContinuous AddCommGrpCat (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)).obj F).H n

Cohomology is unchanged by pushforward along a closed embedding, at the HasExt witness instance search finds.

Equations

• DerivedAlgGeo.Topology.cohomologyPushforwardAddEquiv f hemb hcl F n = DerivedAlgGeo.Topology.cohomologyPushforwardAddEquivAt f hemb hcl ⋯ ⋯ F n