English
For g,c with c ∈ g.cycleFactorsFinset and x ∈ α, we have c = g.cycleOf x iff x ∈ c.support.
Русский
Для g,c с c ∈ cycleFactorsFinset(g) и x ∈ α верно: c = g.cycleOf x ↔ x ∈ c.support.
LaTeX
$$c = g.cycleOf x ↔ x ∈ c.support$$
Lean4
/-- If c is a cycle, a ∈ c.support and c is a cycle of f, then `c = f.cycleOf a` -/
theorem cycle_is_cycleOf {f c : Equiv.Perm α} {a : α} (ha : a ∈ c.support) (hc : c ∈ f.cycleFactorsFinset) :
c = f.cycleOf a :=
by
suffices f.cycleOf a = c.cycleOf a by
rw [this]
apply symm
exact
Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left (Equiv.Perm.mem_support.mp ha)
let hfc := (Equiv.Perm.disjoint_mul_inv_of_mem_cycleFactorsFinset hc).symm
let hfc2 := Perm.Disjoint.commute hfc
rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]
·
simp only [hfc2.eq, inv_mul_cancel_right]
-- `a` is in the support of `c`, hence it is not in the support of `g c⁻¹`
exact Equiv.Perm.notMem_support.mp (Finset.disjoint_left.mp (Equiv.Perm.Disjoint.disjoint_support hfc) ha)
