∀ {R S : CommRingCat} (f : R ⟶ S) {U : (AlgebraicGeometry.Spec S).Opens} {V : (AlgebraicGeometry.Spec R).Opens}
  (e : U ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.map f).base).obj V),
  AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Spec.map f) V U e =
    CommRingCat.ofHom (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) V U e)