Zulip Chat Archive

Stream: maths

Topic: Transferring equiv.perm over embeddings


view this post on Zulip Yakov Pechersky (Jan 14 2021 at 07:21):

Is this a valid construction? If it is, a lot of code about transferring perms to option or across fin can become much simpler since some, fin.succ, fin.cast_succ, fin.succ_above are all embeddings.

import group_theory.perm.sign
import data.set.finite

section

open equiv

variables {α β : Type*}

lemma function.embedding.exists_unique (f : α  β) {b : β} (hb : b  set.range f) :
  ∃! a, f a = b :=
begin
  obtain a, ha := hb,
  refine a, ha, λ a' ha', f.injective _⟩,
  rw [ha, ha']
end

lemma function.embedding.exists_unique' [fintype α] (f : α  β) {b : β} (hb : b  set.range f) :
  ∃! a, a  (finset.univ : finset α)  f a = b :=
begin
  obtain a, ha, hu := f.exists_unique hb,
  exact a, finset.mem_univ a, ha⟩, λ a' ha', hu a' ha'.right
end

def function.embedding.inv_of_mem_range [fintype α] [decidable_eq β] (f : α  β) {b : β}
  (hb : b  set.range f) : α :=
finset.choose (λ a, f a = b) finset.univ (f.exists_unique' hb)

@[simp] lemma function.embedding.left_inv_of_inv_of_mem_range [fintype α] [decidable_eq β]
  (f : α  β) {b : β} (hb : b  set.range f) : f (f.inv_of_mem_range hb) = b :=
(finset.choose_spec (λ a, f a = b) finset.univ (f.exists_unique' hb)).right

@[simp] lemma function.embedding.right_inv_of_inv_of_mem_range [fintype α] [decidable_eq β]
  (f : α  β) (a : α) : f.inv_of_mem_range (set.mem_range_self a : f a  set.range f) = a :=
f.injective (finset.choose_spec (λ a', f a' = f a) finset.univ
  (f.exists_unique' (set.mem_range_self a))).right

def equiv.perm.of_embedding [fintype α] [decidable_eq β]
  (e : perm α) (f : function.embedding α β) : perm β :=
{ to_fun := λ b, if h : b  (set.range f).to_finset
    then f (e (f.inv_of_mem_range (set.mem_to_finset.mp h))) else b,
  inv_fun := λ b, if h : b  (set.range f).to_finset
    then f (e.symm (f.inv_of_mem_range (set.mem_to_finset.mp h))) else b,
  left_inv := λ b,
  begin
    by_cases hb : b  (set.range f).to_finset,
    { simp [hb] },
    { dsimp only,
      rw dif_neg;
      rwa dif_neg hb }
  end,
  right_inv := λ b,
  begin
    by_cases hb : b  (set.range f).to_finset,
    { simp [hb] },
    { dsimp only,
      rw dif_neg;
      rwa dif_neg hb }
  end }

end

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 07:22):

@Eric Wieser

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:13):

Does it make sense to introduce a bundled type for functions and their left inverse, as a stronger form of embedding but a weaker form of equiv?

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:14):

Or is that just a special case of docs#local_equiv?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:19):

Yeah, it's a local_equiv where the source is univ and the constraints become easy to satisfy from that. There's probably some relation here to functorial inductives and how some allow for "retrieval", like option, list, etc.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:21):

You think it's not worth it to provide a generic left-inverse for embeddings (when satisfying the fintype/deceq constraint)?

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:30):

I think if we had the bundled type, then we could replace your left inverse with a promotion to that bundled type

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:30):

And that way we have just one equiv.perm.of_left_invertible that works for any construction of the bundled left inverse

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:33):

But the embedding itself, when over the fintype/deceq has a unique left inverse as it is. So are you saying have the bundled type without the constraint, and have a def that upgrades any embedding from/to fintype/deceq to the bundled type?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:33):

Of course, computationally, the provided inverse is terrible because it's O(N)

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:37):

Yes, because that means that a computationally/ definitionally sensible inverse can be also be bundled manually

view this post on Zulip Eric Wieser (Jan 14 2021 at 09:38):

Just like we have a way to upgrade bijective to an equiv today

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:40):

Maybe just require (g) (hg : function.left_inverse g f_embed)?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:41):

In fact, we have docs#function.left_inverse.injective

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 09:43):

so {g} {f} (h : function.left_inverse g f) should be enough, since the injectivity of f that makes it an embedding is inferrable.

view this post on Zulip Eric Wieser (Jan 14 2021 at 10:42):

I'm suggesting that there might be value in bundling those three things eventually, but working with them separately is fine in the meantime.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 10:43):

How would you phrase it for the left inverse of some?

view this post on Zulip Eric Wieser (Jan 14 2021 at 10:51):

Are you asking for a left-inverse of some? It's just option.cases_on default id, right, or maybe option.get?


Last updated: May 11 2021 at 16:22 UTC