English
For a cycle σ, the subgroup generated by σ is in bijection with its support; there exists an Equiv between the two finite sets.
Русский
Для цикла σ порожденная им подгруппа и поддержка цикла связаны биекцией; существует эквивиалентность между ними.
LaTeX
$$(Subgroup.zpowers σ) ≃ σ.support$$
Lean4
/-- The subgroup generated by a cycle is in bijection with its support -/
noncomputable def zpowersEquivSupport {σ : Perm α} (hσ : IsCycle σ) : (Subgroup.zpowers σ) ≃ σ.support :=
Equiv.ofBijective
(fun (τ : ↥((Subgroup.zpowers σ) : Set (Perm α))) =>
⟨(τ : Perm α) (Classical.choose hσ), by
obtain ⟨τ, n, rfl⟩ := τ
rw [Subtype.coe_mk, zpow_apply_mem_support, mem_support]
exact (Classical.choose_spec hσ).1⟩)
(by
constructor
· rintro ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h
ext y
by_cases hy : σ y = y
· simp_rw [zpow_apply_eq_self_of_apply_eq_self hy]
· obtain ⟨i, rfl⟩ := (Classical.choose_spec hσ).2 hy
rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]
exact congr_arg _ (Subtype.ext_iff.mp h)
· rintro ⟨y, hy⟩
rw [mem_support] at hy
obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy
exact ⟨⟨σ ^ n, n, rfl⟩, rfl⟩)
