Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Modules.overMapCompOverEquiv

{X : AlgebraicGeometry.Scheme} →
  {U V : X.Opens} →
    (f : V ⟶ U) →
      (SheafOfModules.overMap X.ringCatSheaf f).comp (AlgebraicGeometry.Scheme.Modules.overEquiv V).functor ≅
        (AlgebraicGeometry.Scheme.Modules.overEquiv U).functor.comp
          (AlgebraicGeometry.Scheme.Modules.restrictFunctor (X.homOfLE ⋯))

Up to Scheme.Modules.overEquiv, SheafOfModules.overMap is isomorphic to Scheme.Modules.restrictFunctor.

Defined in

Mathlib.AlgebraicGeometry.Modules.Sheaf

Cited by

0 results in Mathlib

Foundations

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