English
The action respects cycle unions and disjointness: the image under ofPermHomFun is disjoint on different cycle factors.
Русский
Действие сохраняет непересечение: изображение через ofPermHomFun не пересекается на разных факторцикла.
LaTeX
$$disjointness of supports under ofPermHomFun$$
Lean4
theorem ofPermHomFun_commute_zpow_apply (x : α) (j : ℤ) : ofPermHomFun a τ ((g ^ j) x) = (g ^ j) (ofPermHomFun a τ x) :=
by
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | hx)
· rw [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ofPermHomFun_apply_of_mem_fixedPoints]
rw [Function.mem_fixedPoints_iff]
simp only [← mul_apply, ← zpow_one_add, add_comm]
conv_rhs => rw [← hx, ← mul_apply, ← zpow_add_one]
· obtain ⟨c, hc, m, hm⟩ := hx
have hm' : (g ^ (j + m)) (a c) = (g ^ j) x := by rw [zpow_add, mul_apply, hm]
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm, ofPermHomFun_apply_of_cycleOf_mem a τ _ hm', ← mul_apply, ←
zpow_add]
exact zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff.mpr hc
