English
There is a natural equivalence between the set of cyclic permutations of α and the set of nontrivial nodup cycles in α; forward and inverse maps are given by taking the formPerm and forming a cycle respectively.
Русский
Существует естественный биективный correspondence между циклическими перестановками на α и ненулевыми неповторяющимися циклами в α; переход вперёд задаётся формой перестановки цикла, переход обратно — построением цикла.
LaTeX
$$$\\{ f : Perm α \\mid IsCycle f \\} \\cong { s : 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 finding this `Cycle α` using `Fintype.choose`.
-/
def isoCycle' : { f : Perm α // IsCycle f } ≃ { s : Cycle α // s.Nodup ∧ s.Nontrivial } :=
let f : { s : Cycle α // s.Nodup ∧ s.Nontrivial } → { f : Perm α // IsCycle f } := fun s =>
⟨(s : Cycle α).formPerm s.prop.left, (s : Cycle α).isCycle_formPerm _ s.prop.right⟩
{ toFun :=
Fintype.bijInv
(show Function.Bijective f by
rw [Function.bijective_iff_existsUnique]
rintro ⟨f, hf⟩
simp only [Subtype.ext_iff]
exact hf.existsUnique_cycle_nontrivial_subtype)
invFun := f
left_inv := Fintype.rightInverse_bijInv _
right_inv := Fintype.leftInverse_bijInv _ }
-- mutes `'decide' tactic does nothing [linter.unusedTactic]`
