English
The centralizer of g is contained in the alternating group if and only if all cycle lengths are odd, the size bound holds, and each cycle length occurs at most once.
Русский
Централиатор {g} лежит в Alt(α) тогда и только тогда, когда все длины циклов нечетны, соблюдается граница на размер множества и для каждой длины цикла встречается не более одного раза.
LaTeX
$$$ Subgroup.centralizer\{ g \} \le Alt(\alpha) \iff (\forall c \in g.cycleType, Odd c) \land |\alpha| \le g.cycleType.sum + 1 \land \forall i, g.cycleType.count i \le 1$$$
Lean4
/-- The centralizer of a permutation is contained in the alternating group if and only if
its cycles have odd length, with at most one of each, and there is at most one fixed point. -/
theorem centralizer_le_alternating_iff :
Subgroup.centralizer { g } ≤ alternatingGroup α ↔
(∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ i, g.cycleType.count i ≤ 1 :=
by
rw [SetLike.le_def]
constructor
· intro h
exact
⟨odd_of_centralizer_le_alternatingGroup h, card_le_of_centralizer_le_alternating h,
count_le_one_of_centralizer_le_alternating h⟩
· rintro ⟨h_odd, h_fixed, h_count⟩ x hx
rw [← kerParam_range_eq_centralizer_of_count_le_one h_count] at hx
obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx
rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]
convert mul_one _
· apply Finset.prod_eq_one
rintro ⟨c, hc⟩ _
obtain ⟨k, hk⟩ := (uv _).prop
rw [← hk, map_zpow]
convert one_zpow k
rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]
· apply h_odd
rw [cycleType_def, Multiset.mem_map]
exact ⟨c, hc, rfl⟩
· rw [mem_cycleFactorsFinset_iff] at hc
exact hc.left
· suffices y = 1 by simp [this]
have := card_fixedPoints g
exact card_support_le_one.mp <| le_trans (Finset.card_le_univ _) (by cutsat)
