-
Notifications
You must be signed in to change notification settings - Fork 331
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
feat: quantales #17289
base: master
Are you sure you want to change the base?
feat: quantales #17289
Conversation
PR summary 2f0ddb0cd9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
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.
Welcome to Mathlib! I've left some comments to get you started. Please let me / us know if you have questions. Also, please see the commit conventions about the PR title and description.
Different bullet style Co-authored-by: Jireh Loreaux <[email protected]>
Style change, including 'left' Co-authored-by: Jireh Loreaux <[email protected]>
@j-loreaux Do I understand correctly that removing the |
Yes, generally, although it is also possible to request review. I see that you now also consider semigroups, which has led to a proliferation of classes. I think there is yet another possibility to consider here: make the algebraic structure an argument to the class rather than extending it. So you would write class Quantale (\a : Type*) [Semigroup \a] extends CompleteLattice \a where ...` The downside is that you have to write two things to get a quantale, but the upside is that you can easily change the underlying algebraic structure without defining all new classes. So, to get a bare bones quantale, you just write: but to get a commutative unital one, you simply change this to: After that, you could potentially make |
That does not seem the best way to go to me. I think the definition I have now for quantales fits best. The construct you are proposing would make sense if the general way of looking at it is that "you turn a semigroup into a quantale", but (just like with a ring consisting of two semigroups) that is not the way quantales are being used imo. Thanks for thinking along though! It really helps to have someone giving feedback :-) |
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
Co-authored-by: Yaël Dillies <[email protected]>
…Residual and rightResidual notation for AddQuantales (to_additive does not work there).
…nd - since to_additive was giving trouble)
…ver-community/mathlib4 into PieterCuijpers_Quantales
You still need to merge master. Do you know how to do that? |
Did not realize it was a separate step, next to running the CI, but I found this command: git merge origin master. |
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
First definition of Quantales - a non-commutative generalization of Locales/Frames. There are still some points of discussion, which would require changes elsewhere in Mathlib, but this definition should be workeable as a starting point (I think).
It's my first PR, but I've tried to stay close to what I've seen in CompleteLattices.