English
Let σ,π and τ,ρ be permutations of a finite set with σ conjugate to π and τ conjugate to ρ, and suppose σ and τ are disjoint as well as π and ρ. Then the product σ τ is conjugate to π ρ.
Русский
Пусть σ конъюгирован к π, τ конъюгирован к ρ, и при этом σ и τ_disjoint, а также π и ρ_disjoint. Тогда произведение σ τ конъюгировано к π ρ.
LaTeX
$$$\\text{If } σ \\sim π \\text{ and } τ \\sim ρ \\text{ and } Disjoint(σ,τ), Disjoint(π,ρ), \\text{ then } στ \\sim πρ.$$$
Lean4
theorem isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ π) (hc2 : IsConj τ ρ) (hd1 : Disjoint σ τ)
(hd2 : Disjoint π ρ) : IsConj (σ * τ) (π * ρ) := by
classical
cases nonempty_fintype α
obtain ⟨f, rfl⟩ := isConj_iff.1 hc1
obtain ⟨g, rfl⟩ := isConj_iff.1 hc2
have hd1' := coe_inj.2 hd1.support_mul
have hd2' := coe_inj.2 hd2.support_mul
rw [coe_union] at *
have hd1'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd1)
have hd2'' := disjoint_coe.2 (disjoint_iff_disjoint_support.1 hd2)
refine isConj_of_support_equiv ?_ ?_
·
refine
((Equiv.setCongr hd1').trans (Equiv.Set.union hd1'')).trans
((Equiv.sumCongr (subtypeEquiv f fun a => ?_) (subtypeEquiv g fun a => ?_)).trans
((Equiv.setCongr hd2').trans (Equiv.Set.union hd2'')).symm) <;>
· simp only [Set.mem_image, toEmbedding_apply, exists_eq_right, support_conj, coe_map, apply_eq_iff_eq]
· intro x hx
simp only [trans_apply, symm_trans_apply, Equiv.setCongr_apply, Equiv.setCongr_symm_apply, Equiv.sumCongr_apply]
rw [hd1', Set.mem_union] at hx
rcases hx with hxσ | hxτ
· rw [mem_coe, mem_support] at hxσ
rw [Set.union_apply_left, Set.union_apply_left]
· simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply, Set.union_symm_apply_left, Subtype.coe_mk,
apply_eq_iff_eq]
have h := (hd2 (f x)).resolve_left ?_
· rw [mul_apply, mul_apply] at h
rw [h, inv_apply_self, (hd1 x).resolve_left hxσ]
· rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
· rwa [Subtype.coe_mk, mem_coe, mem_support]
· rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe, apply_mem_support, mem_support]
· rw [mem_coe, ← apply_mem_support, mem_support] at hxτ
rw [Set.union_apply_right, Set.union_apply_right]
· simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply, Set.union_symm_apply_right,
Subtype.coe_mk]
have h := (hd2 (g (τ x))).resolve_right ?_
· rw [mul_apply, mul_apply] at h
rw [inv_apply_self, h, (hd1 (τ x)).resolve_right hxτ]
· rwa [mul_apply, mul_apply, inv_apply_self, apply_eq_iff_eq]
· rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
· rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ, mem_coe, mem_support]
