-
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] - feat(algebra/direct_sum_graded): A 0
is a ring, A i
is an A 0
-module, and direct_sum.of A 0
is a ring_hom
#6851
Conversation
… 0` is a ring_hom
… eric-wieser/direct_sum.of_ring_hom_injective
… eric-wieser/direct_sum.of_ring_hom_injective
A 0
is a ring and direct_sum.of A 0
is a ring_homA 0
is a ring, A i
is an A 0
-module, and direct_sum.of A 0
is a ring_hom
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
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.
I haven't checked too carefully, but it seems that a few of these lemmas should be tagged with simp
. What do you think?
On behalf of @adamtopaz |
…odule, and `direct_sum.of A 0` is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`. Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice.
Build failed (retrying...): |
…odule, and `direct_sum.of A 0` is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`. Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice.
This branch uses |
Canceled. |
bors r+ Thanks for cleaning up the conflicts, @urkud |
…odule, and `direct_sum.of A 0` is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`. Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Build failed (retrying...): |
…odule, and `direct_sum.of A 0` is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`. Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
…odule, and `direct_sum.of A 0` is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade `i` (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are `direct_sum.grade_zero.comm_ring`, `direct_sum.grade_zero.semimodule`, and `direct_sum.of_zero_ring_hom`. Note that we have no way to let the user provide their own ring structure on `A 0`, as `[Π i, add_comm_monoid (A i)] [semiring (A 0)]` provides `add_comm_monoid (A 0)` twice. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
A 0
is a ring, A i
is an A 0
-module, and direct_sum.of A 0
is a ring_homA 0
is a ring, A i
is an A 0
-module, and direct_sum.of A 0
is a ring_hom
In a graded ring, grade 0 is itself a ring, and grade
i
(and therefore, the overall direct_sum) is a module over elements of grade 0.This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR.
The main results here are
direct_sum.grade_zero.comm_ring
,direct_sum.grade_zero.semimodule
, anddirect_sum.of_zero_ring_hom
.Note that we have no way to let the user provide their own ring structure on
A 0
, as[Π i, add_comm_monoid (A i)] [semiring (A 0)]
providesadd_comm_monoid (A 0)
twice.This is a rework of #6837 that avoids having to prove anything interesting.