∀ {R : CommRingCat} (M : ModuleCat ↑R) (U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R))
  (i : V ⟶ U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.tilde.toOpen M U)
      ((AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.map i.op) =
    AlgebraicGeometry.tilde.toOpen M V