Zulip Chat Archive

Stream: maths

Topic: image vs map and injective


view this post on Zulip Sean Leather (Jun 22 2018 at 07:21):

In data.finset, finset.map is defined as mapping an embedding or an injective function over a finset, and finset.image is mapping a function over a finset. Other mathlib components (e.g set, multiset, list, 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 data/list/basic.lean for injective: these declarations could be changed to use embedding. But I'm not sure about the image vs 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?

view this post on Zulip Reid Barton (Jun 22 2018 at 14:07):

The purpose of the distinction is that while finset.map and 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.

view this post on Zulip 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).

view this post on Zulip Reid Barton (Jun 22 2018 at 14:11):

As far as the other types you mentioned are concerned, the "positive" types multiset, list, 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 (set t = t -> Prop) we can't really hope to compute the image, so we can just use the logical definition.

view this post on Zulip 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.image is the logical image of a set.
  • finset.image is the analog to set.image for a finite set. Since set.image involves a equality test, it makes since that finset.image require decidable_eq on β.
  • list.map, multiset.map, etc. are the standard (functor) mappings.
  • finset.map is the implementation equivalent of list.map, etc. but requires injectivity to preserve the finset properties.

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 list.map using 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?

view this post on Zulip 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

view this post on Zulip Sean Leather (Jun 25 2018 at 07:00):

Right. The only reason would be for convenience, not for necessity of proof.

view this post on Zulip 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 finset.map?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jun 25 2018 at 07:11):

I mean that there is no gain besides a slightly longer name

view this post on Zulip Mario Carneiro (Jun 25 2018 at 07:11):

If you want to use map on an injective function, just use it

view this post on Zulip Mario Carneiro (Jun 25 2018 at 07:12):

with finset.map there is a clear difference since the definition is different

view this post on Zulip 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