English
The range_toPermHom' g maps into a subgroup of Perm(g.cycleFactorsFinset) preserving cycle lengths.
Русский
range_toPermHom' g отображает в подгруппу Perm(g.cycleFactorsFinset) сохраняющую длины циклов.
LaTeX
$$$\operatorname{range\_toPermHom'}(g) \leq \operatorname{Perm}(g.cycleFactorsFinset)$ with the length-preserving property$$
Lean4
theorem ofPermHomFun_apply_of_cycleOf_mem {x : α} {c : g.cycleFactorsFinset} (hx : x ∈ c.val.support) {m : ℤ}
(hm : (g ^ m) (a c) = x) : ofPermHomFun a τ x = (g ^ m) (a ((τ : Perm g.cycleFactorsFinset) c)) :=
by
have hx' : c = g.cycleOf x := cycle_is_cycleOf hx (Subtype.prop c)
have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop
set n := Nat.find (a.sameCycle hx'').exists_nat_pow_eq
have hn : (g ^ (n : ℤ)) (a c) = x :=
by
rw [← Nat.find_spec (a.sameCycle hx'').exists_nat_pow_eq, zpow_natCast]
congr
rw [← Subtype.coe_inj, hx']
suffices ofPermHomFun a τ x = (g ^ (n : ℤ)) (a ((τ : Perm g.cycleFactorsFinset) c))
by
rw [this,
IsCycleOn.zpow_apply_eq_zpow_apply
(isCycleOn_support_of_mem_cycleFactorsFinset ((τ : Perm g.cycleFactorsFinset) c).prop)
(mem_support_self a ((τ : Perm g.cycleFactorsFinset) c))]
simp only [τ.prop c]
rw [←
IsCycleOn.zpow_apply_eq_zpow_apply (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)]
rw [hn, hm]
simp only [ofPermHomFun, dif_pos hx'']
congr
exact hx'.symm
