Exact direct image for a closed immersion

Mathematical statement

Let $i:Z\hookrightarrow X$ be a closed immersion of schemes and let $R$ be a commutative ring. For every short exact sequence of sheaves of $R$-modules on $Z_{\mathrm{et}}$, $$0\longrightarrow A\longrightarrow B\longrightarrow C\longrightarrow0,$$ direct image gives a short exact sequence $$0\longrightarrow i_*A\longrightarrow i_*B\longrightarrow i_*C\longrightarrow0$$ on $X_{\mathrm{et}}$.

The coefficient ring is fixed independently of the schemes. These are étale sheaves of modules, with no quasi-coherence, finite-generation, torsion, or noetherian hypothesis.

Lean code

`EtaleCohomology.etalePushforwardClosed_shortExact`

Published library source ↗Same source in NYLL ↗

lemma etalePushforwardClosed_shortExact
    (S : ShortComplex (Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) : (S.map (etalePushforward i R)).ShortExact

In-scope Lean context

noncomputable section

universe u

open AlgebraicGeometry CategoryTheory Limits

namespace EtaleCohomology

variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Full declaration and proof

/-- Direct image along a closed immersion preserves short exact sequences. -/
lemma etalePushforwardClosed_shortExact
    (S : ShortComplex (Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) : (S.map (etalePushforward i R)).ShortExact := by
  classical
  apply (shortExact_iff_residueStalk X R _).mpr
  intro x
  let tx : Spec (.of (SeparableClosure (X.residueField x))) ⟶ X :=
    (Scheme.SpecToEquivOfField (SeparableClosure (X.residueField x)) X).symm
      ⟨x, CommRingCat.ofHom (algebraMap (X.residueField x) _)⟩
  let z : Spec (.of (SeparableClosure (X.residueField x))) := Classical.choice inferInstance
  change (S.map (etalePushforward i R ⋙ (Scheme.pointSmallEtale tx).sheafFiber)).ShortExact
  by_cases h : tx z ∈ Set.range i
  · have hrange : Set.range tx ⊆ Set.range i := by
      rintro y ⟨a, rfl⟩
      rwa [Subsingleton.elim a z]
    obtain ⟨r, hr⟩ := IsClosedImmersion.exists_lift_of_isReduced_of_range_subset i tx hrange
    rw [← hr]
    exact ShortComplex.shortExact_of_iso
      (S.mapNatIso (etalePushforwardClosedStalkIso i r R).symm)
      (hS.map_of_exact (Scheme.pointSmallEtale r).sheafFiber)
  · exact
      { exact := ShortComplex.exact_of_isZero_X₂ _
          (etalePushforward_stalk_isZero_of_not_mem_range i R tx z h S.X₂)
        mono_f := (etalePushforward_stalk_isZero_of_not_mem_range i R tx z h S.X₁).mono _
        epi_g := (etalePushforward_stalk_isZero_of_not_mem_range i R tx z h S.X₃).epi _ }

Source credits and license

Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

The Stacks Project Authors. Section 59.46: Closed immersions and pushforward. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.