Transferring equiv.perm over embeddings

Stream: maths

[Yakov Pechersky]

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

[Yakov Pechersky]

@Eric Wieser

[Eric Wieser]

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?

[Eric Wieser]

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

[Yakov Pechersky]

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.

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Yakov Pechersky]

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?

[Yakov Pechersky]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Eric Wieser]

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

[Yakov Pechersky]

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

[Eric Wieser]

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