English
The action of the centralizer element via toCentralizer is equivariant with respect to the cycle-factor structure, aligning with the action of the corresponding τ on cycle factors.
Русский
Действие элемента центральизатора через toCentralizer эквивариантно по отношению к структуре факторов цикла, согласуясь с действием соответствующего τ на факторы цикла.
LaTeX
$$$(toCentralizer\\;a\\;\\tau) \\cdot c = (\\tau : Perm\\ g.cycleFactorsFinset)\\;c$$$
Lean4
theorem toCentralizer_equivariant : (toCentralizer a τ) • c = (τ : Perm g.cycleFactorsFinset) c :=
by
simp only [← Subtype.coe_inj, val_centralizer_smul, InvMemClass.coe_inv, mul_inv_eq_iff_eq_mul]
ext x
simp only [mul_apply, toCentralizer_apply]
by_cases hx : x ∈ c.val.support
· rw [(mem_cycleFactorsFinset_iff.mp c.prop).2 x hx]
have := ofPermHomFun_commute_zpow_apply a τ x 1
simp only [zpow_one] at this
rw [this, ← (mem_cycleFactorsFinset_iff.mp ((τ : Perm g.cycleFactorsFinset) c).prop).2]
rw [ofPermHomFun_apply_mem_support_cycle_iff]
exact hx
· rw [notMem_support.mp hx, eq_comm, ← notMem_support, ofPermHomFun_apply_mem_support_cycle_iff]
exact hx
