English
Let m and n be finite types. If a permutation σ of the disjoint sum m ⊕ n preserves the left summand (i.e., maps the image of Sum.inl into itself), then σ arises from independently permuting m and n. Equivalently, σ lies in the image of the natural map Perm(m) × Perm(n) → Perm(m ⊕ n) that acts separately on each summand.
Русский
Пусть m и n – конечные множества. Пусть σ — перестановка над объединением m ⊔ n, которая сохраняет левый блок (отображает множество Sum.inl в Sum.inl). Тогда σ получается путём независимой перестановки элементов m и элементов n; то есть σ лежит в образе отображения Perm(m) × Perm(n) → Perm(m ⊕ n), действующего по каждому сомножителю на своей части.
LaTeX
$$$\\exists \\alpha \\in \\mathrm{Sym}(m), \\exists \\beta \\in \\mathrm{Sym}(n): \\sigma = \\mathrm{sumCongrHom}(m,n)(\\alpha,\\beta).$$$
Lean4
theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type*} [Finite m] [Finite n] {σ : Perm (m ⊕ n)}
(h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) : σ ∈ (sumCongrHom m n).range := by
classical
have h1 : ∀ x : m ⊕ n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x :=
by
rintro x ⟨a, ha⟩
apply h
rw [← ha]
exact ⟨a, rfl⟩
have h3 : ∀ x : m ⊕ n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x :=
by
rintro x ⟨b, hb⟩
apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
rw [← hb]
exact ⟨b, rfl⟩
let σ₁' := subtypePermOfFintype σ h1
let σ₂' := subtypePermOfFintype σ h3
let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
rw [MonoidHom.mem_range, Prod.exists]
use σ₁, σ₂
rw [Perm.sumCongrHom_apply]
ext x
rcases x with a | b
· rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inl_injective]
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
dsimp [Set.range]
rw [subtypePerm_apply]
· rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inr_injective,
ofInjective_apply]
dsimp [Set.range]
rw [subtypePerm_apply]
