English
There is an isomorphism between cyclic permutations and the nontrivial nodup cycles given by toCycle and its inverse.
Русский
Существует изоморфизм между циклами перестановок и не тривиальными циклами без повторов, заданный toCycle и обратным отображением.
LaTeX
$$$$\text{isoCycle : }\{ f : \mathrm{Perm} \ α \mid \mathrm{IsCycle} f \} \simeq \{ s : \mathrm{Cycle} α \mid s.Nodup \land s.Nontrivial \}.$$$$
Lean4
/-- Any cyclic `f : Perm α` is isomorphic to the nontrivial `Cycle α`
that corresponds to repeated application of `f`.
The forward direction is implemented by `Equiv.Perm.toCycle`.
-/
def isoCycle : { f : Perm α // IsCycle f } ≃ { s : Cycle α // s.Nodup ∧ s.Nontrivial }
where
toFun f := ⟨toCycle (f : Perm α) f.prop, nodup_toCycle (f : Perm α) f.prop, nontrivial_toCycle _ f.prop⟩
invFun s := ⟨(s : Cycle α).formPerm s.prop.left, (s : Cycle α).isCycle_formPerm _ s.prop.right⟩
left_inv
f := by
obtain ⟨x, hx, -⟩ := id f.prop
simpa [toCycle_eq_toList (f : Perm α) f.prop x hx, formPerm_toList, Subtype.ext_iff] using f.prop.cycleOf_eq hx
right_inv
s := by
rcases s with ⟨⟨s⟩, hn, ht⟩
obtain ⟨x, -, -, hx, -⟩ := id ht
have hl : 2 ≤ s.length := by simpa using Cycle.length_nontrivial ht
simp only [Cycle.mk_eq_coe, Cycle.nodup_coe_iff, Cycle.mem_coe_iff, Cycle.formPerm_coe] at hn hx ⊢
apply Subtype.ext
dsimp
rw [toCycle_eq_toList _ _ x]
· refine Quotient.sound' ?_
exact toList_formPerm_isRotated_self _ hl hn _ hx
· rw [← mem_support, support_formPerm_of_nodup _ hn]
· simpa using hx
· rintro _ rfl
simp at hl
