-
Notifications
You must be signed in to change notification settings - Fork 298
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(algebra/module/localized_module): add characteristic predicate for localized_module
#15507
Conversation
@@ -33,7 +33,6 @@ Given a commutative ring `R`, a multiplicative subset `S ⊆ R` and an `R`-modul | |||
## Future work | |||
|
|||
* Redefine `localization` for monoids and rings to coincide with `localized_module`. |
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.
Something that is has to be done is to generalize the API for localized_module
to anything that satisfies the characteristic predicate.
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.
In #15584, Eric is trying to make localized_module
and localization
definitionally equal
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
This looks fine to me. I'm quite surprised we didn't have this earlier, but we didn't seem to. |
Sorry, I forgot about this. Thanks! bors merge |
Pull request successfully merged into master. Build succeeded: |
localized_module
localized_module
Add characteristic predicate for localised module similar to ring localization and prove that the concrete construction satisfies the characteristic predicate.
Co-authored-by: Andrew Yang @erdOne