Being an isomorphism is local at the target

theorem AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective : CategoryTheory.MorphismProperty.isomorphisms Scheme = @IsOpenImmersion ⊓ @Surjective

theorem AlgebraicGeometry.isomorphisms_eq_stalkwise : CategoryTheory.MorphismProperty.isomorphisms Scheme = (CategoryTheory.MorphismProperty.isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓ stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => Function.Bijective ⇑f

instance AlgebraicGeometry.instIsLocalAtTargetIsomorphismsScheme : IsLocalAtTarget (CategoryTheory.MorphismProperty.isomorphisms Scheme)

instance AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop : HasAffineProperty (CategoryTheory.MorphismProperty.isomorphisms Scheme) fun (X x : Scheme) (f : X ⟶ x) (x_1 : IsAffine x) => IsAffine X ∧ CategoryTheory.IsIso (Scheme.Hom.appTop f)

instance AlgebraicGeometry.instIsLocalAtTargetMonomorphismsScheme : IsLocalAtTarget (CategoryTheory.MorphismProperty.monomorphisms Scheme)