English
Two cycle factors Finsets are equal iff the underlying cycle lists satisfy the cycle conditions and the products agree.
Русский
Два цикла-фактора-файнсета равны тогда и только тогда, когда соответствующие списки циклов удовлетворяют условиям цикла и произведение совпадает.
LaTeX
$$$cycleFactorsFinset = s \\iff \\big( \\forall f, f \\in s \\Rightarrow f.IsCycle \\big) \\land \\exists h, s.noncommProd id = f$$$
Lean4
theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
σ.cycleFactorsFinset = l.toFinset ↔ (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ :=
by
obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors
have ht : cycleFactorsFinset σ = l'.toFinset := by
rw [cycleFactorsFinset, ← hl, Trunc.lift_mk, Multiset.toFinset_eq, List.toFinset_coe]
rw [ht]
constructor
· intro h
have hn' : l'.Nodup := nodup_of_pairwise_disjoint_cycles hc' hd'
have hperm : l ~ l' := List.perm_of_nodup_nodup_toFinset_eq hn hn' h.symm
refine ⟨?_, ?_, ?_⟩
· exact fun _ h => hc' _ (hperm.subset h)
· have := List.Perm.pairwise_iff (@Disjoint.symmetric _) hperm
rwa [this]
· rw [← hp', hperm.symm.prod_eq']
refine hd'.imp ?_
exact Disjoint.commute
· rintro ⟨hc, hd, hp⟩
refine List.toFinset_eq_of_perm _ _ ?_
refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd
rw [hp, hp']
