Isomorphism invariance of coherent sheaves

Finite presentation is invariant under isomorphism on an arbitrary ringed site by Algebra.Category.ModuleCat.Sheaf.Presentation.Isomorphism. This geometric consumer records that coherent sheaves on a scheme are therefore closed under isomorphisms in the ambient category of sheaves of modules.

instance AlgebraicGeometry.Scheme.coherent_isClosedUnderIsomorphisms (X : Scheme) : X.coherent.IsClosedUnderIsomorphisms

Coherent sheaves on X are closed under isomorphisms in X.Modules.