New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebraic_geometry): Lift isomorphism of sheafed spaces to locally ringed spaces #8887
Conversation
…unity/mathlib into split_local_ring
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors d+
Unfortunately, this equality is not well-formed, as their types are not _definitionally_ the same. | ||
To get a proper congruence lemma, we therefore have to introduce these `eq_to_hom` arrows on | ||
either side of the equality. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is quite unfortunate. But I don't see a better solution atm.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it took me some time to get used to all the eq_to_homs involved... But now I think it's not so bad after all.
✌️ justus-springer can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
…m/leanprover-community/mathlib into locally_ringed_space_reflects_iso
bors r+ |
…ly 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. Co-authored-by: justus-springer <50165510+justus-springer@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
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.This PR will be used to lift the isomorphism
restrict_top_iso
from the level of presheafed spaces to the level of locally ringed spaces. This is needed to complete the redefinition of Schemes (see #8888).