Fixed-target arrows on affine basic opens

For a noetherian affine scheme, every arrow into the restriction of a fixed coherent sheaf to D(r) extends from some coherent sheaf on the ambient affine scheme, up to an isomorphism on its source. The proof transports the affine localization theorem across the coherent pullback equivalence induced by basicOpenIsoSpecAway r.

This is an underived arrow theorem for one basic open. It does not assert that the extended arrow is monic or construct a global extension across a quasi-compact open in a general scheme.

theorem AlgebraicGeometry.Coh.fixedTargetArrowExtension_pullbackBasicOpen {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (E : Coh (Spec R)) : CategoryTheory.Subobject.FixedTargetArrowExtension (pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))) E

Fixed-target arrow extension for coherent sheaves along the actual basic-open immersion D(r) ↪ Spec R. The target E stays fixed, and only the arrow's source is replaced by an isomorphic coherent pullback. This is ordinary coherent pullback, not a derived arrow.