Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-29 14:08 395bb6ca

View on Github →

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.

Estimated changes