Skip to content

feat(GroupTheory): add divisible completion#25338

Closed
wwylele wants to merge 1 commit intomasterfrom
wwylele-hahn-completion
Closed

feat(GroupTheory): add divisible completion#25338
wwylele wants to merge 1 commit intomasterfrom
wwylele-hahn-completion

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented May 31, 2025

This is part of #25140. In order to "decompose" a linearly ordered group by its Archimedean classes, it needs to be embedded in a divisible group first. This code prepares for that embedding.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented May 31, 2025 •
edited
Loading

PR summary 2536582a52

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.GroupTheory.DivisibleCompletion (new file) 791

Declarations diff

+ PreDivisibleCompletion
+ PreRootableCompletion
+ PreRootableCompletion.mul
+ PreRootableCompletion.setoid
+ RootableCompletion
+ eq
+ instCommGroup
+ instCommMonoid
+ instIsOrderedMonoid
+ instLE
+ instLinearOrder
+ instMul
+ instOne
+ instRootableBy
+ inv_mk
+ le_def
+ le_iff
+ le_iff_left
+ mabs_mk
+ max_left
+ min_left
+ mk
+ monoidHom
+ monoidHom_apply
+ monoidHom_injective
+ mul_mk
+ one_eq
+ orderMonoidHom
+ orderMonoidHom_apply
+ orderMonoidHom_eq_monoidHom
+ orderMonoidHom_injective
+ out_eq
+ pow_mk

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label May 31, 2025
@wwylele wwylele mentioned this pull request May 31, 2025
Closed
7 tasks
@wwylele wwylele force-pushed the wwylele-hahn-completion branch from 094cf67 to 2536582 Compare May 31, 2025 22:26
@wwylele wwylele marked this pull request as draft June 7, 2025 16:35
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Jun 22, 2025

Another way to do this is to do the tensor product with Q, though one still need to develop the ordering theory on it. I am still thinking which is better. This one is used only at the final step of Hahn embedding theorem, so this can wait

@wwylele wwylele mentioned this pull request Jul 18, 2025
Closed
7 tasks
@grunweg grunweg added t-group-theory Group theory and removed t-algebra Algebra (groups, rings, fields, etc) labels Aug 5, 2025
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Aug 19, 2025 •
edited
Loading

Is this construction (at least in the additive case) not a special case of the module localisation? Making the add monoid M "divisible" is the same thing as making the ℕ-module M into a ℚ≥0-module, where ℚ≥0 is the localisation of ℕ at non-zero elements.

I am closing this since it is not from a fork, but please reopen it from your fork when it's ready!

@YaelDillies YaelDillies deleted the wwylele-hahn-completion branch August 19, 2025 08:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

t-group-theory Group theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@wwylele @YaelDillies @grunweg