feat(src/algebra): add basic theory of lattice ordered groups #8663
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
jcommelin
changed the title
jcommelin
added
the
awaiting-review
jcommelin
reviewed
Aug 13, 2021
There was a problem hiding this comment.
Thanks for your PR! The code looks pretty mature already, at first sight.
But there are some stylistic issues. I've marked the first few, but please go through the entire file.
Concerning the additive/multiplicative decision: I think @[to_additive] could do almost all of the work for you, right? So in principal it shouldn't be much harder to develop the multiplicative story as well.
Otoh, I agree that maybe it's not likely to see use in the future.
Comment on lines
+39
to
+41
| - `a⁺ = a ⊔ 0`: The *positive component* of an element a of a `lattice_ordered_add_comm_group` | ||
| - `a⁻ = (-a) ⊔ 0`: The *negative component* of an element a of a `lattice_ordered_add_comm_group` | ||
| * `|a| = a⊔(-a)`: The *absolute value* of an element a of a `lattice_ordered_add_comm_group` |
There was a problem hiding this comment.
Suggested change
| - `a⁺ = a ⊔ 0`: The *positive component* of an element a of a `lattice_ordered_add_comm_group` | |
| - `a⁻ = (-a) ⊔ 0`: The *negative component* of an element a of a `lattice_ordered_add_comm_group` | |
| * `|a| = a⊔(-a)`: The *absolute value* of an element a of a `lattice_ordered_add_comm_group` | |
| - `a⁺ = a ⊔ 0`: The *positive component* of an element `a` of a `lattice_ordered_add_comm_group` | |
| - `a⁻ = (-a) ⊔ 0`: The *negative component* of an element `a` of a `lattice_ordered_add_comm_group` | |
| * `|a| = a⊔(-a)`: The *absolute value* of an element `a` of a `lattice_ordered_add_comm_group` |
| universe u | ||
|
|
||
| /-- | ||
| A group (α,*), equipped with a partial order ≤, making α into a lattice, such that, given elements |
There was a problem hiding this comment.
Please surround all the variables etc with backticks.
Comment on lines
+130
to
+131
| end | ||
| } |
Comment on lines
+143
to
+144
| end | ||
| } |
Comment on lines
+160
to
+162
| { simp, } | ||
| }, | ||
| { rw ← add_le_add_iff_left (-c), simp, } |
There was a problem hiding this comment.
Suggested change
| { simp, } | |
| }, | |
| { rw ← add_le_add_iff_left (-c), simp, } | |
| { simp, } }, | |
| { rw ← add_le_add_iff_left (-c), simp, } |
2 tasks
YaelDillies
removed
the
awaiting-review
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.
feat(src/algebra) : add basic theory of lattice ordered groups
This is my first non-trivial PR to mathlib. It adds the basic theory of lattice ordered groups, which is useful as the algebraic underpinnings of vector lattices, Banach lattices, AL-space, AM-space etc. I am still relatively new to lean/mathlib and have a lot to learn, so constructive criticism is very welcome. I imagine an expert could write more succinct proofs.
I have defined both the multiplicative and additive classes, but have mostly developed the theory with the additive classes as this notation seems more natural in this context, and I have not myself had an application for multiplicative lattice ordered groups. I'm happy to rewrite the file in the multiplicative form if required.
Many of the results are valid in the non-commutative case, but the proofs are more involved. I've only submitted the commutative case, as that's all I personally need. Should I be aiming for greater generality?
Thanks for your time,
Christopher Hoskin