[Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball by wwylele · Pull Request #27885 · leanprover-community/mathlib4

wwylele · 2025-08-02T20:41:06Z

Part of #27043 (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (Valuation.ball) and Metric.ball / Metric.closedBall (ArchimedeanClass M actually becomes a Valuation when M is a ring so these names make sense).

github-actions · 2025-08-02T20:42:22Z

PR summary aced7b254a

Import changes exceeding 2%

%	File
+2.01%	`Mathlib.Algebra.Order.Archimedean.Class`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Archimedean.Class	745	760	+15 (+2.01%)

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Order.Archimedean.Class`	15

Declarations diff

+ Iio_eq_bot
+ Ioi_eq_top
+ ballSubgroup
+ ballSubgroup_antitone
+ ballSubgroup_top
+ closedBallSubgroup
+ closedBallSubgroup_top
+ mem_ballSubgroup_iff
+ mem_closedBallSubgroup_iff
+ mem_subgroup_iff
+ subgroup
+ subgroup_antitone
+ subgroup_eq_bot
+ subgroup_strictAntiOn
+ subsemigroup
+ subsemigroup_eq_subgroup_of_ne_top

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/Algebra/Order/Archimedean/Class.lean

Mathlib/Algebra/Order/Module/Archimedean.lean

Mathlib/Algebra/Order/Archimedean/Class.lean

Mathlib/Algebra/Order/Module/Archimedean.lean

wwylele · 2025-08-10T20:33:38Z

Removed the module part from the PR and addressed the comments. It seems that I hit some unknown error in CI, so I rebased on latest master branch

Mathlib/Algebra/Order/Archimedean/Class.lean

alreadydone · 2025-08-10T22:40:34Z

Mathlib/Algebra/Order/Archimedean/Class.lean

+/-- An open ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ioi A`.
+For `A = ⊤`, we assign the junk value `⊥`. -/
+@[to_additive "An open ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ioi A`.
+For `A = ⊤`, we assign the junk value `⊥`. "]
+noncomputable
+abbrev ballSubgroup (A : MulArchimedeanClass M) := subgroup (UpperSet.Ioi A)


It's a bit confusing to use an uppercase letter for an element, which is usually used for types. Why not use {m : M} (c : MulArchimedeanClass M)?

I have been using (A : MulArchimedeanClass M) (a : M) (h : mk a = A) throughout the file. I don't quite remember how I chose this, but maybe I already committed to it so I should make it consistent?

Oh, it turns out a lot of (A : MulArchimedeanClass M) have gone from previous refactoring, so maybe I should change this

Mathlib/Order/UpperLower/Principal.lean

Mathlib/Algebra/Order/Archimedean/Class.lean

YaelDillies · 2025-08-11T05:49:13Z

Mathlib/Algebra/Order/Archimedean/Class.lean

+/-- A subgroup `G` is called a grade at `c` iff
+`ballSubgroup c` and `G` are complements in the lattice under `closedBallSubgroup c` -/
+@[to_additive "A subgroup `G` is called a grade at `c` iff
+`ballAddSubgroup c` and `G` are complements in the lattice under `closedBallAddSubgroup c`"]
+def IsGradeSubgroup (c : MulArchimedeanClass M) (G : Subgroup M) :=
+  Disjoint (ballSubgroup c) G ∧ ballSubgroup c ⊔ G = closedBallSubgroup c


This docstring doesn't teach me anything more than what I can already infer from the Lean code, but what does it mean to be a grade?

Let me see if I can explain this more in the file level doc to avoid duplicating the explanation for to_additive

Updated the file doc to provide some motivation. This is also where I'd like suggestions on better names. I named this originally from graded ring, because there are examples where an ordered ring is graded by archimedean classes (This makes more sense after #28179 defines addition on archimedean classes). Though, this is not generally true for all ordered rings, nor for ordered groups, so the name is not really accurate. Other names I have considered are

"summand", as in direct sum. Feels too generic

"residue": for an ordered field, this isomorphic to the residue field of the ArchimedeanClass.addValuation in [Merged by Bors] - feat: LinearOrderedAddCommGroupWithTop (ArchimedeanClass R) #28179. But this is only applicable to ring/field

"sphere": not really correct. Sphere usually is the set difference between closedBall and ball, but the one here is isomorphic to a quotient group.

Sorry, I don't get it. Where does this appear in the proof of Hahn's embedding theorem?

In https://www.jstor.org/stable/2032549?origin=crossref, this is $K_t$ on page 861 (whereas $H_t$ and $H'_t$ are closed/open balls). In the context of the paper, because the group was already assumed divisible, $K_t$ always exists. I don't assume additional condition yet, so this is only a Prop for now.

In https://www.ams.org/journals/proc/1952-003-06/S0002-9939-1952-0052045-1/, because the proof is done for only ordered real vector space, the "grade" submodule degenerates to one dimensional (thus become basis for finite dimensional spaces). This is $e_t$ on page 979

Sorry, I remain unconvinced by the design, in particular whether it should be a Prop or a definition, or even simply inlined. Do you mind moving it to the PR where it is used?

Mathlib/Algebra/Order/Archimedean/Class.lean

wwylele · 2025-08-12T14:23:26Z

Rebased and updated to the new to_additive doc string

riccardobrasca · 2025-08-14T20:02:44Z

Thanks!

bors merge

Part of #27043 (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

mathlib-bors · 2025-08-14T20:25:31Z

Build failed:

CI Success

riccardobrasca · 2025-08-14T20:30:08Z

Can you please merge master and fix the error? Thanks!

bors d+

mathlib-bors · 2025-08-14T20:30:11Z

✌️ 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.

wwylele · 2025-08-14T20:47:47Z

Apparently I missed a few to_additive doc fix, plus there is a recent rename of StrictAntiOn.le_iff_ge. Will merge soon once the fix passes

wwylele · 2025-08-14T21:05:51Z

bors r+

Part of #27043 (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

mathlib-bors · 2025-08-14T21:51:42Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

Part of leanprover-community#27043 (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from leanprover-community#27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

This continues #27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)

…munity#28449) This continues leanprover-community#27885 and promotes `ArchimedeanClass.addSubgroup` to a submodule. Balls are promoted to submodules with shorter names `ball` and `closedBall`, as they will be used a lot in the proof of Hahn embedding theorem (if you don't agree with this I can rename them to `ballSubmodule` and `closedBallSubmodule`)

github-actions bot added t-algebra Algebra (groups, rings, fields, etc) large-import Automatically added label for PRs with a significant increase in transitive imports labels Aug 2, 2025

wwylele mentioned this pull request Aug 2, 2025

[Merged by Bors] - feat(Algebra/Order): Hahn embedding theorem, part 1 #27043

Closed

7 tasks

YaelDillies reviewed Aug 6, 2025

View reviewed changes

Mathlib/Algebra/Order/Archimedean/Class.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Order/Archimedean/Class.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Order/Module/Archimedean.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Aug 10, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 10, 2025

wwylele force-pushed the wwylele-hahn-ball branch 2 times, most recently from 210eb47 to 28a1f91 Compare August 10, 2025 20:27

wwylele commented Aug 10, 2025

View reviewed changes

Mathlib/Algebra/Order/Archimedean/Class.lean Outdated Show resolved Hide resolved

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

alreadydone reviewed Aug 10, 2025

View reviewed changes

YaelDillies reviewed Aug 11, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 11, 2025

wwylele force-pushed the wwylele-hahn-ball branch from 2154848 to 31fbc85 Compare August 11, 2025 12:49

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

wwylele requested a review from YaelDillies August 12, 2025 14:18

wwylele added 7 commits August 12, 2025 10:20

feat(Algebra/Order): ArchimedeanClass ball and grade

5221d5a

address comments

1ac9de2

address comments

dbf63e5

Remove simp from mem_closedBallSubgroup_iff

54e7959

golf

1033578

rename

00abda1

address comments

501ef4e

wwylele force-pushed the wwylele-hahn-ball branch from 31fbc85 to d203967 Compare August 12, 2025 14:22

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Aug 12, 2025

use new additive doc

5ab6c3f

wwylele force-pushed the wwylele-hahn-ball branch from d203967 to 5ab6c3f Compare August 12, 2025 14:22

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

shake

1703711

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

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 14, 2025

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 14, 2025

wwylele added 2 commits August 14, 2025 16:40

Merge remote-tracking branch 'upstream/master' into wwylele-hahn-ball

2098704

fix merging with master

d5b8d91

mathlib-bors bot changed the title ~~feat(Algebra/Order): ArchimedeanClass ball~~ [Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball Aug 14, 2025

mathlib-bors bot closed this Aug 14, 2025

wwylele mentioned this pull request Aug 14, 2025

[Merged by Bors] - feat(Algebra/Order): ArchimedeanClass ball for module #28449

Closed

wwylele deleted the wwylele-hahn-ball branch September 2, 2025 01:31

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary aced7b254a

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

wwylele commented Aug 10, 2025

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wwylele Aug 11, 2025 • 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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

wwylele commented Aug 12, 2025

Uh oh!

riccardobrasca commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

riccardobrasca commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

wwylele commented Aug 14, 2025

Uh oh!

wwylele commented Aug 14, 2025

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

wwylele commented Aug 2, 2025 •

edited

Loading

github-actions bot commented Aug 2, 2025 •

edited

Loading

wwylele Aug 11, 2025 •

edited

Loading