-
Notifications
You must be signed in to change notification settings - Fork 297
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] - refactor(algebra/direct_sum): rework internally-graded objects #10127
Conversation
src/algebra/direct_sum/internal.lean
Outdated
|
||
* `direct_sum.add_submonoid_coe_ring_hom` (a `ring_hom` version of `direct_sum.add_submonoid_coe`) | ||
* `direct_sum.add_subgroup_coe_ring_hom` (a `ring_hom` version of `direct_sum.add_subgroup_coe`) | ||
* `direct_sum.submodule_coe_ring_hom` (an `alg_hom` version of `direct_sum.submodule_coe`) |
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.
* `direct_sum.submodule_coe_ring_hom` (an `alg_hom` version of `direct_sum.submodule_coe`) | |
* `direct_sum.submodule_coe_alg_hom` (an `alg_hom` version of `direct_sum.submodule_coe`) |
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.
Whoops, nice catch; don't write docstrings at 2am!
Co-authored-by: Johan Commelin <johan@commelin.net>
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 🎉
bors merge
This is a replacement for the `graded_ring.core` typeclass in #10115, which is called `set_like.graded_monoid` here. The advantage of this approach is that we can use the same typeclass for graded semirings, graded rings, and graded algebras. Largely, this change replaces a bunch of `def`s with `instances`, by bundling up the arguments to those defs to a new typeclass. This seems to make life easier for the few global `gmonoid` instance we already provide for direct sums of submodules, suggesting this API change is a useful one. In principle the new `[set_like.graded_monoid A]` typeclass is useless, as the same effect can be achieved with `[set_like.has_graded_one A] [set_like.has_graded_mul A]`; pragmatically though this is painfully verbose, and probably results in larger term sizes. We can always remove it later if it causes problems. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Pull request successfully merged into master. Build succeeded: |
This is a replacement for the `graded_ring.core` typeclass in #10115, which is called `set_like.graded_monoid` here. The advantage of this approach is that we can use the same typeclass for graded semirings, graded rings, and graded algebras. Largely, this change replaces a bunch of `def`s with `instances`, by bundling up the arguments to those defs to a new typeclass. This seems to make life easier for the few global `gmonoid` instance we already provide for direct sums of submodules, suggesting this API change is a useful one. In principle the new `[set_like.graded_monoid A]` typeclass is useless, as the same effect can be achieved with `[set_like.has_graded_one A] [set_like.has_graded_mul A]`; pragmatically though this is painfully verbose, and probably results in larger term sizes. We can always remove it later if it causes problems. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Deletes a section that was always content-free, as well as a reference to code that was removed in leanprover-community/mathlib#10127.
This is a replacement for the
graded_ring.core
typeclass in #10115, which is calledset_like.graded_monoid
here. The advantage of this approach is that we can use the same typeclass for graded semirings, graded rings, and graded algebras.Largely, this change replaces a bunch of
def
s withinstances
, by bundling up the arguments to those defs to a new typeclass. This seems to make life easier for the few globalgmonoid
instance we already provide for direct sums of submodules, suggesting this API change is a useful one.In principle the new
[set_like.graded_monoid A]
typeclass is useless, as the same effect can be achieved with[set_like.has_graded_one A] [set_like.has_graded_mul A]
; pragmatically though this is painfully verbose, and probably results in larger term sizes. We can always remove it later if it causes problems.This does not fully replace #10115: that PR also provides
We still want that class or something similar to it (replacing
graded_ring.core
withset_like.graded_monoid
), but I deliberately leave it out of scope for this PR.