English
If the centralizer of g is contained in the alternating group, then the total size of the cycle type of g is bounded by the size of α, i.e., card α ≥ g.cycleType.sum.
Русский
Если центральизатор g лежит внутри чередующейся группы, то сумма длин циклов не превосходит размера множества.
LaTeX
$$$\text{If }\operatorname{Cent}({g}) \le \operatorname{Alt}(\alpha) \text{ then } |\alpha| \ge g.cycleType.sum$$$
Lean4
theorem card_le_of_centralizer_le_alternating (h : Subgroup.centralizer { g } ≤ alternatingGroup α) :
Fintype.card α ≤ g.cycleType.sum + 1 := by
by_contra! hm
replace hm : 2 + g.cycleType.sum ≤ Fintype.card α := by omega
suffices 1 < Fintype.card (Function.fixedPoints g)
by
obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 from this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
simp [sign_kerParam_apply_apply, hab]
rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]
rw [sum_cycleType]
exact Finset.card_le_univ _
