Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Modules.restrictAppIso

{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (M : Y.Modules) →
        (U : X.Opens) →
          (M.restrict f).presheaf.obj (Opposite.op U) ≅
            M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))

The sections of the restriction of M over U are isomorphic to `Γ(M, f ''ᵁ U).

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

14 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion