Module

ProperHenselianSheafRestriction.lean

Nyll.SchemeTheory.Morphisms.ProperHenselianSheafRestriction

1 declaration indexed from sourceView source ↗

Module documentation

Sheaf sections on a proper henselian closed fiber

Every sheaf of sets on the underlying space of an arbitrary proper scheme over a henselian local ring has the same global sections on its actual closed fiber. The map is the unit of the topological inverse-image adjunction. Connected point-closure intersections come from proper henselian geometry, and the spectral restriction theorem applies directly.

Imports7

Nyll.SchemeTheory.Morphisms.ProperHenselianClosedRestriction
Nyll.SchemeTheory.Topology.SpectralClosedSheafRestriction
Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Mathlib.AlgebraicGeometry.Properties
Mathlib.RingTheory.Henselian
Mathlib.Topology.Sheaves.Functors

Imported by2

theorem

sheaf_closedFiber_restriction_bijective

L36 ↗

AlgebraicGeometry.sheaf_closedFiber_restriction_bijective

Documentation

The actual closed-fiber restriction on global sections is bijective for every topological sheaf on a proper scheme over a henselian local ring.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry

Lean source · statement

theorem sheaf_closedFiber_restriction_bijective
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) [IsProper f]
    (F : CategoryTheory.Sheaf (Opens.grothendieckTopology X) (Type u)) :
    Function.Bijective
      (((TopCat.Sheaf.pullbackPushforwardAdjunction (Type u)
        (TopCat.ofHom
          (⟨Subtype.val, continuous_subtype_val⟩ :
            C(TopCat.of (f ⁻¹' {IsLocalRing.closedPoint R}), TopCat.of X)))).unit.app F).hom.app
        (op (⊤ : Opens X)))

Module documentation

Sheaf sections on a proper henselian closed fiber

Declarations

sheaf_closedFiber_restriction_bijective