∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules) {f g : (↑R)ᵒᵖ} (i : f ⟶ g),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp
            (AlgebraicGeometry.modulesSpecToSheaf.obj
                (AlgebraicGeometry.tilde
                  ((AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)))).obj).map
        i)
      (ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (Opposite.unop g))
          (ModuleCat.Hom.hom
            (AlgebraicGeometry.tilde.toOpen ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.obj (Opposite.op ⊤))
              (PrimeSpectrum.basicOpen (Opposite.unop g))))
          (ModuleCat.Hom.hom ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op)) ⋯)) =
    CategoryTheory.CategoryStruct.comp
      (ModuleCat.ofHom
        (IsLocalizedModule.lift (Submonoid.powers (Opposite.unop f))
          (ModuleCat.Hom.hom
            (AlgebraicGeometry.tilde.toOpen ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.obj (Opposite.op ⊤))
              (PrimeSpectrum.basicOpen (Opposite.unop f))))
          (ModuleCat.Hom.hom ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op)) ⋯))
      (((CategoryTheory.inducedFunctor PrimeSpectrum.basicOpen).op.comp
            (AlgebraicGeometry.modulesSpecToSheaf.obj M).obj).map
        i)