[Merged by Bors] - feat(ring_theory/localization): Define local ring hom on localization at prime ideal #7522
Conversation
github-actions
bot
added
blocked-by-other-PR
github-actions
bot
added
merge-conflict
github-actions
bot
removed
merge-conflict
|
🎉 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! |
justus-springer
added
the
awaiting-review
|
|
||
| /-- For a ring hom `f : P →+* R` and a prime ideal `I` in `R`, the induced ring hom from the | ||
| localization of `P` at `ideal.comap f I` to the localization of `R` at `I` -/ | ||
| noncomputable def local_ring_hom : at_prime (ideal.comap f I) →+* at_prime I := |
There was a problem hiding this comment.
One thing that I'm a bit worried about is that in practice you might want to apply this when you need at_prime J →+* at_prime I. And then maybe J is not defeq to ideal.comap f I.
So it might be more flexible to ask for h : J = ideal.comap f I as extra argument to this definition.
There was a problem hiding this comment.
I'm currently in the middle of putting all things together to finally make Spec a functor and I'm pretty certain that for this application, the ideal is always defeq to ideal.comap f I. But of course I can't rule out out that for other applications, we want a more flexible version (but tbh, I can't think of many other applications at all...).
Should I change it to the more general version nevertheless? Or can we keep it for now and see how it goes?
There was a problem hiding this comment.
We can keep it like this for now.
github-actions
bot
added
ready-to-merge
… at prime ideal (#7522) Defines the induced ring homomorphism on the localizations at a prime ideal and proves that it is local and uniquely determined.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Defines the induced ring homomorphism on the localizations at a prime ideal and proves that it is local and uniquely determined.
This is mostly a specialization of
localization_map.map, which is itself a specialization oflocalization_map.lift. The only new lemma is the proof that it's a local ring hom, which will be needed to show thatSpecon morphisms gives a map of locally ringed spaces.