-
Notifications
You must be signed in to change notification settings - Fork 297
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/morphisms): Basic framework for classes of morphisms between schemes #14944
Conversation
erdOne
commented
Jun 25, 2022
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.
looks nice!
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
…-community/mathlib into scheme_morphism_basic
|
||
/-- A morphism property is `stable_under_composition` if the base change of such a morphism | ||
still falls in the class. -/ | ||
def stable_under_base_change |
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.
I guess this should come with API that let's you apply/construct this using "a base change" instead of "the base change". Can be done in a future PR.
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 merge
…rphisms between schemes (#14944) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Build failed (retrying...): |
…rphisms between schemes (#14944) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…rphisms between schemes (leanprover-community#14944) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
…rphisms between schemes (#14944) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
…rphisms between schemes (#14944) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>