feat: quantales #17289
Open
feat: quantales #17289
+231
−1
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
new-contributor
PR summary 2f0ddb0cd9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
j-loreaux
reviewed
Sep 30, 2024
There was a problem hiding this comment.
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.
j-loreaux
added
the
awaiting-author
Different bullet style Co-authored-by: Jireh Loreaux <[email protected]>
Style change, including 'left' Co-authored-by: Jireh Loreaux <[email protected]>
PieterCuijpers
removed
the
awaiting-author
j-loreaux
added
the
awaiting-author
PieterCuijpers
removed
the
awaiting-author
|
@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 |
j-loreaux
added
the
awaiting-author
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
PieterCuijpers
added
awaiting-CI
and removed
awaiting-author
|
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. |
leanprover-community-bot-assistant
removed
the
merge-conflict
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.