English
If Nat.card α = 4 and g lies in Alt α, and orderOf g divides 2^n, then the cycleType of g is either empty or {2,2}.
Русский
Если |α| = 4 и g ∈ Alt α, и order(g) делит 2^n, то cycleType(g) равно пустому или {2,2}.
LaTeX
$$$Nat.card α = 4 \Rightarrow (g ∈ Alt(α) \land orderOf g \mid 2^n) \Rightarrow (g.cycleType = \emptyset \lor g.cycleType = {2,2})$$$
Lean4
theorem mem_kleinFour_of_order_two_pow (hα4 : Nat.card α = 4) {g : Perm α} (hg0 : g ∈ alternatingGroup α) {n : ℕ}
(hg : orderOf g ∣ 2 ^ n) : g.cycleType = { } ∨ g.cycleType = { 2, 2 } :=
by
rw [mem_alternatingGroup, sign_of_cycleType] at hg0
have h1 : g.cycleType.sum ≤ 4 := by
rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
exact g.support.card_le_univ
have h2 : ∀ k ∈ g.cycleType, k = 2 := by
intro k hk
have hk4 := (Multiset.le_sum_of_mem hk).trans h1
have hk1 := one_lt_of_mem_cycleType hk
interval_cases k
· rfl
· rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)
· contrapose! hg0
obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk
rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff, Multiset.sum_eq_zero_iff, ←
Multiset.eq_replicate_card] at h1
have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
simp [ht, h, Units.ext_iff]
rw [← Multiset.eq_replicate_card] at h2
rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1
interval_cases g.cycleType.card <;> simp [h2, Units.ext_iff] at hg0 ⊢
