English
If g ∈ G is a cycle in the permutation group, then the fixing-subgroup action is pretransitive.
Русский
Если в группе G есть цикл g, то действие фиксации подгруппы является предтранситивным.
LaTeX
$$IsPretransitive (fixingSubgroup G (g.support)ᶜ) (SubMulAction.ofFixingSubgroup G (g.support)ᶜ)$$
Lean4
theorem isPretransitive_of_isCycle_mem {g : Perm α} (hgc : g.IsCycle) (hg : g ∈ G) :
IsPretransitive (fixingSubgroup G (g.support : Set α)ᶜ) (SubMulAction.ofFixingSubgroup G (g.support : Set α)ᶜ) :=
by
obtain ⟨a, _, hgc⟩ := hgc
have hs : ∀ x : α, g • x ≠ x ↔ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ) :=
by
intro x
simp [SubMulAction.mem_ofFixingSubgroup_iff]
suffices
∀ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ),
∃ k : fixingSubgroup G ((↑g.support : Set α)ᶜ), x = k • a
by
rw [isPretransitive_iff]
rintro ⟨x, hx⟩ ⟨y, hy⟩
obtain ⟨k, hk⟩ := this x hx
obtain ⟨k', hk'⟩ := this y hy
use k' * k⁻¹
rw [← SetLike.coe_eq_coe]
simp only [SetLike.mk_smul_mk]
rw [hk, hk', smul_smul, inv_mul_cancel_right]
intro x hx
have hg' : (⟨g, hg⟩ : ↥G) ∈ fixingSubgroup G ((↑g.support : Set α)ᶜ) :=
by
simp_rw [mem_fixingSubgroup_iff G]
intro y hy
simpa only [Set.mem_compl_iff, Finset.mem_coe, notMem_support] using hy
let g' : fixingSubgroup (↥G) ((↑g.support : Set α)ᶜ) := ⟨(⟨g, hg⟩ : ↥G), hg'⟩
obtain ⟨i, hi⟩ := hgc ((hs x).mpr hx)
exact ⟨g' ^ i, hi.symm⟩
