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/structure_sheaf): Define comap on structure sheaf #7788
Conversation
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
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.
How far are we from turning this into a morphism of sheaves?
If a section `s` on `U` is locally equal to the fraction `a/b`, its image on `V` is locally equal | ||
to the fraction `f(a)/f(b)`. | ||
-/ | ||
@[simps] def structure_sheaf.comap (f : R →+* S) (U : opens (prime_spectrum.Top R)) |
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.
Does @[simps]
generate a useful _apply
lemma here? The to_fun
entry looks pretty intimidating.
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's used multiple times in the subsequent lemmas. The bulk of the to_fun
entry is the proof that the section on V
is again locally fraction, which doesn't show up in the _apply
lemma any more. Still it's not exactly easy to read, I agree. I'm not sure how to improve it though. The comment above is meant to give an idea of what the definition means. Maybe I should expand upon that?
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.
One way to improve it might be to make an earlier definition comap_fun
and use that here. That way you can govern to what extent simp
will explode into a huge formula.
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.
Okay, I will try to do that!
Co-authored-by: Johan Commelin <johan@commelin.net>
It will be a morphism of sheaves in #7790. I didn't do it here because it requires |
Thanks 🎉 bors merge |
…heaf (#7788) Defines the comap of a ring homomorphism on the structure sheaves of the prime spectra. Co-authored-by: justus-springer <50165510+justus-springer@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Defines the comap of a ring homomorphism on the structure sheaves of the prime spectra.