Zulip Chat Archive

Stream: Is there code for X?

Topic: If an equiv is contained with a set then so is its inverse


view this post on Zulip Eric Wieser (Jan 12 2021 at 10:00):

Does this exist? Is it true?

lemma equiv.inv_maps_to {s : set α} {f : perm α}
  (h : set.maps_to f s s) : set.maps_to (f⁻¹ : _) s s :=
begin
  unfold set.maps_to at *,
  sorry
end

This came up in #5706, where a similar lemma is introduced that requires fintype α. It's not clear to me whether this assumption is needed, but it's entirely possible I'm missing relevant intuition about finiteness

view this post on Zulip Anne Baanen (Jan 12 2021 at 10:07):

This should be true: the restriction of f to s is injective, so by finiteness of s it is also surjective, therefore an equiv. The inverse restricted to s is the inverse to the restriction of f.

view this post on Zulip Eric Wieser (Jan 12 2021 at 10:07):

Ah, so the fintype assumption is needed?

view this post on Zulip Anne Baanen (Jan 12 2021 at 10:08):

Yes, otherwise you can do things like mapping each rational number x to x / 2, which maps [0, 1] to [0, 1] but not in the other direction.

view this post on Zulip Eric Wieser (Jan 12 2021 at 10:08):

Thanks, a counter-example was exactly what I was hoping for. I should have looked for examples beyond nat and int...

view this post on Zulip Sebastien Gouezel (Jan 12 2021 at 10:23):

You have a counterexample in int, with the addition of 1 mapping the natural numbers to themselves, contrary to its inverse.

view this post on Zulip Eric Wieser (Jan 12 2021 at 10:44):

So in that example α is int, f is the permutation which adds one, and s is "non-negative"? Good point. I was slightly sad but not surprised to see that slim_check couldn't help me here.


Last updated: May 07 2021 at 19:12 UTC