English
If σ.cycleType = τ.cycleType, then σ and τ are conjugate (IsConj).
Русский
Если cycleType(σ) = cycleType(τ), то σ и τ сопряжены.
LaTeX
$$$$\mathrm{cycleType}(\sigma) = \mathrm{cycleType}(\tau) \implies \mathrm{IsConj}(\sigma, \tau). $$$$
Lean4
theorem isConj_of_cycleType_eq {σ τ : Perm α} (h : cycleType σ = cycleType τ) : IsConj σ τ := by
induction σ using cycle_induction_on generalizing τ with
| base_one =>
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h
rw [h]
| base_cycles σ hσ =>
have hτ := card_cycleType_eq_one.2 hσ
rw [h, card_cycleType_eq_one] at hτ
apply hσ.isConj hτ
rwa [hσ.cycleType, hτ.cycleType, Multiset.singleton_inj] at h
| induction_disjoint σ π hd hc hσ hπ =>
rw [hd.cycleType_mul] at h
have h' : #σ.support ∈ τ.cycleType := by simp [← h, hc.cycleType]
obtain ⟨σ', hσ'l, hσ'⟩ := Multiset.mem_map.mp h'
have key : IsConj (σ' * τ * σ'⁻¹) τ := (isConj_iff.2 ⟨σ', rfl⟩).symm
refine IsConj.trans ?_ key
rw [mul_assoc]
have hs : σ.cycleType = σ'.cycleType :=
by
rw [← Finset.mem_def, mem_cycleFactorsFinset_iff] at hσ'l
rw [hc.cycleType, ← hσ', hσ'l.left.cycleType]; rfl
refine hd.isConj_mul (hσ hs) (hπ ?_) ?_
· rw [cycleType_mul_inv_mem_cycleFactorsFinset_eq_sub, ← h, add_comm, hs, add_tsub_cancel_right]
rwa [Finset.mem_def]
· exact (disjoint_mul_inv_of_mem_cycleFactorsFinset hσ'l).symm
