English
If there exists a nontrivial fixed point for a permutation action, then a certain pretransitive property holds for the corresponding subgroup action.
Русский
Если существует нетривиальная точка фиксации для перестановочного действия, то выполняется соответствующее предтранситивное свойство для подгруппы.
LaTeX
$$IsMultiplyPretransitive K α n$$
Lean4
theorem isMultiplyPretransitive_of_nontrivial {K : Type*} [Group K] [MulAction K α] (hα : Nat.card α = 2)
(hK : fixedPoints K α ≠ .univ) (n : ℕ) : IsMultiplyPretransitive K α n :=
by
have : Finite α := Or.resolve_right (finite_or_infinite α) (fun _ ↦ by simp [Nat.card_eq_zero_of_infinite] at hα)
have : Fintype α := Fintype.ofFinite α
suffices h2 : IsMultiplyPretransitive K α 2 by
by_cases hn : n ≤ 2
· apply MulAction.isMultiplyPretransitive_of_le' hn
simp [← hα]
· suffices (IsEmpty (Fin n ↪ α)) by infer_instance
apply Or.resolve_right (isEmpty_or_nonempty _)
rwa [Function.Embedding.nonempty_iff_card_le, Fintype.card_fin, ← Nat.card_eq_fintype_card, hα]
let φ := MulAction.toPermHom K α
let f : α →ₑ[φ] α :=
{ toFun := id
map_smul' := fun _ _ ↦ rfl }
have hf : Function.Bijective f := Function.bijective_id
suffices Function.Surjective φ by
unfold IsMultiplyPretransitive
rw [IsPretransitive.of_embedding_congr this hf (n := Fin 2), ← hα]
apply Perm.isMultiplyPretransitive
rw [← MonoidHom.range_eq_top]
apply Subgroup.eq_top_of_card_eq
apply le_antisymm (card_le_card_group φ.range)
simp only [Nat.card_perm, hα, Nat.factorial_two]
by_contra H
simp only [not_le, Nat.lt_succ, Finite.card_le_one_iff_subsingleton] at H
apply hK
apply Set.eq_univ_of_univ_subset
intro a _ g
suffices φ g = φ 1 by
conv_rhs => rw [← one_smul K a]
simp only [← toPerm_apply, ← toPermHom_apply K α g]
exact congrFun (congrArg DFunLike.coe this) a
simpa [← Subtype.coe_inj] using H.elim ⟨_, ⟨g, rfl⟩⟩ ⟨_, ⟨1, rfl⟩⟩
