Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (x : ↥X) →
        (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).comp
            ((AlgebraicGeometry.Scheme.Modules.toPresheaf X).comp (TopCat.Presheaf.stalkFunctor Ab x)) ≅
          (AlgebraicGeometry.Scheme.Modules.toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor Ab (f x))

Restriction along open immersions commutes with taking stalks.

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsOpenImmersion