Zulip Chat Archive

Stream: Is there code for X?

Topic: Injective map inducing perm group homomorphism


view this post on Zulip Jordan Brown (Feb 15 2021 at 02:13):

I want to use the fact that an injective map induces an inclusion of permutation groups; the case where the map is inclusion of a subtype already seems to be in mathlib, but I cannot find the result for an arbitrary injective map. Is it in mathlib yet, or do I need to prove it?

view this post on Zulip Yakov Pechersky (Feb 15 2021 at 04:15):

Something like

def equiv.perm.of_embedding {α β : Type*} [fintype α] [decidable_eq β]
  (e : equiv.perm α) (f : α  β) : equiv.perm β :=
equiv.perm.subtype_congr (e.of_embedding_subtype f) (equiv.refl _)

Last updated: May 17 2021 at 15:13 UTC