[Merged by Bors] - feat(Order): Quotient lift for ArchimedeanClass#26789
[Merged by Bors] - feat(Order): Quotient lift for ArchimedeanClass#26789wwylele wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
…Class This adds two features: - A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially. - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
PR summary 063d2e5dacImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| /-- Subtype of `MulArchimedeanClass` that removes the top element. -/ | ||
| @[to_additive ArchimedeanClass₀ "Subtype of `ArchimedeanClass` that removes the top element"] | ||
| abbrev MulArchimedeanClass₁ := {A : MulArchimedeanClass M // A ≠ ⊤} |
There was a problem hiding this comment.
Hmm, what's your use case for this? I fail to see
There was a problem hiding this comment.
The use case is here: https://github.com/leanprover-community/mathlib4/pull/25970/files#diff-d857e311a02648211ccdbdcba5616aaa348393380d223a4ab803a1bd02ab0d69R347 and will be also in the statement of Hahn embedding theorem.
There was a problem hiding this comment.
Can you maybe hold onto MulArchimedeanClass₁ until a later PR which actually uses it. Right now I don't fully get the point, and I strongly suspect there is a better way to do things that would completely bypass it
There was a problem hiding this comment.
Sure, I can remove them from this PR.
Here is another attempt to convince you that this will be eventually needed: as noted in Hahn embedding theorem https://en.wikipedia.org/wiki/Hahn_embedding_theorem , archimedean classes are often discussed among non-zero elements
Two nonzero elements g and h of G are Archimedean equivalent if there exist...
And the Ω in the theorem statement is the set of all non-zero Archimedean classes. To accurately state this theorem, a condition of "something that's not zero" has to be introduced somewhere, so here are the options
- Introduce the subtype on the group M from the beginning. Only define archimedean classes on non-zero elements. This makes it much easier to run into dependent type hell, as opposite to the existing natural definition of Archimedean classes on all elements.
- Prove the theorem all the way with Ω including the zero/top element, and only at the final step argue that one can remove the element: this might be possible, but it will make a lot of nice intermediate result not as sharp as it can be, such as the one I linked above.
- Introduce the subtype for intermediate result, but just use bare subtype, not a new definition: doable, but statements will get longer and busier overall. This was how I did it in my original draft, and in the end I introduced a custom notation for this just to make it more readable.
There was a problem hiding this comment.
btw, here is the statement of the theorem I am aiming for
theorem hahn_embedding (M: Type*) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]:
∃ f : M →+o Lex (HahnSeries (ArchimedeanClass₀ M) ℝ), Function.Injective f := sorry
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! bors merge |
This adds two features: - ~~A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.~~ - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
|
This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried. |
This adds two features: - ~~A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.~~ - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
|
Pull request successfully merged into master. Build succeeded: |
…#26789) This adds two features: - ~~A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.~~ - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
…#26789) This adds two features: - ~~A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.~~ - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
…#26789) This adds two features: - ~~A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.~~ - Add lift for both ArchimedeanClass and the subtype, analog to Quotient.lift Further more, promote it to a OrderHom given suitable conditions.
This adds two features:
A subtype of ArchimedeanClass that removes the top element. It is often useful to treat the top element specially.