Coherent subobject order is local on an open cover

Restriction to any open cover of a locally Noetherian scheme reflects order and equality between coherent subobjects of one fixed coherent sheaf. The required finite-limit preservation of Coh.restrict is established only inside the order proof. No local subobject is extended or glued here.

theorem AlgebraicGeometry.Coh.subobject_le_iff_restrict_openCover {U : Scheme} [IsLocallyNoetherian U] (𝒰 : U.OpenCover) (E : Coh U) (P Q : CategoryTheory.Subobject E) : P ≤ Q ↔ ∀ (i : 𝒰.I₀), CategoryTheory.Subobject.mapFunctor (restrict (𝒰.f i)) P ≤ CategoryTheory.Subobject.mapFunctor (restrict (𝒰.f i)) Q

An open cover detects order between existing coherent subobjects of E. The cover need not be finite.

theorem AlgebraicGeometry.Coh.subobject_eq_iff_restrict_openCover {U : Scheme} [IsLocallyNoetherian U] (𝒰 : U.OpenCover) (E : Coh U) (P Q : CategoryTheory.Subobject E) : P = Q ↔ ∀ (i : 𝒰.I₀), CategoryTheory.Subobject.mapFunctor (restrict (𝒰.f i)) P = CategoryTheory.Subobject.mapFunctor (restrict (𝒰.f i)) Q

Equality of existing coherent subobjects is local on an open cover.