feat(GroupTheory): define left-orderable groups by homeowmorphism · Pull Request #41505 · leanprover-community/mathlib4

homeowmorphism · 2026-07-08T16:03:29Z

A group G is left-orderable if it admits a linear order invariant under left-multiplication that is, for all group elements a, b, and c, a < b → c * a < c * b. A group G is right-orderable if it admits a linear order invariant under right-multiplication a < b → a * c < b * c. A group G is bi-orderable if it admits a linear order invariant under left and right-multiplication a < b → c * a < c * b and a < b → a * c < b * c

This file defines the Prop-valued class IsLeftOrderable G, IsRightOrderable G and IsBiOrderable
asserting the existence of such orders.

Co-authored by: Yaël Dillies yael.dillies@gmail.com

Authored using Claude Fable during the Fermat’s Last Theorem workshop.

…oups Introduce `IsLeftOrderable`, a `Prop`-valued class recording that a group admits a linear order invariant under left multiplication (`MulLeftMono`), together with the instance deriving it from a concrete compatible order. The `@[mk_iff]` attribute generates `isLeftOrderable_iff`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…into IsLeftOrderable

homeowmorphism · 2026-07-08T16:03:48Z

+LLM-generated

github-actions · 2026-07-08T16:04:54Z

PR summary 242407fa16

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.GroupTheory.Orderable` (new file)	642

Declarations diff (regex)

+ IsBiOrderable
+ IsBiOrderable.of_mulEquiv
+ IsBiOrderable.to_isLeftOrderable
+ IsBiOrderable.to_isRightOrderable
+ IsLeftOrderable
+ IsLeftOrderable.of_mulEquiv
+ IsRightOrderable
+ IsRightOrderable.of_mulEquiv
+ MulEquiv.isBiOrderable_congr
+ MulEquiv.isLeftOrderable_congr
+ MulEquiv.isRightOrderable_congr
+ MulLeftStrictMono.to_isBiOrderable
+ MulLeftStrictMono.to_isLeftOrderable
+ MulRightStrictMono.to_isRightOrderable
+ Pi.instIsLeftOrderable
+ Pi.instIsRightOrderable
+ Prod.instIsLeftOrderable
+ Prod.instIsRightOrderable
+ exists_linearOrder_mulLeftMono
+ exists_linearOrder_mulLeftMono_mulRightMono
+ exists_linearOrder_mulRightMono
+ from
+ instance [Mul α] [Preorder α] [MulLeftStrictMono α]
+ instance [Mul α] [Preorder α] [MulRightStrictMono α]
+ instance [∀ i, Mul (α i)] [∀ i, PartialOrder (α i)] [∀ i, MulLeftStrictMono (α i)] :
+ instance [∀ i, Mul (α i)] [∀ i, PartialOrder (α i)] [∀ i, MulRightStrictMono (α i)] :
+ instance [∀ i, Mul (α i)] [∀ i, Preorder (α i)] [∀ i, MulLeftStrictMono (α i)] :
+ instance [∀ i, Mul (α i)] [∀ i, Preorder (α i)] [∀ i, MulRightStrictMono (α i)] :
+ isBiOrderable_iff_exists_linearOrder_mulLeftMono_mulRightMono
+ isBiOrderable_mulOpposite_iff
+ isLeftOrderable_iff_exists_linearOrder_mulLeftMono
+ isLeftOrderable_iff_isRightOrderable
+ isLeftOrderable_mulOpposite_iff_isRightOrderable
+ isRightOrderable_iff_exists_linearOrder_mulRightMono
+ isRightOrderable_mulOpposite_iff_isLeftOrderable

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 242407f).

+58 new declarations
−0 removed declarations

+IsBiOrderable
+IsBiOrderable.casesOn
+IsBiOrderable.exists_linearOrder_mulLeftStrictMono_mulRightStrictMono
+IsBiOrderable.mk
+IsBiOrderable.of_mulEquiv
+IsBiOrderable.rec
+IsBiOrderable.recOn
+IsBiOrderable.to_isLeftOrderable
+IsBiOrderable.to_isRightOrderable
+IsLeftOrderable
+IsLeftOrderable.casesOn
+IsLeftOrderable.exists_linearOrder_mulLeftStrictMono
+IsLeftOrderable.mk
+IsLeftOrderable.of_mulEquiv
+IsLeftOrderable.rec
+IsLeftOrderable.recOn
+IsRightOrderable
+IsRightOrderable.casesOn
+IsRightOrderable.exists_linearOrder_mulRightStrictMono
+IsRightOrderable.mk
+IsRightOrderable.of_mulEquiv
+IsRightOrderable.rec
+IsRightOrderable.recOn
+MulEquiv.isBiOrderable_congr
+MulEquiv.isLeftOrderable_congr
+MulEquiv.isRightOrderable_congr
+MulLeftStrictMono.to_isBiOrderable
+MulLeftStrictMono.to_isLeftOrderable
+MulRightStrictMono.to_isRightOrderable
+Pi.Lex.instAddLeftMonoLexForallOfAddLeftStrictMono
+Pi.Lex.instAddLeftStrictMonoLexForall
+Pi.Lex.instAddRightMonoLexForallOfAddRightStrictMono
+Pi.Lex.instAddRightStrictMonoLexForall
+Pi.Lex.instMulLeftMonoLexForallOfMulLeftStrictMono
+Pi.Lex.instMulLeftStrictMonoLexForall
+Pi.Lex.instMulRightMonoLexForallOfMulRightStrictMono
+Pi.Lex.instMulRightStrictMonoLexForall
+Pi.instIsLeftOrderable
+Pi.instIsRightOrderable
+Prod.Lex.instAddLeftMonoLexOfAddLeftStrictMono
+Prod.Lex.instAddRightMonoLexOfAddRightStrictMono
+Prod.Lex.instMulLeftMonoLexOfMulLeftStrictMono
+Prod.Lex.instMulRightMonoLexOfMulRightStrictMono
+Prod.instIsLeftOrderable
+Prod.instIsRightOrderable
+exists_linearOrder_mulLeftMono
+exists_linearOrder_mulLeftMono_mulRightMono
+exists_linearOrder_mulRightMono
+isBiOrderable_iff
+isBiOrderable_iff_exists_linearOrder_mulLeftMono_mulRightMono
+isBiOrderable_mulOpposite_iff
+isLeftOrderable_iff
+isLeftOrderable_iff_exists_linearOrder_mulLeftMono
+isLeftOrderable_iff_isRightOrderable
+isLeftOrderable_mulOpposite_iff_isRightOrderable
+isRightOrderable_iff
+isRightOrderable_iff_exists_linearOrder_mulRightMono
+isRightOrderable_mulOpposite_iff_isLeftOrderable

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5002	1	exposed public sections

Current commit 242407fa16
Reference commit 27c42f4d5c

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

YaelDillies

I was going to ask if we could have (bi-)orderable groups/monoids because they would be useful to state things in formal-conjectures, but then I read somewhere that a monoid is orderable iff it is cancellative and torsion-free. Assuming this is true, I believe we shouldn't have IsOrderable but instead spell it out as cancellative + torsion-free. Could you then leave a comment that cancellative + torsion-free implies IsLeftOrderable M?

homeowmorphism · 2026-07-10T10:38:02Z

I read somewhere that a monoid is orderable iff it is cancellative and torsion-free. Assuming this is true, I believe we shouldn't have IsOrderable but instead spell it out as cancellative + torsion-free.

I believe this refers to a commutative semigroup? I've found the statement is in p.5 of this paper https://arxiv.org/pdf/2511.00691, where Definition 2.1 refers to a monoid as a commutative and cancellative semigroup with identity so I think they are talking about the commutative monoid case.

Just as a sanity check, I tried to work out a counterexample, that is, finding a non-commutative monoid that is cancellative and torsion-free but not (bi)-orderable.

Take the Klein bottle group as a monoid with presentation $K_2 = \langle x,y | xyx = y\rangle$. Then this monoid is torsion-free and cancellative because it's apparently Adian by Theorem 2 in https://www.math.unl.edu/~jmeakin2/groups%20and%20semigroups.pdf, but it won't be (bi)-orderable as a monoid.

w.l.o.g assuming $1<x$, multiplication yields the following:

$y<yx$ (by left mul by $y$)
$yx < xyx = y$ (by right mul with $yx$)
Therefore, $y<yx<y$, which is a contradiction.

I might be wrong because I’m not solid on my monoids, but I do know that this Klein bottle group is not bi-orderable by non-example 1.5.0.6 in my thesis https://arxiv.org/pdf/2512.07035, so at the very least this statement doesn't make sense when you pass down to groups (groups are always cancellative, and left-orderable groups are always torsion-free unless they are the identity, and that doesn't automatically make them bi-orderable).

homeowmorphism · 2026-07-10T23:32:47Z

-awaiting-author

homeowmorphism · 2026-07-11T07:08:22Z

Looking at this code, I find the repetition of the statements with right-orderable groups quite repetitive. Sorry if this has already been covered, but what would be a possible better way to do it?

tb65536 · 2026-07-11T07:13:05Z

+i.e. `a < b → c * a < c * b`. -/
+@[mk_iff]
+class IsLeftOrderable (G : Type*) [Group G] : Prop where
+  exists_linearOrder_mulLeftStrictMono (G) : ∃ _ : LinearOrder G, MulLeftStrictMono G


Even though MulLeftStrictMono might be how it's often written, I think MulLeftMono might make your life slightly easier, and then the MulLeftStrictMono version can be an API lemma.

tb65536 · 2026-07-11T07:13:48Z

+  isBiOrderable_iff_exists_linearOrder_mulLeftMono_mulRightMono.mp ‹_›
+
+/-- A group is left-orderable iff it is right-orderable. -/
+theorem isLeftOrderable_iff_isRightOrderable : IsLeftOrderable G ↔ IsRightOrderable G := by


If these are equivalent, then there's no point in having both definitions, I feel. Why not just have an IsOrderable class with API lemmas giving the equivalence with left-orderability and right-orderability?

(although if you generalize to monoids, then maybe having both is necessary)

tb65536 · 2026-07-11T07:15:18Z

+class IsLeftOrderable (G : Type*) [Group G] : Prop where
+  exists_linearOrder_mulLeftStrictMono (G) : ∃ _ : LinearOrder G, MulLeftStrictMono G


Can you to_additive-ize this file?

tb65536 · 2026-07-11T07:16:11Z

+single order invariant under both left and right multiplication; this is strictly stronger than
+being both left- and right-orderable, since the latter may be witnessed by different orders.


Since you're just dealing with Prop-valued typeclasses, I don't think IsBiOrderable G is any stronger than IsLeftOrderable, right?

homeowmorphism and others added 7 commits March 18, 2026 16:03

wip still trying to figure out the core defs

8f72b00

changed var name

4f92864

Merge branch 'IsLeftOrderable' of github.com:homeowmorphism/mathlib4 …

5081744

…into IsLeftOrderable

first commit

a97755f

more Claude steering

4fe09fe

add authorship

6d0fa05

YaelDillies added t-algebra Algebra (groups, rings, fields, etc) LLM-generated PRs with substantial input from LLMs - review accordingly labels Jul 8, 2026

github-actions Bot added the t-group-theory Group theory label Jul 8, 2026

YaelDillies removed the t-algebra Algebra (groups, rings, fields, etc) label Jul 8, 2026

homeowmorphism added 5 commits July 8, 2026 17:12

moved file

df0c703

moved file

d7ff9d4

fix instance naming and shorten docstrings

f17f0ff

added instance names back

00f3438

named left-orderable instance

a0dc7b3

tb65536 reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/GroupTheory/Orderable.lean Outdated

tb65536 reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/GroupTheory/Orderable.lean Outdated

tb65536 reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/GroupTheory/Orderable.lean

homeowmorphism added 2 commits July 9, 2026 11:22

rename LO inst

af861d0

remove synth

63ed3a9

tb65536 reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/GroupTheory/Orderable.lean Outdated

homeowmorphism added 2 commits July 9, 2026 11:24

fixed indentation

944be9a

deleted the Claude-generated instance names

5b4d7cc

YaelDillies reviewed Jul 9, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Order/Monoid/Prod.lean

Comment thread Mathlib/GroupTheory/Orderable.lean Outdated

Comment thread Mathlib/GroupTheory/Orderable.lean Outdated

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 9, 2026

use MulLeftStrictMono

fbc57eb

homeowmorphism added 3 commits July 10, 2026 16:01

changed docstring

a1f8567

added right and bi

c094f38

added mop

242407f

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 10, 2026

tb65536 reviewed Jul 11, 2026

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 13, 2026

		class IsLeftOrderable (G : Type*) [Group G] : Prop where
		exists_linearOrder_mulLeftStrictMono (G) : ∃ _ : LinearOrder G, MulLeftStrictMono G

		single order invariant under both left and right multiplication; this is strictly stronger than
		being both left- and right-orderable, since the latter may be witnessed by different orders.

Uh oh!

Conversation

homeowmorphism commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

homeowmorphism commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 242407fa16

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

homeowmorphism commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

homeowmorphism commented Jul 10, 2026

Uh oh!

homeowmorphism commented Jul 11, 2026

Uh oh!

tb65536 Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

tb65536 Jul 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tb65536 Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

tb65536 Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

tb65536 Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

homeowmorphism commented Jul 8, 2026 •

edited

Loading

homeowmorphism commented Jul 8, 2026 •

edited

Loading

github-actions Bot commented Jul 8, 2026 •

edited

Loading

homeowmorphism commented Jul 10, 2026 •

edited

Loading

tb65536 Jul 11, 2026 •

edited

Loading