Skip to content

[Merged by Bors] - feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder#25168

Closed
wwylele wants to merge 7 commits intomasterfrom
wwylele-hahn-series
Closed

[Merged by Bors] - feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder#25168
wwylele wants to merge 7 commits intomasterfrom
wwylele-hahn-series

Conversation

@wwylele
Copy link
Copy Markdown
Collaborator

@wwylele wwylele commented May 24, 2025 •
edited by YaelDillies
Loading

This is part of #25140. As the future codomain of the Hahn embedding theorem, HahnSeries needs a linear order.

It might be debatable whether the lexicographical order should be the order of HahnSeries. Aside from usage in Hahn embedding theorem, this order also represents, for example, the asymptotic behavior around (x : R) = 0, so it is generally useful. Updated to add LinearOrder on Lex (HahnSeries _ _) instead

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 45feb5a269

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.HahnSeries.Lex (new file) 692

Declarations diff

+ coeff_untop_eq_leadingCoeff
+ instance : IsOrderedAddMonoid (Lex (HahnSeries Γ R))
+ instance : LinearOrder (Lex (HahnSeries Γ R))
+ instance : PartialOrder (Lex (HahnSeries Γ R))
+ leadingCoeff_abs
+ leadingCoeff_neg
+ leadingCoeff_neg_iff
+ leadingCoeff_nonneg_iff
+ leadingCoeff_nonpos_iff
+ leadingCoeff_pos_iff
+ lt_iff
+ orderTop_abs
+ order_abs
+ support_abs

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 24, 2025
@wwylele wwylele mentioned this pull request May 25, 2025
Closed
7 tasks
eric-wieser
eric-wieser reviewed Jun 8, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Jun 8, 2025
View reviewed changes
ScottCarnahan
ScottCarnahan reviewed Jun 9, 2025
View reviewed changes
ScottCarnahan
ScottCarnahan reviewed Jun 9, 2025
View reviewed changes
ScottCarnahan
ScottCarnahan reviewed Jun 9, 2025
View reviewed changes
ScottCarnahan
ScottCarnahan reviewed Jun 9, 2025
View reviewed changes
@wwylele wwylele force-pushed the wwylele-hahn-series branch from 3ea7895 to 23b5730 Compare June 9, 2025 18:07
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Jun 9, 2025

Addressed comments and changed it to use Lex. I also renamed the file to Lex following by convention I see in other places.

ScottCarnahan
ScottCarnahan reviewed Jun 10, 2025
View reviewed changes
ScottCarnahan
ScottCarnahan reviewed Jun 10, 2025
View reviewed changes
@wwylele wwylele force-pushed the wwylele-hahn-series branch from 1543bd8 to 507631a Compare June 10, 2025 19:34
@wwylele wwylele requested a review from eric-wieser June 11, 2025 21:11
@ScottCarnahan ScottCarnahan changed the title feat(RingTheorey/HahnSeries): equip HahnSeries with LinearOrder feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder Jun 12, 2025
jcommelin
jcommelin reviewed Jun 12, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I have a few minor comments, and then it's ready for merging.

eric-wieser
eric-wieser reviewed Jun 12, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Jun 12, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it also canonically ordered? That is, if the coefficient ring is canonically ordered and so satifies zero_le, do we have zero_le for Lex (HahnSeries _ _)`?

@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Jun 12, 2025

Is it also canonically ordered? That is, if the coefficient ring is canonically ordered and so satifies zero_le, do we have zero_le for Lex (HahnSeries _ _)`?

I think this is true, though it wouldn't be compatible with the current proof of IsOrderedAddMonoid (Lex (HahnSeries Γ R)), which requires [AddCommGroup R]. Do you suggest having another IsOrderedAddMonoid (Lex (HahnSeries Γ R)) instance for [CanonicallyOrderedAdd R]`? (perhaps in another PR? I got caught in the middle of PR process change and I want to avoid migrating branches)

@wwylele wwylele requested a review from eric-wieser June 12, 2025 18:27
eric-wieser
eric-wieser reviewed Jun 13, 2025
View reviewed changes
@wwylele wwylele force-pushed the wwylele-hahn-series branch from cd97b19 to 1127ebc Compare June 13, 2025 14:59
eric-wieser
eric-wieser reviewed Jun 13, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Jun 13, 2025
View reviewed changes
@wwylele wwylele force-pushed the wwylele-hahn-series branch from ba2a4ec to c836036 Compare June 13, 2025 15:13
@wwylele wwylele force-pushed the wwylele-hahn-series branch from c836036 to c675be0 Compare June 13, 2025 15:13
eric-wieser
eric-wieser reviewed Jun 13, 2025
View reviewed changes
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Jun 13, 2025

Sorry for the consecutive pushes. I restructured sections and variables a little bit

I also checked CanonicallyOrderedAdd again, and now I don't think it is true for the current definition. For exists_add_of_le, if we look at HahnSeries (Fin 2) Nat, we have a = [1, 2] ≤ b = [2, 1], but the hypothetical c = [1, -1] isn't HahnSeries (Fin 2) Nat

@wwylele wwylele requested a review from eric-wieser June 13, 2025 16:48
@wwylele wwylele mentioned this pull request Jun 13, 2025
Closed
@wwylele
Copy link
Copy Markdown
Collaborator Author

wwylele commented Jun 15, 2025 •
edited
Loading

@eric-wieser Got some time for another review?

jcommelin
jcommelin reviewed Jun 16, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jun 16, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jun 16, 2025
@wwylele
feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (#25168)
4bce37e 
This is part of #25140. As the future codomain of the Hahn embedding theorem, `HahnSeries` needs a linear order.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 16, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder [Merged by Bors] - feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder Jun 16, 2025
@mathlib-bors mathlib-bors bot closed this Jun 16, 2025
@mathlib-bors mathlib-bors bot deleted the wwylele-hahn-series branch June 16, 2025 07:25
Rida-Hamadani pushed a commit to Rida-Hamadani/mathlib4 that referenced this pull request Jun 24, 2025
@wwylele @Rida-Hamadani
feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (leanp…
f080df1 
…rover-community#25168)

This is part of leanprover-community#25140. As the future codomain of the Hahn embedding theorem, `HahnSeries` needs a linear order.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@wwylele @callesonne
feat(RingTheory/HahnSeries): equip HahnSeries with LinearOrder (leanp…
fdc098b 
…rover-community#25168)

This is part of leanprover-community#25140. As the future codomain of the Hahn embedding theorem, `HahnSeries` needs a linear order.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

+1 more reviewer

@ScottCarnahan ScottCarnahan ScottCarnahan approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@wwylele @eric-wieser @jcommelin @ScottCarnahan