Coherent subobjects on affine basic opens

A monomorphism into the pullback of a fixed coherent sheaf along D(r) ↪ Spec R is, up to an isomorphism on its source, the pullback of an actual coherent monomorphism into the fixed sheaf. The construction takes the image of the underived fixed-target arrow witness. Exactness of open restriction identifies that image after pullback.

This is a theorem for one affine basic open, not a gluing theorem for a quasi-compact open in an arbitrary scheme.

theorem AlgebraicGeometry.Coh.exists_mono_lift_pullbackBasicOpen {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (E : Coh (Spec R)) (Z : Coh ↑(PrimeSpectrum.basicOpen r)) (β : Z ⟶ (pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj E) [CategoryTheory.Mono β] : ∃ (L : Coh (Spec R)) (m : L ⟶ E), CategoryTheory.Mono m ∧ ∃ (e : Z ≅ (pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj L), β = CategoryTheory.CategoryStruct.comp e.hom ((pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).map m)

Every coherent subobject of the restriction of E to the actual basic open D(r) lifts to a coherent subobject of E. In contrast to a FixedTargetMonoExtension witness, the upstairs arrow m is itself monic.