Commit 2021-08-29 14:08 395bb6ca

feat(algebraic_geometry): Lift isomorphism of sheafed spaces to locally ringed spaces (#8887) Adds the fact that an isomorphism of sheafed spaces can be lifted to an isomorphism of locally ringed spaces. The main ingredient is the fact that stalk maps of isomorphisms are again isomorphisms. In particular, this implies that the forgetful functor LocallyRingedSpace ⥤ SheafedSpace CommRing reflects isomorphisms.