English
The image, under the natural embedding, of even permutations with cycleType m from the alternating group corresponds to the set of all permutations with cycleType m, provided a parity condition holds; otherwise the image is empty.
Русский
Образ при естественном вложении чётных перестановок с cycleType m из чередующейся группы соответствует множеству перестановок с cycleType m, если выполняется условие по парности; иначе образ пуст.
LaTeX
$$$\text{map} (\text{Embedding.subtype }\_)\Big(\{ g\in alternatingGroup(\alpha)\mid (g : Perm \alpha).cycleType = m\}\Big) = \begin{cases} \{ g\in Perm(\alpha)\mid g.cycleType = m\}\ , & \text{Even}(m.sum + m.card) \\ \emptyset, & \text{otherwise} \end{cases}$$$
Lean4
theorem map_subtype_of_cycleType (m : Multiset ℕ) :
({g | (g : Perm α).cycleType = m} : Finset (alternatingGroup α)).map (Embedding.subtype _) =
if Even (m.sum + m.card) then ({g | g.cycleType = m} : Finset (Perm α)) else ∅ :=
by
split_ifs with hm
· ext g
simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists, mem_alternatingGroup,
exists_and_left, exists_prop, exists_eq_right_right, and_iff_left_iff_imp]
intro hg
rw [sign_of_cycleType, hg, Even.neg_one_pow hm]
· rw [Finset.eq_empty_iff_forall_notMem]
intro g hg
simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists, mem_alternatingGroup,
exists_and_left, exists_prop, exists_eq_right_right] at hg
rcases hg with ⟨hg, hs⟩
rw [g.sign_of_cycleType, hg, neg_one_pow_eq_one_iff_even (by simp)] at hs
contradiction
