feat(data/finsupp/equiv_dfinsupp): add an equivalence between finsupp and dfinsupp #7217
Conversation
eric-wieser
changed the title
eric-wieser
added
the
awaiting-review
| variables (M) | ||
|
|
||
| /-- The submonoid corresponding to the range of `finsupp.single`. -/ | ||
| abbreviation single_submonoid [add_monoid M] (i : ι) : add_submonoid (ι →₀ M) := |
There was a problem hiding this comment.
Does it make sense to call this single_mrange?
There was a problem hiding this comment.
If we do that we end up with a name conflict for linear_map.range and subgroup.range when I inevitably extend this to subgroups and submodules - both are after the coveted single_range name, but one will have to be prefixed. I suppose that's not too big a deal, but it's why I went for the easy option of just putting the type at the end.
There was a problem hiding this comment.
I understand, but how about single_grange and single_lrange for those others? I think it's useful if the name mentions range. Now it sounds like you are putting a submonoid instance on something called single, or so...
| noncomputable def finsupp.equiv_dfinsupp_single_submonoid [decidable_eq ι] [add_comm_monoid M] : | ||
| (ι →₀ M) ≃+ (Π₀ i : ι, finsupp.single_submonoid M i) := |
There was a problem hiding this comment.
I would expect the following statement
| noncomputable def finsupp.equiv_dfinsupp_single_submonoid [decidable_eq ι] [add_comm_monoid M] : | |
| (ι →₀ M) ≃+ (Π₀ i : ι, finsupp.single_submonoid M i) := | |
| noncomputable def finsupp.equiv_dfinsupp_single_submonoid [decidable_eq ι] [add_comm_monoid M] : | |
| (ι →₀ M) ≃+ (Π₀ i : ι, M) := |
Is there a reason you picked your version?
There was a problem hiding this comment.
That's probably a good definition to have somewhere (i'm suspicious we already have it), but its not the one I'm interested in - the idea behind this equivalence is that it equates a polynomial with a direct sum of its monomials.
I suppose it would be possible / sensible to split this equivalence into (ι →₀ M) ≃+ (Π₀ i : ι, M) and (Π₀ i : ι, M) ≃+ (Π₀ i : ι, finsupp.single_submonoid M i), but I suspect the proofs would look the same anyway.
There was a problem hiding this comment.
I'll have a go at doing the split.
There was a problem hiding this comment.
Ah, the equivalence you describe roughly exists as finsupp_lequiv_direct_sum
There was a problem hiding this comment.
I've added the additive version in #7311
jcommelin
added
awaiting-author
This adds the bundled homs: * `dfinsupp.map_range.add_monoid_hom` * `dfinsupp.map_range.add_equiv` * `dfinsupp.map_range.linear_map` * `dfinsupp.map_range.linear_equiv` and lemmas * `dfinsupp.map_range_zero` * `dfinsupp.map_range_add` * `dfinsupp.map_range_smul` For which we already have identical lemmas for `finsupp`. Split from #7217, since `map_range.add_equiv` can be used in conjunction with `submonoid.mrange_restrict`
github-actions
bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
semorrison
added
the
too-late
Doing this for
subgroupis slightly harder as some simp lemmas are missing - so I will leave that to a follow up.The missing simp lemma that would be needed for subgroups is in #7218