[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 sorryor 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! |
adomani
changed the title
|
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. |
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 |
eric-wieser
added
the
awaiting-review
eric-wieser
changed the title
eric-wieser
changed the title
|
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
eric-wieser
force-pushed
the
a_bunch_of_function.injective.instances
branch
from
0ca5bd5
to
8ebfeef
Compare
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 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! |
github-actions
bot
removed
the
merge-conflict
|
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. |
|
✌️ 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 |
|
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 |
github-actions
bot
added
the
ready-to-merge
…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: |
bors
bot
changed the title
…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_monoidsubmodule.to_ordered_add_comm_monoidordered_comm_group(and the impliedordered_add_comm_group)subgroup.to_ordered_comm_groupsubmodule.to_ordered_add_comm_groupordered_cancel_comm_monoid(and the impliedordered_cancel_add_comm_monoid)submonoid.to_ordered_cancel_comm_monoidsubmodule.to_ordered_cancel_add_comm_monoidlinear_ordered_cancel_comm_monoid(and the impliedlinear_ordered_cancel_add_comm_monoid)submonoid.to_linear_ordered_cancel_comm_monoidsubmodule.to_linear_ordered_cancel_add_comm_monoidlinear_ordered_comm_monoid_with_zerolinear_ordered_comm_group(and the impliedlinear_ordered_add_comm_group)subgroup.to_linear_ordered_comm_groupsubmodule.to_linear_ordered_add_comm_groupordered_semiringsubsemiring.to_ordered_semiringsubalgebra.to_ordered_semiringordered_comm_semiringsubsemiring.to_ordered_comm_semiringsubalgebra.to_ordered_comm_semiringordered_ringsubring.to_ordered_ringsubalgebra.to_ordered_ringordered_comm_ringsubring.to_ordered_comm_ringsubalgebra.to_ordered_comm_ringlinear_ordered_semiringsubring.to_linear_ordered_semiringsubalgebra.to_linear_ordered_semiringlinear_ordered_ringsubring.to_linear_ordered_ringsubalgebra.to_linear_ordered_ringlinear_ordered_comm_ringsubring.to_linear_ordered_comm_ringsubalgebra.to_linear_ordered_comm_ringlinear_ordered_fieldsubfield.to_linear_ordered_fieldZulip:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/rings.20from.20subtype