∀ {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} (f : M →ₛₗ[σ] N)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier) (a : M) (b : R) (hb : U ≤ PrimeSpectrum.basicOpen b),
  (AlgebraicGeometry.StructureSheaf.comapₗ f U V hUV) (AlgebraicGeometry.StructureSheaf.const a b U hb) =
    AlgebraicGeometry.StructureSheaf.const (f a) (σ b) V ⋯