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/module) : coe and internal #10004
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This looks good to me now, thanks. @kbuzzard, @jcommelin: do these names look reasonable to you? |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
src/algebra/direct_sum/basic.lean
Outdated
@@ -172,13 +172,23 @@ protected def id (M : Type v) (ι : Type* := punit) [add_comm_monoid M] [unique | |||
right_inv := λ x, to_add_monoid_of _ _ _, | |||
..direct_sum.to_add_monoid (λ _, add_monoid_hom.id M) } | |||
|
|||
/-- The canonical embedding from `⨁ i, A i` to `M`-/ |
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 think that this docstring should mention that the A i
are submonoids of M
.
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.
Thank you for the suggestion
src/algebra/direct_sum/basic.lean
Outdated
direct_sum.to_add_monoid (λ i, (A i).subtype) | ||
|
||
@[simp] lemma add_submonoid_coe_of {M : Type*} [decidable_eq ι] [add_comm_monoid M] | ||
(A : ι → add_submonoid M) (i : ι) (x : A i) : | ||
direct_sum.add_submonoid_coe A (direct_sum.of (λ i, A i) i x) = x := | ||
direct_sum.to_add_monoid_of _ _ _ |
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.
Aren't you in the direct_sum
namespace? So I guess you can remove some (all?) of these direct_sum.
prefixes.
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.
Thank you for the suggestion
src/algebra/direct_sum/basic.lean
Outdated
@@ -188,13 +198,23 @@ begin | |||
exact function.bijective.surjective h, | |||
end | |||
|
|||
/-- The canonical embedding from `⨁ i, A i` to `M`-/ |
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.
Idem.
src/algebra/direct_sum/module.lean
Outdated
@@ -194,6 +194,17 @@ lemma component.of (i j : ι) (b : M j) : | |||
if h : j = i then eq.rec_on h b else 0 := | |||
dfinsupp.single_apply | |||
|
|||
/-- The canonical embedding from `⨁ i, A i` to `M`-/ |
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.
Idem.
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 extracts the following `def`s from within the various `is_internal` properties: * `direct_sum.add_submonoid_coe` * `direct_sum.add_subgroup_coe` * `direct_sum.submodule_coe` Packing these into a def makes things more concise, and avoids some annoying elaboration issues. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>
Pull request successfully merged into master. Build succeeded: |
This extracts the following `def`s from within the various `is_internal` properties: * `direct_sum.add_submonoid_coe` * `direct_sum.add_subgroup_coe` * `direct_sum.submodule_coe` Packing these into a def makes things more concise, and avoids some annoying elaboration issues. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>
This extracts the following
def
s from within the variousis_internal
properties:direct_sum.add_submonoid_coe
direct_sum.add_subgroup_coe
direct_sum.submodule_coe
Packing these into a def makes things more concise, and avoids some annoying elaboration issues.
Co-authored-by: Eric Wieser wieser.eric@gmail.com