[Merged by Bors] - feat(algebra/lattice_ordered_group): add basic theory of lattice ordered groups #8673

mans0954 · 2021-08-14T20:05:49Z

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

mans0954 · 2021-08-14T20:06:53Z

Previously opened as #8663

src/algebra/lattice_ordered_group.lean

mans0954 · 2021-08-17T01:50:01Z

I've re-worked the theory into multiplicative notation as suggested by @jcommelin in the original PR.

It appears the abel tactic only works for additive groups, which required reworking some proofs.

mans0954 · 2021-08-19T19:13:07Z

Thanks for all the feedback so far. The linter is currently failing on the branch with:

Run ./scripts/mk_all.sh
  ./scripts/mk_all.sh
  lean --run scripts/lint_mathlib.lean
  shell: /usr/bin/bash -e {0}
deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
Error: Process completed with exit code 1.

I am not sure what to do about this?

src/algebra/lattice_ordered_group.lean

jcommelin · 2021-09-06T11:18:20Z

Thanks 🎉

bors d+

bors · 2021-09-06T11:18:21Z

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mans0954 · 2021-09-06T11:34:20Z

bors r+

…red groups (#8673) Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

bors · 2021-09-06T14:26:26Z

Pull request successfully merged into master.

Build succeeded:

@eric-wieser

The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #8673 for lattice ordered groups, along with the notation `|.|` and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit `has_abs` and the notation to mathlib. I tried to introduce both the `has_abs` class and the `|.|` notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of `abs : α → α` in the following locations: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113 Out of scope are the following `abs : α → β`: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315 Replacing the `abs` notation with `|.|` can be considered in a subsequent PR. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

@eric-wieser

The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #8673 for lattice ordered groups, along with the notation `|.|` and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit `has_abs` and the notation to mathlib. I tried to introduce both the `has_abs` class and the `|.|` notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of `abs : α → α` in the following locations: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113 Out of scope are the following `abs : α → β`: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315 Replacing the `abs` notation with `|.|` can be considered in a subsequent PR. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

@eric-wieser

The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #8673 for lattice ordered groups, along with the notation `|.|` and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit `has_abs` and the notation to mathlib. I tried to introduce both the `has_abs` class and the `|.|` notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of `abs : α → α` in the following locations: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113 Out of scope are the following `abs : α → β`: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315 Replacing the `abs` notation with `|.|` can be considered in a subsequent PR. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

@eric-wieser

The notion of an "absolute value" occurs both in algebra (e.g. lattice ordered groups) and analysis (e.g. GM and GL-spaces). I introduced a `has_abs` notation class in #8673 for lattice ordered groups, along with the notation `|.|` and was asked by @eric-wieser and @jcommelin to add it in a separate PR and retro fit `has_abs` and the notation to mathlib. I tried to introduce both the `has_abs` class and the `|.|` notation in #8891 . However, I'm finding such a large and wide-ranging PR unwieldy to work with, so I'm now opening this PR which just replaces the previous definitions of `abs : α → α` in the following locations: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/algebra/ordered_group.lean#L984 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/topology/continuous_function/basic.lean#L113 Out of scope are the following `abs : α → β`: https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/is_R_or_C.lean#L439 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/complex/basic.lean#L406 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/real/nnreal.lean#L762 https://github.com/leanprover-community/mathlib/blob/f36c98e877dd86af12606abbba5275513baa8a26/src/data/num/basic.lean#L315 Replacing the `abs` notation with `|.|` can be considered in a subsequent PR. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

mans0954 changed the title ~~Lattice ordered group~~ feat(src/algebra) : add basic theory of lattice ordered groups Aug 14, 2021

mans0954 added the awaiting-review The author would like community review of the PR label Aug 14, 2021

eric-wieser reviewed Aug 14, 2021

View reviewed changes

src/algebra/lattice_ordered_group.lean Outdated Show resolved Hide resolved