[Merged by Bors] - feat(algebra/direct_sum): constructor for morphisms into direct sums #5204
Conversation
jcommelin
commented
Dec 3, 2020
•
jcommelin
commented
- depends on: [Merged by Bors] - feat(algebra/group): composition of monoid homs as "bilinear" monoid hom #5202
jcommelin
added
the
awaiting-review
| /-- `from_add_monoid φ` is the natural homomorphism from `γ` to `⨁ i, β i` | ||
| induced by a family `φ` of homomorphisms `γ → β i`. | ||
|
|
||
| Note that this is not an isomorphism. Not every homomorphism `γ →+ ⨁ i, β i` arises in this way. -/ | ||
| def from_add_monoid : (⨁ i, γ →+ β i) →+ (γ →+ ⨁ i, β i) := | ||
| to_add_monoid $ λ i, add_monoid_hom.comp_hom (of β i) |
There was a problem hiding this comment.
Does it make sense to putt this in dfinsupp (and finsupp, as (i →₀ γ →+ β) →+ (γ →+ i →₀ β)) too?
There was a problem hiding this comment.
cc @urkud who added finsupp.lift_add_hom in the first place.
There was a problem hiding this comment.
@eric-wieser I don't know... what will be the benefit of direct_sum over dfinsupp? Should we just remove direct_sum and make it optional notation for dfinsupp? Where exactly should the API boundary lie? I've never really used dfinsupp.
There was a problem hiding this comment.
I already don't know what the benefit of direct_sum over dfinsupp is. My guess is that the best comparison is monoid_algebra vs finsupp, where the former gets convolutive multiplication while the latter gets pointwise multiplication.
Of course, this is currently irrelevant for direct_sum and dfinsupp because neither gets any multiplication!
There was a problem hiding this comment.
hmm, then I would prefer to just do this for direct_sum for now. I tried copying the def to dfinsupp, but it didn't just work. And for me it's clear that this is something that we want for direct sums.
If we decide to merge the two concepts, then this PR is certainly not the place for that.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
jcommelin
added
the
blocked-by-other-PR
bryangingechen
removed
the
blocked-by-other-PR
|
Needs a merge/rebase to remove the changes from #5202 |
eric-wieser
added
awaiting-author
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
🎉 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! |
jcommelin
added
awaiting-review
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
