Topic: image vs map and injective
Sean Leather (Jun 22 2018 at 07:21):
finset.map is defined as mapping an
embedding or an injective function over a
finset.image is mapping a function over a
finset. Other mathlib components (e.g
array, etc.) do not make this distinction using this naming scheme.
I think there is a useful distinction to be made here. For example, grep
injective: these declarations could be changed to use
embedding. But I'm not sure about the
map naming. Is this a standard thing? If so, can we implement it for other components? If not, can we come up with a meaningful naming distinction for mapping a function and mapping an injective function and implement that?
Reid Barton (Jun 22 2018 at 14:07):
The purpose of the distinction is that while
finset.image do the same thing, namely compute the image of a finite set under a function, they do so under incomparable hypotheses. Some hypothesis is necessary because we somehow need to ensure that the resulting
finset has no duplicates.
finset.image requires the target to have decidable equality, which is a free assumption when doing classical mathematics.
finset.map requires the function to be injective.
Reid Barton (Jun 22 2018 at 14:09):
finset.map is also much cheaper computationally, since it just has to apply the given function n times. I guess this is where the name
map comes from; computationally, it's just mapping a function over a data structure (the
Prop part does not exist computationally).
finset.image has to check the resulting list for duplicates and remove them, which takes time O(n^2).
Reid Barton (Jun 22 2018 at 14:11):
As far as the other types you mentioned are concerned, the "positive" types
array have no constraints analogous to the uniqueness in a
finset, so we can just use the
map implementation in all cases. For the "negative" type
set t = t -> Prop) we can't really hope to compute the image, so we can just use the logical definition.
Sean Leather (Jun 25 2018 at 06:46):
@Reid Barton Thanks for the very informative response! I neither noticed the
[decidable_eq β] on
finset.image nor realized its impact, so that's good to know.
I'm still not quite clear on what should be named what. Let me propose what I infer and anybody can shoot it down:
set.imageis the logical image of a set.
finset.imageis the analog to
set.imagefor a finite set. Since
set.imageinvolves a equality test, it makes since that
multiset.map, etc. are the standard (functor) mappings.
finset.mapis the implementation equivalent of
list.map, etc. but requires injectivity to preserve the
If I describe the situation as above, it makes sense to me.
That said, there are some cases where mapping an injective function over a list is useful. Is it worth creating an additional definition for
embedding along with associated theorems?
def list.imap (f : α ↪ β) : list α → list β := list.map f.to_fun
I don't have any good thoughts on the name. Is there a standard here?
Mario Carneiro (Jun 25 2018 at 06:57):
I don't see a reason to have such a definition, since you can just write
list.map f with the inserted coercion
Sean Leather (Jun 25 2018 at 07:00):
Right. The only reason would be for convenience, not for necessity of proof.
Sean Leather (Jun 25 2018 at 07:05):
The only reason would be for convenience, not for necessity of proof.
In fact, however, could you not say the same thing about
Sean Leather (Jun 25 2018 at 07:07):
The main difference, of course, is that
list.map is useful without injectivity and
finset.map is not.
Mario Carneiro (Jun 25 2018 at 07:11):
I mean that there is no gain besides a slightly longer name
Mario Carneiro (Jun 25 2018 at 07:11):
If you want to use
map on an injective function, just use it
Mario Carneiro (Jun 25 2018 at 07:12):
finset.map there is a clear difference since the definition is different
Sean Leather (Jun 25 2018 at 07:32):
Oh, I see. You're referring to the use of
list.map with an injective function. I was referring to the convenience of writing proofs for
map with injectivity: you wouldn't have to specify
injective f. Nonetheless, I concede that it's a pretty weak motivation.
Last updated: May 14 2021 at 18:28 UTC