English
There is a canonical embedding of the permutation group on the subset {x : p x} into the permutation group on α, obtained by extending a permutation by the identity outside the subset. This map preserves composition and the identity, i.e. it is a monoid homomorphism.
Русский
Существует каноническое включение группы перестановок подмножества {x : p x} в группу перестановок на α, получаемое продлением перестановки до α и фиксацией точек вне подмножества. Это отображение сохраняет умножение и единицу, то есть является гомоморфизмом моноида.
LaTeX
$$$ \\mathrm{ofSubtype}: \\operatorname{Perm}(\{x \\mid p(x)\\}) \\to \\operatorname{Perm}(\\alpha)$, $\\mathrm{toFun}(f)=\\mathrm{extendDomain}(f, \\mathrm{refl}(\\{x \\mid p(x)\\}))$, with $\\mathrm{ofSubtype}(1)=1$ and $\\mathrm{ofSubtype}(f\\circ g)=\\mathrm{ofSubtype}(f)\\circ\\mathrm{ofSubtype}(g)$.$$
Lean4
/-- The inclusion map of permutations on a subtype of `α` into permutations of `α`,
fixing the other points. -/
def ofSubtype : Perm (Subtype p) →* Perm α
where
toFun f := extendDomain f (Equiv.refl (Subtype p))
map_one' := Equiv.Perm.extendDomain_one _
map_mul' f g := (Equiv.Perm.extendDomain_mul _ f g).symm
