Zulip Chat Archive

Stream: Is there code for X?

Topic: lifting `α ↪ α` to `α ≃ α` in the presence of `fintype α`?


Scott Morrison (May 20 2020 at 10:54):

Do we have

def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α  α) : α  α := ...

(I don't mind if it is noncomputable particularly; presumably computability would further require [decidable_eq α].)

Scott Morrison (May 20 2020 at 10:55):

I came up with the rather unpleasant

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α  α) : α  α :=
begin
  apply function.embedding.equiv_of_surjective e _,
  apply (fintype.injective_iff_surjective_of_equiv (equiv.refl α)).mp _,
  exact function.embedding.inj e,
end

from the pieces I could find already available, but I'm hoping there's something better available.

Bhavik Mehta (May 20 2020 at 18:38):

Not clear if it's better but I came up with

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α  α) : α  α :=
begin
  apply equiv.of_bijective,
  rw  fintype.injective_iff_bijective,
  exact e.2
end

Bhavik Mehta (May 20 2020 at 18:40):

Term mode version:

noncomputable def function.embedding.equiv_of_fintype_endomorphism {α : Type*} [fintype α] (e : α  α) : α  α :=
equiv.of_bijective (fintype.injective_iff_bijective.1 e.2)

Scott Morrison (May 21 2020 at 01:17):

Thanks, that's perfect.


Last updated: Dec 20 2023 at 11:08 UTC