English
The construction of ofPermHom yields a homomorphism from range_toPermHom' g to Perm α whose action centralizes g.
Русский
Конструкция ofPermHom задаёт гомоморфизм от range_toPermHom' g в Perm α, чьё действие концилизирует g.
LaTeX
$$ofPermHom : range_toPermHom' g →* Perm α$$
Lean4
/-- Given `a : g.Basis` and a permutation of `g.cycleFactorsFinset` that
preserve the lengths of the cycles, a permutation of `α` that
moves the `Basis` and commutes with `g` -/
noncomputable def ofPermHom : range_toPermHom' g →* Perm α
where
toFun
τ :=
{ toFun := ofPermHomFun a τ
invFun := ofPermHomFun a τ⁻¹
left_inv := fun x ↦ by rw [← ofPermHomFun_mul, inv_mul_cancel, ofPermHomFun_one]
right_inv := fun x ↦ by rw [← ofPermHomFun_mul, mul_inv_cancel, ofPermHomFun_one] }
map_one' := ext fun x ↦ ofPermHomFun_one a x
map_mul' := fun σ τ ↦ ext fun x ↦ by simp [mul_apply, ofPermHomFun_mul a σ τ x]
