mathlib3 documentation

group_theory.perm.via_embedding

equiv.perm.via_embedding, a noncomputable analogue of equiv.perm.via_fintype_embedding. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
noncomputable def equiv.perm.via_embedding {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α ↪ β) :
equiv.perm β

Noncomputable version of equiv.perm.via_fintype_embedding that does not assume fintype

Equations
source
theorem equiv.perm.via_embedding_apply {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α ↪ β) (x : α) :
⇑(e.via_embedding ι) (⇑ι x) = ⇑ι (⇑e x)
source
theorem equiv.perm.via_embedding_apply_of_not_mem {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α ↪ β) (x : β) (hx : x ∉ set.range ⇑ι) :
⇑(e.via_embedding ι) x = x
source
noncomputable def equiv.perm.via_embedding_hom {α : Type u_1} {β : Type u_2} (ι : α ↪ β) :
equiv.perm α →* equiv.perm β

via_embedding as a group homomorphism

Equations
source
theorem equiv.perm.via_embedding_hom_apply {α : Type u_1} {β : Type u_2} (e : equiv.perm α) (ι : α ↪ β) :
⇑(equiv.perm.via_embedding_hom ι) e = e.via_embedding ι
source
theorem equiv.perm.via_embedding_hom_injective {α : Type u_1} {β : Type u_2} (ι : α ↪ β) :
function.injective ⇑(equiv.perm.via_embedding_hom ι)