New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebra/ordered_*, */sub{monoid,group,ring,semiring,field,algebra}): pullback of ordered algebraic structures under an injective map #6489
Conversation
It might make sense to also define the obvious |
Eric, I may be misunderstanding, but I think that there already is a |
I said I guess I still said the wrong thing though. I'm suggesting you add the thing that originally motivated this work : instance subsemiring.ordered_semiring [ordered_semiring R] : ordered_semiring (subsemiring R) :=
subtype.coe_injective.ordered_semiring sorry sorry sorry sorry or similar, where I suspect all the Fine to leave for a follow-up though. |
Ah, I had not understood you! And I had not realized that there was still something to do! I will take a look, thanks! |
I added the Eric, were you refactoring One further instance that I can think of that is inherited by subrings, should be |
Doesn't that already exist? I added all those recently.
No, I gave up on this, as I don't really know the maths too well or whether its a good idea. |
Ok, fair enough! Besides, I do not really have a good application for "integral domains" that do not necessarily have opposites. |
Eric, I pushed a version that I think has all the instances that you mentioned. I have not checked the There is also the question of whether we want the From above:
Still undone. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One more request - can you add function.injective.ordered_comm_group
and the associated subgroup.to_ordered_comm_group
instance (and their additive
instances)? I suspect there's nothing new to prove for them.
It would be good to try and pick these up too. I'm not sure that If you have a list in mind of missing instances like this, how about you write it down in a new github issue, and then we proceed without them. |
How about I go add the remaining instances? |
Well, I've added the missing definitions |
And I've updated the PR body to indicate all the new instances and functions. There are five left to add for |
Eric, thank you so much for adding more instances! I am very grateful for this, since it takes me quite some time to figure out what to do, even though I have now done it a few times! I really like the clear description that you gave in the PR body: I am tempted to see if we can get this PR merged and start with a fresh one for the remaining instances. As for the canonical stuff, that would indeed be more interesting, since I agree with you that it is not automatic, and it would be fun to think of the right "saturation" condition to ensure that a sub_thing of a canonically_ordered_thing is also canonically_ordered. |
Eric, thanks for the further instances! If I followed the changes correctly, I think that there is one from your list that is missing:
|
I ran into some issues with defeq-ness between sub and neg. Hopefully pushing a fix now... |
In fact, that issue was present even for your original Elsewhere in the library, we have both |
Wow, the PR went from being 27 changed lines to over 300! |
Yeah, this is a great demonstration of how dire our need for better automation is - your first 27 lines contains all the interesting proofs, and the rest are just boilerplate saying "combine the proofs you already have field-wise". We haven't even added the instances for |
…a}): pullback of ordered algebraic structures under an injective map
0ca5bd5
to
8ebfeef
Compare
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
Note that there's another build of the same commit happening here, with a 40 minutes head start: https://github.com/leanprover-community/mathlib/runs/2030608827 |
I lost track of whether this PR is now ready for review/merging or whether there are still things to be discussed. Also, I completely agree that it would be great to have better automation here. But I have no idea how to design it. |
This PR is strictly smaller than it was when @Vierkantor approved it, as parts of it ended up in other PRs. It's now just waiting for the build to pass, then can be merged. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, LGTM
bors d=@eric-wieser
bors d=@adomani
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
linter errors
This is so close now... Eric, thank you so much for all your effort and your help! |
bors r+ 🎉 |
bors merge |
Already running a review |
…a}): pullback of ordered algebraic structures under an injective map (#6489) Prove that the following 14 order typeclasses can be pulled back via an injective map (`function.injective.*`), and use them to attach 30 new instances to sub-objects: * `ordered_comm_monoid` (and the implied `ordered_add_comm_monoid`) * `submonoid.to_ordered_comm_monoid` * `submodule.to_ordered_add_comm_monoid` * `ordered_comm_group` (and the implied `ordered_add_comm_group`) * `subgroup.to_ordered_comm_group` * `submodule.to_ordered_add_comm_group` * `ordered_cancel_comm_monoid` (and the implied `ordered_cancel_add_comm_monoid`) * `submonoid.to_ordered_cancel_comm_monoid` * `submodule.to_ordered_cancel_add_comm_monoid` * `linear_ordered_cancel_comm_monoid` (and the implied `linear_ordered_cancel_add_comm_monoid`) * `submonoid.to_linear_ordered_cancel_comm_monoid` * `submodule.to_linear_ordered_cancel_add_comm_monoid` * `linear_ordered_comm_monoid_with_zero` * (no suitable subobject exists for monoid_with_zero) * `linear_ordered_comm_group` (and the implied `linear_ordered_add_comm_group`) * `subgroup.to_linear_ordered_comm_group` * `submodule.to_linear_ordered_add_comm_group` * `ordered_semiring` * `subsemiring.to_ordered_semiring` * `subalgebra.to_ordered_semiring` * `ordered_comm_semiring` * `subsemiring.to_ordered_comm_semiring` * `subalgebra.to_ordered_comm_semiring` * `ordered_ring` * `subring.to_ordered_ring` * `subalgebra.to_ordered_ring` * `ordered_comm_ring` * `subring.to_ordered_comm_ring` * `subalgebra.to_ordered_comm_ring` * `linear_ordered_semiring` * `subring.to_linear_ordered_semiring` * `subalgebra.to_linear_ordered_semiring` * `linear_ordered_ring` * `subring.to_linear_ordered_ring` * `subalgebra.to_linear_ordered_ring` * `linear_ordered_comm_ring` * `subring.to_linear_ordered_comm_ring` * `subalgebra.to_linear_ordered_comm_ring` * `linear_ordered_field` * `subfield.to_linear_ordered_field` Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…ects (#6509) This changes `subfield.to_field` to ensure that division is defeq. It also removes `subring.subset_comm_ring` which was identical to `subring.to_comm_ring`, renames some `subalgebra` instances to match those of `subring`s, and cleans up a few related proofs that relied on the old names. These are cleanups split from #6489, which failed CI but was otherwise approved
…a}): pullback of ordered algebraic structures under an injective map (#6489) Prove that the following 14 order typeclasses can be pulled back via an injective map (`function.injective.*`), and use them to attach 30 new instances to sub-objects: * `ordered_comm_monoid` (and the implied `ordered_add_comm_monoid`) * `submonoid.to_ordered_comm_monoid` * `submodule.to_ordered_add_comm_monoid` * `ordered_comm_group` (and the implied `ordered_add_comm_group`) * `subgroup.to_ordered_comm_group` * `submodule.to_ordered_add_comm_group` * `ordered_cancel_comm_monoid` (and the implied `ordered_cancel_add_comm_monoid`) * `submonoid.to_ordered_cancel_comm_monoid` * `submodule.to_ordered_cancel_add_comm_monoid` * `linear_ordered_cancel_comm_monoid` (and the implied `linear_ordered_cancel_add_comm_monoid`) * `submonoid.to_linear_ordered_cancel_comm_monoid` * `submodule.to_linear_ordered_cancel_add_comm_monoid` * `linear_ordered_comm_monoid_with_zero` * (no suitable subobject exists for monoid_with_zero) * `linear_ordered_comm_group` (and the implied `linear_ordered_add_comm_group`) * `subgroup.to_linear_ordered_comm_group` * `submodule.to_linear_ordered_add_comm_group` * `ordered_semiring` * `subsemiring.to_ordered_semiring` * `subalgebra.to_ordered_semiring` * `ordered_comm_semiring` * `subsemiring.to_ordered_comm_semiring` * `subalgebra.to_ordered_comm_semiring` * `ordered_ring` * `subring.to_ordered_ring` * `subalgebra.to_ordered_ring` * `ordered_comm_ring` * `subring.to_ordered_comm_ring` * `subalgebra.to_ordered_comm_ring` * `linear_ordered_semiring` * `subring.to_linear_ordered_semiring` * `subalgebra.to_linear_ordered_semiring` * `linear_ordered_ring` * `subring.to_linear_ordered_ring` * `subalgebra.to_linear_ordered_ring` * `linear_ordered_comm_ring` * `subring.to_linear_ordered_comm_ring` * `subalgebra.to_linear_ordered_comm_ring` * `linear_ordered_field` * `subfield.to_linear_ordered_field` Zulip: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…10900) Moving these to separate files should make typeclass synthesis less expensive. Additionally two of them are quite long and this shrinks them slightly. This handles: * `Submonoid` * `Subgroup` * `Subsemiring` * `Subring` * `Subfield` * `Submodule` * `Subalgebra` This also moves `Units.posSubgroup` into its own file. The copyright headers are from: * leanprover-community/mathlib#6489 * leanprover-community/mathlib#8466 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…10900) Moving these to separate files should make typeclass synthesis less expensive. Additionally two of them are quite long and this shrinks them slightly. This handles: * `Submonoid` * `Subgroup` * `Subsemiring` * `Subring` * `Subfield` * `Submodule` * `Subalgebra` This also moves `Units.posSubgroup` into its own file. The copyright headers are from: * leanprover-community/mathlib#6489 * leanprover-community/mathlib#8466 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…10900) Moving these to separate files should make typeclass synthesis less expensive. Additionally two of them are quite long and this shrinks them slightly. This handles: * `Submonoid` * `Subgroup` * `Subsemiring` * `Subring` * `Subfield` * `Submodule` * `Subalgebra` This also moves `Units.posSubgroup` into its own file. The copyright headers are from: * leanprover-community/mathlib#6489 * leanprover-community/mathlib#8466 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…10900) Moving these to separate files should make typeclass synthesis less expensive. Additionally two of them are quite long and this shrinks them slightly. This handles: * `Submonoid` * `Subgroup` * `Subsemiring` * `Subring` * `Subfield` * `Submodule` * `Subalgebra` This also moves `Units.posSubgroup` into its own file. The copyright headers are from: * leanprover-community/mathlib#6489 * leanprover-community/mathlib#8466 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Prove that the following 14 order typeclasses can be pulled back via an injective map (
function.injective.*
), and use them to attach 30 new instances to sub-objects:ordered_comm_monoid
(and the impliedordered_add_comm_monoid
)submonoid.to_ordered_comm_monoid
submodule.to_ordered_add_comm_monoid
ordered_comm_group
(and the impliedordered_add_comm_group
)subgroup.to_ordered_comm_group
submodule.to_ordered_add_comm_group
ordered_cancel_comm_monoid
(and the impliedordered_cancel_add_comm_monoid
)submonoid.to_ordered_cancel_comm_monoid
submodule.to_ordered_cancel_add_comm_monoid
linear_ordered_cancel_comm_monoid
(and the impliedlinear_ordered_cancel_add_comm_monoid
)submonoid.to_linear_ordered_cancel_comm_monoid
submodule.to_linear_ordered_cancel_add_comm_monoid
linear_ordered_comm_monoid_with_zero
linear_ordered_comm_group
(and the impliedlinear_ordered_add_comm_group
)subgroup.to_linear_ordered_comm_group
submodule.to_linear_ordered_add_comm_group
ordered_semiring
subsemiring.to_ordered_semiring
subalgebra.to_ordered_semiring
ordered_comm_semiring
subsemiring.to_ordered_comm_semiring
subalgebra.to_ordered_comm_semiring
ordered_ring
subring.to_ordered_ring
subalgebra.to_ordered_ring
ordered_comm_ring
subring.to_ordered_comm_ring
subalgebra.to_ordered_comm_ring
linear_ordered_semiring
subring.to_linear_ordered_semiring
subalgebra.to_linear_ordered_semiring
linear_ordered_ring
subring.to_linear_ordered_ring
subalgebra.to_linear_ordered_ring
linear_ordered_comm_ring
subring.to_linear_ordered_comm_ring
subalgebra.to_linear_ordered_comm_ring
linear_ordered_field
subfield.to_linear_ordered_field
Zulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype