Being an isomorphism is local at the target

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

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

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

Equations

• AlgebraicGeometry.instIsLocalAtTargetIsomorphismsScheme = ⋯

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

Equations

• AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTopOpens = ⋯