English
If the centralizer of g lies in the alternating group, then each cycle length i appears at most once in g’s cycle type.
Русский
Если центральизатор g лежит в Alt(α), то любой длине цикла i встречается не более одного раза в cycleType(g).
LaTeX
$$$\forall i:\mathbb{N},\; g.cycleType.count(i) \le 1$$$
Lean4
theorem count_le_one_of_centralizer_le_alternating (h : Subgroup.centralizer { g } ≤ alternatingGroup α) :
∀ i, g.cycleType.count i ≤ 1 :=
by
rw [← Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def]
rw [Multiset.nodup_map_iff_inj_on g.cycleFactorsFinset.nodup]
simp only [Function.comp_apply, ← Finset.mem_def]
by_contra! hm
obtain ⟨c, hc, d, hd, hm, hm'⟩ := hm
let τ : Equiv.Perm g.cycleFactorsFinset := Equiv.swap ⟨c, hc⟩ ⟨d, hd⟩
obtain ⟨a⟩ := Equiv.Perm.Basis.nonempty g
have hτ : τ ∈ range_toPermHom' g := fun x ↦ by
by_cases hx : x = ⟨c, hc⟩
· rw [hx, Equiv.swap_apply_left]; exact hm.symm
by_cases hx' : x = ⟨d, hd⟩
· rw [hx', Equiv.swap_apply_right]; exact hm
· rw [Equiv.swap_apply_of_ne_of_ne hx hx']
set k := toCentralizer a ⟨τ, hτ⟩ with hk
suffices hsign_k : k.val.sign = -1 by
apply units_ne_neg_self (1 : ℤˣ)
rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]
/- to prove that `hsign_k : sign k = -1` below,
we could prove that it is the product of the transpositions with disjoint supports
[(g ^ n) (a c), (g ^ n) (a d)], for 0 ≤ n < c.support.card,
which are in odd number by `odd_of_centralizer_le_alternatingGroup`,
but it will be sufficient to observe that `k ^ 2 = 1`
(which implies that `k.cycleType` is of the form (2,2,…))
and to control its support. -/
have hk_cT : k.val.cycleType = Multiset.replicate k.val.cycleType.card 2 :=
by
rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow, ← Subgroup.coe_one, Subtype.coe_inj, hk,
← map_pow]
convert MonoidHom.map_one _
rw [← Subtype.coe_inj]
apply Equiv.swap_mul_self
rw [sign_of_cycleType, hk_cT]
simp only [Multiset.sum_replicate, smul_eq_mul, Multiset.card_replicate, pow_add, even_two, Even.mul_left,
Even.neg_pow, one_pow, one_mul]
apply Odd.neg_one_pow
apply odd_of_centralizer_le_alternatingGroup h
have this : (k : Perm α).cycleType.card * 2 = (k : Perm α).support.card :=
by
rw [← sum_cycleType, hk_cT]
simp
have that : Multiset.card (k : Perm α).cycleType = (c : Perm α).support.card :=
by
rw [← Nat.mul_left_inj (a := 2) (by simp), this]
simp only [hk, toCentralizer, MonoidHom.coe_mk, OneHom.coe_mk, card_ofPermHom_support]
have H : (⟨c, hc⟩ : g.cycleFactorsFinset) ≠ ⟨d, hd⟩ := Subtype.coe_ne_coe.mp hm'
simp only [τ, support_swap H]
rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]), Finset.sum_singleton, hm, mul_two]
rw [that]
simp only [cycleType_def, Multiset.mem_map]
exact ⟨c, hc, by simp only [Function.comp_apply]⟩
