English
If f is a cycle factor of g, then the cycle factors of g multiplied by f^{-1} are exactly the cycle factors of g with f removed.
Русский
Если f является циклом-фактором g, то cycleFactorsFinset( g f^{-1}) = cycleFactorsFinset(g) без {f}.
LaTeX
$$$\forall {f,g : \mathrm{Perm}(\alpha)}, f \in cycleFactorsFinset(g) \Rightarrow cycleFactorsFinset (g * f^{-1}) = cycleFactorsFinset(g) \setminus \{ f \}$$$
Lean4
theorem cycleFactorsFinset_mul_inv_mem_eq_sdiff [DecidableEq α] [Fintype α] {f g : Perm α}
(h : f ∈ cycleFactorsFinset g) : cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ { f } :=
by
revert f
refine
cycle_induction_on (P := fun {g : Perm α} ↦
∀ {f}, (f ∈ cycleFactorsFinset g) → cycleFactorsFinset (g * f⁻¹) = cycleFactorsFinset g \ { f }) _ ?_ ?_ ?_
· simp
· intro σ hσ f hf
simp only [cycleFactorsFinset_eq_singleton_self_iff.mpr hσ, mem_singleton] at hf ⊢
simp [hf]
· intro σ τ hd _ hσ hτ f
simp_rw [hd.cycleFactorsFinset_mul_eq_union, mem_union]
-- if only `wlog` could work here...
rintro (hf | hf)
· rw [hd.commute.eq, union_comm, union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
Disjoint.cycleFactorsFinset_mul_eq_union, hσ hf]
· rw [mem_cycleFactorsFinset_iff] at hf
intro x
rcases hd.symm x with hx | hx
· exact Or.inl hx
· refine Or.inr ?_
by_cases hfx : f x = x
· rw [← hfx]
simpa [hx] using hfx.symm
· rw [mul_apply]
rw [← hf.right _ (mem_support.mpr hfx)] at hx
contradiction
· exact fun H => notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem hf H))
· rw [union_sdiff_distrib, sdiff_singleton_eq_erase, erase_eq_of_notMem, mul_assoc,
Disjoint.cycleFactorsFinset_mul_eq_union, hτ hf]
· rw [mem_cycleFactorsFinset_iff] at hf
intro x
rcases hd x with hx | hx
· exact Or.inl hx
· refine Or.inr ?_
by_cases hfx : f x = x
· rw [← hfx]
simpa [hx] using hfx.symm
· rw [mul_apply]
rw [← hf.right _ (mem_support.mpr hfx)] at hx
contradiction
· exact fun H => notMem_empty _ (hd.disjoint_cycleFactorsFinset.le_bot (mem_inter_of_mem H hf))
