## Stream: maths

### Topic: Transferring equiv.perm over embeddings

#### 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


@Eric Wieser

#### 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?

#### Eric Wieser (Jan 14 2021 at 09:14):

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

#### 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.

#### 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)?

#### 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

#### 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

#### 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?

#### Yakov Pechersky (Jan 14 2021 at 09:33):

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

#### Eric Wieser (Jan 14 2021 at 09:37):

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

#### Eric Wieser (Jan 14 2021 at 09:38):

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

#### Yakov Pechersky (Jan 14 2021 at 09:40):

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

#### Yakov Pechersky (Jan 14 2021 at 09:41):

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

#### 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.

#### 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.

#### Yakov Pechersky (Jan 14 2021 at 10:43):

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

#### 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