[Merged by Bors] - feat(GroupTheory): add DivisibleHull by wwylele · Pull Request #29275 · leanprover-community/mathlib4

wwylele · 2025-09-03T00:10:53Z

This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of LocalizedModule that this PR uses. Hopefully I avoided interfering it by using mostly with public API.

depends on: [Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers #29277
depends on: [Merged by Bors] - feat(RingTheory): NNRat is ring of fractions of Nat #29388
depends on: [Merged by Bors] - feat(Algebra/Order): Generalize IsMulTorsionFree to linearly ordered monoid #29386

github-actions · 2025-09-03T00:12:00Z

PR summary 09100dc0a5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Order.Monoid.PNat` (new file)	633
`Mathlib.GroupTheory.DivisibleHull` (new file)	1041

Declarations diff

+ DivisibleHull
+ IsOrderedCancelMonoid.of_mul_lt_mul_left
+ PNat.equivNonZeroDivisorsNat
+ archimedeanClassMk_mk_eq
+ archimedeanClassOrderHom
+ archimedeanClassOrderHomInv
+ archimedeanClassOrderIso
+ archimedeanClassOrderIso_apply
+ archimedeanClassOrderIso_symm_apply
+ coe
+ coeAddMonoidHom
+ coeOrderAddMonoidHom
+ coe_add
+ coe_inj
+ coe_injective
+ ind
+ instance : Coe M (DivisibleHull M)
+ instance : IsOrderedCancelAddMonoid (DivisibleHull M)
+ instance : IsStrictOrderedModule ℚ (DivisibleHull M)
+ instance : IsStrictOrderedModule ℚ≥0 (DivisibleHull M)
+ instance : LE (DivisibleHull M)
+ instance : LinearOrder (DivisibleHull M)
+ instance : Module ℚ (DivisibleHull M)
+ instance : SMul ℚ (DivisibleHull M)
+ liftOn
+ liftOn_mk
+ liftOn₂
+ liftOn₂_mk
+ mk
+ mk_add_mk
+ mk_add_mk_left
+ mk_eq_mk
+ mk_eq_mk_iff_smul_eq_smul
+ mk_le_mk
+ mk_left_injective
+ mk_lt_mk
+ neg_mk
+ nnqsmul_mk
+ nsmul_mk
+ pow_le_pow_iff_left
+ qsmul_def
+ qsmul_mk
+ qsmul_of_nonneg
+ qsmul_of_nonpos
+ zero_qsmul
+ zsmul_mk
++ mk_zero

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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).

Mathlib/GroupTheory/DivisibleHull.lean

vihdzp · 2025-09-03T04:49:28Z

Mathlib/GroupTheory/DivisibleHull.lean

+
+/-- The divisible hull of a Abelian group (as a ℤ-module) is the localized module by
+`Submonoid.pos ℤ`, thus a ℕ-divisble group, or a ℚ-module -/
+abbrev DivisibleHull := LocalizedModule (Submonoid.pos ℤ) M


I don't quite understand what the plan with LocalizedModule is, though I think the idea might be to entirely deprecate it in favor of OreLocalization at some point in the future. Might be worth checking in on that.

Mathlib/GroupTheory/DivisibleHull.lean

vihdzp · 2025-09-03T05:14:31Z

Mathlib/GroupTheory/DivisibleHull.lean

+def archimedeanClassOrderHom : ArchimedeanClass M →o ArchimedeanClass (DivisibleHull M) :=
+  ArchimedeanClass.orderHom (mkOrderAddMonoidHom M)
+
+theorem archimedeanClassMk_mk (m : M) (s : Submonoid.pos ℤ) :


Does this seem reasonable?

Suggested change

theorem archimedeanClassMk_mk (m : M) (s : Submonoid.pos ℤ) :

@[simp]

theorem archimedeanClassMk_mk (m : M) (s : Submonoid.pos ℤ) :

I removed this because this sent some simp in archimedeanClassOrderIso in a loop, but I'll investigate it

vihdzp · 2025-09-03T05:15:07Z

Mathlib/GroupTheory/DivisibleHull.lean

+      apply_fun ArchimedeanClass.mk at h
+      simp_rw [archimedeanClassMk_mk] at h
+      exact archimedeanClassOrderHom_injective M h))


You could then do:

Suggested change

apply_fun ArchimedeanClass.mk at h

simp_rw [archimedeanClassMk_mk] at h

exact archimedeanClassOrderHom_injective M h))

apply archimedeanClassOrderHom_injective M

simp))

Mathlib/GroupTheory/DivisibleHull.lean

…9277) Part of #29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.

Mathlib/GroupTheory/DivisibleHull.lean

wwylele · 2025-09-06T02:40:34Z

I added a second file Mathlib/GroupTheory/DivisibleHull2.lean to showcase generalizing this to AddCommMonoid. The unfortunate part of this generalization is the Q-module needs to be made manually. Not sure if this is the mathematically correct definition and whether we want this

Mathlib.lean

vihdzp

Some initial comments on the module version (which I agree is the better one to have).

Mathlib/GroupTheory/DivisibleHull2.lean

…anprover-community#29277) Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.

Extract from the new revision of #29275.

mathlib4-dependent-issues-bot · 2025-09-11T09:47:51Z

This PR/issue depends on:

~~[Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers #29277~~
~~[Merged by Bors] - feat(RingTheory): NNRat is ring of fractions of Nat #29388~~
~~[Merged by Bors] - feat(Algebra/Order): Generalize IsMulTorsionFree to linearly ordered monoid #29386~~
By Dependent Issues (🤖). Happy coding!

…anprover-community#29277) Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.

YaelDillies

Don't forget Violeta's comments!

Mathlib/GroupTheory/DivisibleHull.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

github-actions · 2025-09-18T17:49:51Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

…anprover-community#29277) Part of leanprover-community#29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.

…nity#29388) Extract from the new revision of leanprover-community#29275.

jcommelin

bors d+

Mathlib/GroupTheory/DivisibleHull.lean

mathlib-bors · 2025-10-09T08:39:13Z

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

Co-authored-by: Johan Commelin <johan@commelin.net>

wwylele · 2025-10-09T12:08:01Z

bors r+

This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.

mathlib-bors · 2025-10-09T13:01:41Z

Pull request successfully merged into master.

Build succeeded:

This is part of Hahn embedding theorem leanprover-community#27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at leanprover-community#25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API.

wwylele mentioned this pull request Sep 3, 2025

[Merged by Bors] - feat: Hahn embedding theorem #27268

Closed

7 tasks

github-actions bot added the t-group-theory Group theory label Sep 3, 2025

wwylele mentioned this pull request Sep 3, 2025

[Merged by Bors] - feat(RingTheory): Rat is localization of Int at positive integers #29277

Closed

wwylele force-pushed the wwylele-hahn-localize branch 2 times, most recently from a93a1b4 to 49935c3 Compare September 3, 2025 00:55

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 3, 2025

vihdzp reviewed Sep 3, 2025

View reviewed changes

wwylele force-pushed the wwylele-hahn-localize branch from 49935c3 to b9ddffd Compare September 4, 2025 01:06

mathlib-bors bot pushed a commit that referenced this pull request Sep 4, 2025

feat(RingTheory): Rat is localization of Int at positive integers (#2…

896dbda

…9277) Part of #29275. I put it immediately under `IsLocalization (nonZeroDivisors ℤ) ℚ` given the similarity.

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 4, 2025

vihdzp reviewed Sep 4, 2025

View reviewed changes

Mathlib/GroupTheory/DivisibleHull.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/DivisibleHull.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/DivisibleHull.lean Show resolved Hide resolved

Mathlib/GroupTheory/DivisibleHull.lean Show resolved Hide resolved

wwylele force-pushed the wwylele-hahn-localize branch from b9ddffd to c0fbed2 Compare September 5, 2025 00:30

vihdzp reviewed Sep 6, 2025

View reviewed changes

Mathlib.lean Outdated Show resolved Hide resolved

vihdzp reviewed Sep 6, 2025

View reviewed changes

Mathlib/GroupTheory/DivisibleHull2.lean Outdated Show resolved Hide resolved

vihdzp reviewed Sep 6, 2025

View reviewed changes

Mathlib/GroupTheory/DivisibleHull2.lean Outdated Show resolved Hide resolved

wwylele mentioned this pull request Sep 6, 2025

[Merged by Bors] - feat(RingTheory): NNRat is ring of fractions of Nat #29388

Closed

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 7, 2025

wwylele force-pushed the wwylele-hahn-localize branch 2 times, most recently from 835db3c to a883036 Compare September 7, 2025 18:23

mathlib-bors bot pushed a commit that referenced this pull request Sep 11, 2025

feat(RingTheory): NNRat is ring of fractions of Nat (#29388)

b26156e

Extract from the new revision of #29275.

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 11, 2025

wwylele force-pushed the wwylele-hahn-localize branch from a883036 to 14e9660 Compare September 11, 2025 18:59

wwylele marked this pull request as ready for review September 11, 2025 19:33

simp and clean up

7746f79

wwylele removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 18, 2025

missing doc

56bdf2e

wwylele requested a review from YaelDillies September 18, 2025 13:10

YaelDillies reviewed Sep 18, 2025

View reviewed changes

Mathlib/GroupTheory/DivisibleHull.lean Outdated Show resolved Hide resolved

address comments

bc3a1d3

wwylele force-pushed the wwylele-hahn-localize branch from 8559f86 to bc3a1d3 Compare September 18, 2025 15:12

remove redundant injective lemma

6c22748

wwylele requested a review from YaelDillies September 18, 2025 16:00

YaelDillies approved these changes Sep 18, 2025

View reviewed changes

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean Show resolved Hide resolved

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 18, 2025

use alias

164f85f

leanprover-community-bot-assistant assigned tb65536 Sep 26, 2025

joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Oct 2, 2025

feat(RingTheory): NNRat is ring of fractions of Nat (leanprover-commu…

72d807b

…nity#29388) Extract from the new revision of leanprover-community#29275.

zhuyizheng pushed a commit to zhuyizheng/mathlib4 that referenced this pull request Oct 2, 2025

feat(RingTheory): NNRat is ring of fractions of Nat (leanprover-commu…

7f1f4da

…nity#29388) Extract from the new revision of leanprover-community#29275.

jcommelin reviewed Oct 9, 2025

View reviewed changes

Mathlib/GroupTheory/DivisibleHull.lean Outdated Show resolved Hide resolved

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 9, 2025

Update Mathlib/GroupTheory/DivisibleHull.lean

0cf29a4

Co-authored-by: Johan Commelin <johan@commelin.net>

mathlib-bors bot changed the title ~~feat(GroupTheory): add DivisibleHull~~ [Merged by Bors] - feat(GroupTheory): add DivisibleHull Oct 9, 2025

mathlib-bors bot closed this Oct 9, 2025

wwylele deleted the wwylele-hahn-localize branch November 20, 2025 04:41

	theorem archimedeanClassMk_mk (m : M) (s : Submonoid.pos ℤ) :
	@[simp]
	theorem archimedeanClassMk_mk (m : M) (s : Submonoid.pos ℤ) :

Conversation

wwylele commented Sep 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Sep 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 09100dc0a5

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

vihdzp Sep 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vihdzp Sep 3, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Sep 4, 2025

Choose a reason for hiding this comment

Uh oh!

vihdzp Sep 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

wwylele commented Sep 6, 2025

Uh oh!

Uh oh!

vihdzp left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Sep 11, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Sep 18, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 9, 2025

Uh oh!

wwylele commented Oct 9, 2025

Uh oh!

mathlib-bors bot commented Oct 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

wwylele commented Sep 3, 2025 •

edited

Loading

github-actions bot commented Sep 3, 2025 •

edited

Loading