Degree-zero proper base change over a henselian local ring

Mathematical statement

Let $R$ be a henselian local ring with residue field $\kappa$, let $f:X\to\operatorname{Spec}R$ be proper, and write $i:X_\kappa\to X$ for the closed-fiber inclusion. For any commutative coefficient ring $\Lambda$ and any étale sheaf $F$ of $\Lambda$-modules on $X$, restriction is bijective: $$H^0(X_{\mathrm{et}},F)\xrightarrow{\;\sim\;}H^0((X_\kappa)_{\mathrm{et}},i^*F).$$

No noetherianity or torsion condition is imposed. Only degree zero is asserted here, so these cohomology groups are global sections.

Lean code

`EtaleCohomology.etaleClosedFiber_globalSections_bijective`

Published library source ↗Same source in NYLL ↗

theorem etaleClosedFiber_globalSections_bijective
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    let r : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ Spec (CommRingCat.of R) :=
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))
    let i : pullback f r ⟶ X := pullback.fst f r
    Function.Bijective (etalePullbackGlobalSectionsMap i Λ F) := by
  intro r i
  rw [← etalePullbackGlobalSectionsMap_eq_unit]
  exact (ConcreteCategory.bijective_of_isIso
    (etalePushforwardGlobalSectionsIso i Λ ((etalePullback i Λ).obj F)).hom).comp
      (etaleClosedFiber_unit_globalSections_bijective R f Λ F)

In-scope Lean context

noncomputable section

universe u

open AlgebraicGeometry CategoryTheory Limits Opposite

namespace EtaleCohomology

Full declaration and proof

/-- Restriction to the actual closed fiber is bijective on étale H⁰ for every
module sheaf on a proper scheme over a henselian local ring. -/
theorem etaleClosedFiber_globalSections_bijective
    (R : Type u) [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (Λ : Type u) [CommRing Λ] (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} Λ)) :
    let r : Spec (CommRingCat.of (IsLocalRing.ResidueField R)) ⟶ Spec (CommRingCat.of R) :=
      Spec.map (CommRingCat.ofHom (IsLocalRing.residue R))
    let i : pullback f r ⟶ X := pullback.fst f r
    Function.Bijective (etalePullbackGlobalSectionsMap i Λ F) := by
  intro r i
  rw [← etalePullbackGlobalSectionsMap_eq_unit]
  exact (ConcreteCategory.bijective_of_isIso
    (etalePushforwardGlobalSectionsIso i Λ ((etalePullback i Λ).obj F)).hom).comp
      (etaleClosedFiber_unit_globalSections_bijective R f Λ F)

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.91: The proper base change theorem. 2026. Living reference; consulted 15 October 2026. The tag is the stable identifier.