{R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {S : Type u} →
          [inst_3 : CommRing S] →
            {N : Type u} →
              [inst_4 : AddCommGroup N] →
                [inst_5 : Module S N] →
                  {σ : R →+* S} →
                    (M →ₛₗ[σ] N) →
                      (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
                        (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                          V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier →
                            ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x) →
                              (y : ↥V) → AlgebraicGeometry.StructureSheaf.Localizations N ↑y