English
For any x and y, if x and y belong to the same cycle under f, then x and y belong to the same support structure and the cycles coincide on their support.
Русский
Для любых x,y, если они находятся в одном цикле относительно f, то они принадлежат одной и той же поддержке и циклы совпадают на их поддержке.
LaTeX
$$$f.SameCycle x y \\\\Rightarrow x,y \\\\in \\\\text{support}(f) \\\\Rightarrow f.cycleOf x = f.cycleOf y$$$
Lean4
theorem mem_list_cycles_iff {α : Type*} [Finite α] {l : List (Perm α)} (h1 : ∀ σ : Perm α, σ ∈ l → σ.IsCycle)
(h2 : l.Pairwise Disjoint) {σ : Perm α} : σ ∈ l ↔ σ.IsCycle ∧ ∀ a, σ a ≠ a → σ a = l.prod a :=
by
suffices σ.IsCycle → (σ ∈ l ↔ ∀ a, σ a ≠ a → σ a = l.prod a) by
exact ⟨fun hσ => ⟨h1 σ hσ, (this (h1 σ hσ)).mp hσ⟩, fun hσ => (this hσ.1).mpr hσ.2⟩
intro h3
classical
cases nonempty_fintype α
constructor
· intro h a ha
exact eq_on_support_mem_disjoint h h2 _ (mem_support.mpr ha)
· intro h
have hσl : σ.support ⊆ l.prod.support := by
intro x hx
rw [mem_support] at hx
rwa [mem_support, ← h _ hx]
obtain ⟨a, ha, -⟩ := id h3
rw [← mem_support] at ha
obtain ⟨τ, hτ, hτa⟩ := exists_mem_support_of_mem_support_prod (hσl ha)
have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2
have key : ∀ x ∈ σ.support ∩ τ.support, σ x = τ x :=
by
intro x hx
rw [h x (mem_support.mp (mem_of_mem_inter_left hx)), hτl x (mem_of_mem_inter_right hx)]
convert hτ
refine h3.eq_on_support_inter_nonempty_congr (h1 _ hτ) key ?_ ha
exact key a (mem_inter_of_mem ha hτa)
