# Zulip Chat Archive

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

s 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 (Jan 14 2021 at 07:22):

@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