odd_of_centralizer_le_alternatingGroup

English

If the centralizer of g is contained in the alternating group, then every cycle length occurring in g is odd.

Русский

Если центральизатор g лежит внутри чередующейся группы, то каждый встречающийся в g размер цикла нечетный.

LaTeX

$$$\text{If } \operatorname{Cent}(g) \le \operatorname{Alt}(\alpha), \ \forall i \in g.cycleType:\; Odd(i)$$$

Lean4

theorem odd_of_centralizer_le_alternatingGroup (h : Subgroup.centralizer { g } ≤ alternatingGroup α) (i : ℕ)
    (hi : i ∈ g.cycleType) : Odd i :=
  by
  rw [cycleType_def g, Multiset.mem_map] at hi
  obtain ⟨c, hc, rfl⟩ := hi
  rw [← Finset.mem_def] at hc
  suffices sign c = 1 by
    rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
    · rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow
    · rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left
  apply h
  rw [Subgroup.mem_centralizer_singleton_iff]
  exact Equiv.Perm.self_mem_cycle_factors_commute hc

Похожие утверждения