English
The map toCentralizer is a right inverse of the permutation-to-centralizer construction on the relevant range: it assigns to each τ in range_toPermHom' g a centralizing element whose image under the toPermHom map is τ.
Русский
Отображение toCentralizer является правым оборотом отображения toPermHom на соответствующем диапазоне: каждому τ из range_toPermHom' g ставится в соответствие элемент, центральизующий g, чьё изображение в toPermHom равно τ.
LaTeX
$$toCentralizer: range_toPermHom' g →* centralizer\\{g\\}$$
Lean4
/-- Given `a : Equiv.Perm.Basis g`,
we define a right inverse of `Equiv.Perm.OnCycleFactors.toPermHom`,
on `range_toPermHom' g` -/
noncomputable def toCentralizer : range_toPermHom' g →* centralizer { g }
where
toFun τ := ⟨ofPermHom a τ, ofPermHom_mem_centralizer a τ⟩
map_one' := by simp only [map_one, mk_eq_one]
map_mul' σ τ := by simp only [map_mul, MulMemClass.mk_mul_mk]
