Classifying coherent subobjects on one affine basic open

An arbitrary coherent mono into the restriction of E to D(r) is, up to an isomorphism on its source, the restriction of the tilde inclusion associated to a finitely generated submodule of the affine global sections of E. The explicit chart comparison identifies that inclusion with localization of the chosen submodule. This is underived and does not glue across opens.

theorem AlgebraicGeometry.Coh.exists_tilde_subobject_pullbackBasicOpen {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (Z : Coh ↑(PrimeSpectrum.basicOpen r)) (β : Z ⟶ (pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj E) [CategoryTheory.Mono β] : let FR := FGModuleCat.affineTilde; let G := pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r)); ∃ (N : Submodule ↑R ↑M.obj) (hN : N.FG), let K := FGModuleCat.of ↑R ↥N; have g := FGModuleCat.ofHom N.subtype; have f := CategoryTheory.CategoryStruct.comp (FR.map g) cR.inv; (∃ (e : Z ≅ G.obj (FR.obj K)), β = CategoryTheory.CategoryStruct.comp e.hom (G.map f)) ∧ ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (basicOpenCoherentSubobject r M E cR N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

Every coherent mono on the actual basic open is the restriction, up to a source isomorphism, of the coherent tilde inclusion of a finite submodule of the chosen module presentation of E. The transported chart subobject is its canonical localization.

theorem AlgebraicGeometry.Coh.exists_coherentTildeSubobject_pullbackBasicOpen {R : CommRingCat} [IsNoetherianRing ↑R] (r : ↑R) (M : FGModuleCat ↑R) (E : Coh (Spec R)) (cR : E ≅ FGModuleCat.affineTilde.obj M) (Z : Coh ↑(PrimeSpectrum.basicOpen r)) (β : Z ⟶ (pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r))).obj E) [CategoryTheory.Mono β] : let G := pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r)); ∃ (N : Submodule ↑R ↑M.obj) (hN : N.FG), have P := coherentTildeSubobject M E cR N hN; (∃ (e : Z ≅ G.obj (CategoryTheory.Subobject.underlying.obj P)), β = CategoryTheory.CategoryStruct.comp e.hom (G.map P.arrow)) ∧ ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (basicOpenCoherentSubobject r M E cR N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

Every prescribed mono on D(r) is the restriction of the actual coherent tilde subobject of a finite submodule. The chart module subobject, with target transported by basicOpenGlobalSectionsIso, is N.localized'.

theorem AlgebraicGeometry.Coh.exists_coherentTildeSubobject_pullbackBasicOpen_globalSections {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 β] : let ER := affineEquivalence; let M := ER.functor.obj E; let G := pullback (Scheme.Opens.ι (PrimeSpectrum.basicOpen r)); ∃ (N : Submodule ↑R ↑M.obj) (hN : N.FG), have P := coherentTildeSubobject M E (ER.unitIso.app E) N hN; (∃ (e : Z ≅ G.obj (CategoryTheory.Subobject.underlying.obj P)), β = CategoryTheory.CategoryStruct.comp e.hom (G.map P.arrow)) ∧ ((ModuleCat.localizedModuleFunctor (Submonoid.powers r)).obj M.obj).subobjectModule (basicOpenCoherentSubobject r M E (ER.unitIso.app E) N hN) = Submodule.localized' (Localization.Away r) (Submonoid.powers r) (M.obj.localizedModuleMkLinearMap (Submonoid.powers r)) N

Canonical M = Γ(E) specialization of the one-chart classification. No presentation or ring action equality is left for the caller to choose.