English
Let σ, τ be elements of Alt(α) such that there exists a permutation π with σ = π τ π^{-1} and a support bound; then σ and τ are conjugate in Alt(α).
Русский
Пусть σ, τ ∈ Alt(α) такие, что существует перестановка π с σ = π τ π^{-1} и выполняется ограничение по опоре; тогда σ и τ конъугированы в Alt(α).
LaTeX
$$$\text{IsConj}_{\mathrm{Alt}(\alpha)}(\sigma,\tau)$ под предпосылками hc и hσ$$
Lean4
theorem isConj_of {σ τ : alternatingGroup α} (hc : IsConj (σ : Perm α) (τ : Perm α))
(hσ : (σ : Perm α).support.card + 2 ≤ Fintype.card α) : IsConj σ τ :=
by
obtain ⟨σ, hσ⟩ := σ
obtain ⟨τ, hτ⟩ := τ
obtain ⟨π, hπ⟩ := isConj_iff.1 hc
rw [Subtype.coe_mk, Subtype.coe_mk] at hπ
rcases Int.units_eq_one_or (Perm.sign π) with h | h
· rw [isConj_iff]
refine ⟨⟨π, mem_alternatingGroup.mp h⟩, Subtype.val_injective ?_⟩
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using hπ
· have h2 : 2 ≤ σ.supportᶜ.card :=
by
rw [Finset.card_compl, le_tsub_iff_left σ.support.card_le_univ]
exact hσ
obtain ⟨a, ha, b, hb, ab⟩ := Finset.one_lt_card.1 h2
refine isConj_iff.2 ⟨⟨π * swap a b, ?_⟩, Subtype.val_injective ?_⟩
· rw [mem_alternatingGroup, MonoidHom.map_mul, h, sign_swap ab, Int.units_mul_self]
· simp only [← hπ, Subgroup.coe_mul]
have hd : Disjoint (swap a b) σ :=
by
rw [disjoint_iff_disjoint_support, support_swap ab, Finset.disjoint_insert_left, Finset.disjoint_singleton_left]
exact ⟨Finset.mem_compl.1 ha, Finset.mem_compl.1 hb⟩
rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk]
simp [mul_assoc]
